Abstract
We provide a complete system of transformation rules for semantic unification with respect to theories defined by convergent rewrite systems. We show that this standard unification procedure, with slight modifications, can be used to solve the satisfiability problem in combinatory logic with a convergent set of algebraic axioms R, thus resulting in a complete higher-order unification procedure for R. Furthermore, we use the system of transformation rules to provide a syntactic characterization for R which results in decidability of semantic unification.
Cite
CITATION STYLE
Dershowitz, N., & Mitra, S. (1993). Higher-order and semantic unification. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 761 LNCS, pp. 139–150). Springer Verlag. https://doi.org/10.1007/3-540-57529-4_49
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
