Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
My Menu
Marked Items 
Alerts
Order History
Saved Items
All
Favorites
    
Book Chapter Printable view
Decidability of Bounded Higher-Order Unification

Decidability of Bounded Higher-Order Unification

Book SeriesLecture Notes in Computer Science
PublisherSpringer Berlin / Heidelberg
ISSN0302-9743 (Print) 1611-3349 (Online)
VolumeVolume 2471/2002
BookComputer Science Logic
DOI10.1007/3-540-45793-3
Copyright2002
ISBN978-3-540-44240-0
DOI10.1007/3-540-45793-3_35
Pages403-441
Subject CollectionComputer Science
SpringerLink DateTuesday, January 01, 2002
Add to marked items

Decidability of Bounded Higher-Order Unification

Manfred Schmidt-Schauß5 Contact Information and Klaus U. Schulz6 Contact Information

(5)  Institut für Informatik, J.-W.-Goethe-Universität, Postfach 11 19 32, D-60054 Frankfurt, Germany
(6)  CIS, University of Munich, Oettingenstr 67, D-80538 München, Germany
Abstract
It is shown that unifiability of terms in the simply typed lambda calculus with β and η rules becomes decidable if there is a bound on the number of bound variables and lambdas in a unifier in η-long β-normal form.

Contact Information Manfred Schmidt-Schauß
Email: schauss@ki.informatik.uni-frankfurt.de

Contact Information Klaus U. Schulz
Email: schulz@cis.uni-muenchen.de
Fulltext Preview (Small, Large)
Image of the first page of the fulltext

References secured to subscribers.
more options
Find


Export this chapter
Export this chapter as RIS | Text
 
Frequently asked questions | General information on journals and books | Send us your feedback | Impressum | Contact
© Springer. Part of Springer Science+Business Media
Privacy, Disclaimer, Terms and Conditions, © Copyright Information
Remote Address: 38.107.191.109 • Server: mpweb02
HTTP User Agent: CCBot/1.0 (+http://www.commoncrawl.org/bot.html)