TY - JOUR
A1 - Johann, Patricia
A1 - Kohlhase, Michael
T1 - Unification in an Extensional Lambda Calculus with Ordered Function Sorts and Constant Overloading
N2 - 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.
T3 - SEKI Report - 93,14
Y1 - 1999
UR - https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/352
UR - https://nbn-resolving.org/urn:nbn:de:hbz:386-kluedo-3231
ER -