Decidability of bounded higher order unification

  • It is shown that unifiability of terms in the simply zyped lambda calculus with β and η rules becomes decidable if there is a bound on the number of bound variables and lambdas in an unifier in η-long β-normal form.

Download full text files

Export metadata

Additional Services

Share in Twitter Search Google Scholar
Metadaten
Author:Manfred Schmidt-SchaußORCiDGND, Klaus U. Schulz
URN:urn:nbn:de:hebis:30-9039
URL:http://www.ki.informatik.uni-frankfurt.de/papers/schauss/bounded-ho5.ps
Parent Title (English):Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik ; 15
Series (Serial Number):Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik (15)
Publisher:Johann Wolfgang Goethe-Univ., Fachbereich Informatik und Mathematik, Inst. für Informatik, Research group for Artificial Intelligence and Software Technology
Place of publication:Frankfurt [am Main]
Document Type:Working Paper
Language:English
Year of Completion:2001
Year of first Publication:2001
Publishing Institution:Universitätsbibliothek Johann Christian Senckenberg
Release Date:2005/05/12
HeBIS-PPN:115213589
Institutes:Informatik und Mathematik / Informatik
Dewey Decimal Classification:0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik
Licence (German):License LogoDeutsches Urheberrecht

OPUS4 Logo