TY  - UNPD
A1  - Schmidt-Schauß, Manfred
A1  - Schulz, Klaus U.
T1  - Decidability of bounded higher order unification
T2  - Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik ; 15
N2  - 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.
T3  - Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik - 15 
Y1  - 2001
UR  - http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/4588
UR  - https://nbn-resolving.org/urn:nbn:de:hebis:30-9039
UR  - http://www.ki.informatik.uni-frankfurt.de/papers/schauss/bounded-ho5.ps
PB  - Johann Wolfgang Goethe-Univ., Fachbereich Informatik und Mathematik, Inst. für Informatik, Research group for Artificial Intelligence and Software Technology
CY  - Frankfurt [am Main]
ER  -