Unification in combinations of collapse-free regular theories
DOI: 10.1016/S0747-7171(87)80025-1
关键词:
摘要: This paper presents a method for combining equational unification algorithms to handle terms containing 'mixed' sets of function symbols. For example, given one algorithm unifying associative-commutative operators, and another commutative our provides both kinds operators. As special case the problem, lifts variable-only general with multiple operator instances free We restrict attention class theories called collapse-free regular theories. give some results characterizing problem in this theories, specifically show restrictions are necessary sufficient correctness algorithm. An implementation has been done as part larger system reasoning about
elsevier.com
sci-hub.se 参考文章(34)
David A. Plaisted, Nachum Dershowitz, N. Alan Josephson, Jien Hsiang, Associative-commutative rewriting international joint conference on artificial intelligence. pp. 940- 944 ,(1983)
Claude Kirchner, Hélène Kirchner, Implementation of a General Completion Procedure Parameterized by Built-in Theories and Strategies european conference on computer algebra. pp. 402- 404 ,(1985) , 10.1007/3-540-15984-3_296
R. Forgaard, A PROGRAM FOR GENERATING AND ANALYZING TERM REWRITING SYSTEMS Massachusetts Institute of Technology. ,(1984)
Ronald V. Book, Formal language theory : perspectives and open problems Academic Press. ,(1980)
Jieh Hsiang, Nachum Dershowitz, Rewrite Methods for Clausal and Non-Clausal Theorem Proving international colloquium on automata, languages and programming. pp. 331- 346 ,(1983) , 10.1007/BFB0036919
Jean-Marie Hullot, Canonical forms and unification 5th Conference on Automated Deduction Les Arcs, France, July 8–11, 1980. pp. 318- 334 ,(1980) , 10.1007/3-540-10009-1_25
François Fages, Associative-Commutative Unification conference on automated deduction. pp. 194- 208 ,(1984) , 10.1007/978-0-387-34768-4_12
Robert A. Kowalski, Predicate Logic as Programming Language. ifip congress. pp. 569- 574 ,(1974)
Claude Kirchner, A New Equational Unification Method: A Generalization of Martelli-Montanari's Algorithm conference on automated deduction. pp. 224- 247 ,(1984) , 10.1007/978-0-387-34768-4_14
K. A. Yelick, A GENERALIZED APPROACH TO EQUATIONAL UNIFICATION Massachusetts Institute of Technology. ,(1985)