Unification in an Extensional Lambda Calculus with Ordered Function Sorts and Constant Overloading

  • We develop an order-sorted higher-order calculus suitable forautomatic theorem proving applications by extending the extensional simplytyped lambda calculus with a higher-order ordered sort concept and constantoverloading. Huet's well-known techniques for unifying simply typed lambdaterms are generalized to arrive at a complete transformation-based unificationalgorithm for this sorted calculus. Consideration of an order-sorted logicwith functional base sorts and arbitrary term declarations was originallyproposed by the second author in a 1991 paper; we give here a correctedcalculus which supports constant rather than arbitrary term declarations, aswell as a corrected unification algorithm, and prove in this setting resultscorresponding to those claimed there.

Export metadata

  • Export Bibtex
  • Export RIS

Additional Services

Share in Twitter Search Google Scholar
Metadaten
Author:Patricia Johann, Michael Kohlhase
URN (permanent link):urn:nbn:de:hbz:386-kluedo-3231
Serie (Series number):SEKI Report (93,14)
Document Type:Article
Language of publication:English
Year of Completion:1999
Year of Publication:1999
Publishing Institute:Technische Universität Kaiserslautern
Faculties / Organisational entities:Fachbereich Informatik
DDC-Cassification:004 Datenverarbeitung; Informatik

$Rev: 12793 $