DocumentCode
2144828
Title
Unification and anti-unification in the calculus of constructions
Author
Pfenning, Frank
Author_Institution
Sch. of Comput. Sci., Carnegie Mellon Univ., Pittsburgh, PA, USA
fYear
1991
fDate
15-18 July 1991
Firstpage
74
Lastpage
85
Abstract
Algorithms for unification and anti-unification in the calculus of constructions, where occurrences of free variables (the variables subject to instantiation) are restricted to higher-order patterns, are presented. Most general unifiers and least common anti-instances are shown to exist and are unique up to a simple equivalence. The unification algorithm is used for logic program execution and type and term reconstruction in the current implementation of Elf and has shown itself to be practical
Keywords
formal logic; logic programming; Elf; anti-instances; anti-unification; calculus of constructions; free variables; logic program execution; term reconstruction; unification algorithm; Artificial intelligence; Calculus; Computer languages; Computer science; Internet; Logic programming; Terminology;
fLanguage
English
Publisher
ieee
Conference_Titel
Logic in Computer Science, 1991. LICS '91., Proceedings of Sixth Annual IEEE Symposium on
Conference_Location
Amsterdam
Print_ISBN
0-8186-2230-X
Type
conf
DOI
10.1109/LICS.1991.151632
Filename
151632
Link To Document