Title :
Unification and anti-unification in the calculus of constructions
Author_Institution :
Sch. of Comput. Sci., Carnegie Mellon Univ., Pittsburgh, PA, USA
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;
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
DOI :
10.1109/LICS.1991.151632
