The search result changed since you submitted your search request. Documents might be displayed in a different sort order.
  • search hit 33 of 656
Back to Result List

Unification in a Sorted (lambda)-Calculus with Term Declarations and Function Sorts

  • The introduction of sorts to first-order automated deduc-tion has brought greater conciseness of representation and a considerablegain in efficiency by reducing search spaces. This suggests that sort in-formation can be employed in higher-order theorem proving with similarresults. This paper develops a sorted (lambda)-calculus suitable for automatictheorem proving applications. It extends the simply typed (lambda)-calculus by ahigher-order sort concept that includes term declarations and functionalbase sorts. The term declaration mechanism studied here is powerfulenough to subsume subsorting as a derived notion and therefore gives ajustification for the special form of subsort inference. We present a set oftransformations for sorted (pre-) unification and prove the nondetermin-istic completeness of the algorithm induced by these transformations.

Download full text files

Export metadata

Additional Services

Share in Twitter Search Google Scholar
Author:Michael Kohlhase
URN (permanent link):urn:nbn:de:hbz:386-kluedo-2551
Document Type:Article
Language of publication:English
Year of Completion:1994
Year of Publication:1994
Publishing Institute:Technische Universität Kaiserslautern
Date of the Publication (Server):2000/04/03
Faculties / Organisational entities:Fachbereich Informatik
DDC-Cassification:0 Allgemeines, Informatik, Informationswissenschaft / 004 Informatik
Licence (German):Standard gemäß KLUEDO-Leitlinien vor dem 27.05.2011