Gerald E. Peterson
- 1 COHN, P.M. Universal Algebra. Harper and Row, New York, 1965.Google Scholar
- 2 DERSHOWITZ, N, AND MANNA,Z Proving termination with multiset ordermgs. Commun. ACM 22, 8(Aug 1979), 465-476. Google Scholar
- 3 EVANS, T. On multiphcatwe systems defined by generators and relaUons. I. Normal form theorems. Proc. Cambridge Phd. Soc 47 (1951), 637-649.Google Scholar
- 4 HINDLEY, R. An abstract Church-Rosser theorem, ii Apphcattons. J Symbohc Logzc 39 (1974), 1-21.Google Scholar
- 5 HUET, G. Umficatlon m typed lambda calculus, in h Calculus and Computer Science Theory, Lecture Notes m Computer Science 37, Springer Verlag, Heidelberg, 1975, pp 192-212. Google Scholar
- 6 HUET,G. Unification dans des langages d'ordre 1, 2 .. w These d'Etat, Universit6 Pans VI, 1976.Google Scholar
- 7 HUET, G Confluent reductions. Abstract properties and apphcations to term rewriting systems J A CM 27, 4(Oct 1980), 797-821 Google Scholar
- 8 HUET, G., AND OPPEN, D C Equations and rewrite rules. Tech Rep. CSL-II, SRI International, Menlo Park, Cahf, 1980. Google Scholar
- 9 KNUTH, D.E., AND BENDIX, P.B.Simple word problems in umversal algebras. In Computational Problems m Abstract Algebras, J Leech, Ed, Pergammon Press, 1970, pp. 263-297.Google Scholar
- 10 LANKFORD, D S. Canomcal algebraic slmphficatlon m computaUonal logic Tech. Rep, Mathemaucs Dep, Unlv of Texas, Austin, Texas, May 1975Google Scholar
- 11 LANKFORD, D S Canonical reference Tech. Rep., Mathemaucs Dep., Umv of Texas, Austin, Texas, Dec. 1975Google Scholar
- 12 LANKFORD, D S A umficatlon algorithm for Abehan group theory Tech Rep., Mathematics Dep, Lomslana Tech Umv, Ruston, La, January 1979.Google Scholar
- 13 LANKFORD, D.S On proving term rewriting systems are noethenan. Tech Pep., Mathematics Dep, Louisiana Tech Umv, Ruston, La., May 1979Google Scholar
- 14 LANKFORD, D.S, AND BALLANTYNE, A.M. Decision procedures for simple equational theories wRh a commutative axiom. Complete sets of commutative reductions Tech Rep., Mathematics Dep., Univ. of Texas, Austin, Texas, March 1977Google Scholar
- 15 LANK_FORD, D.S, AND BALLANTYNE, A M Decision procedures for simple equational theories with permutattve axioms: Complete sets of permutative reductions. Tech Rep, Mathematics Dep., Univ of Texas, Austin, Texas, April 1977Google Scholar
- 16 LANKFORD, D S, AND BALLANTYNE, A.M.Decision procedures for simple equational theories with commutatwe-associative axioms. Complete sets of commutative-associative reductions. Tech. Rep, Mathematics Dep., Umv. of Texas, Austin, Texas, Aug 1977Google Scholar
- 17 LIVESEY, M., AND SIEKMANN, J Termination and decidability results for string-unification Memo CSM-12, Essex Univ. Computing Center, Colchester, Essex, England, Aug. 1975.Google Scholar
- 18 LIVESEY, M, AND SIEKMANN, J.Umficatlon of A+C-terms (bags) and A+C+l-terms (sets) Interner Bencht Nr 5/76, lnstitut fur Informatik I, Umversltat Karlsruhe, Karlsruhe, W. Germany, 1976Google Scholar
- 19 MANNA, Z Mathemat, cal Theory of Computatmn McGraw-Hill, New York, 1974. Google Scholar
- 20 NEWMAN, M.H.A On theories w~th a combinatorial defmmon of "equivalence." Ann. Math 43 (1942), 223-243.Google Scholar
- 21 PLOTKIN, G.D.Buddmg-m equational theories. Machine intelhgence 7, B. Meltzer and D Mlchle, Eds., Halsted Press, 1972, pp. 73-90.Google Scholar
- 22 QUINE, W.V.The problem of stmphfymg truth funcnons Am. Math Monthly 59, 8 (Oct. 1952), 521-531Google Scholar
- 23 RAULEFS, P, SIEKMANN, J., SZABO, P., AND UNVERICHT, E A short survey on the state of the art m matchmg and umficatmn problems SIGSAM Bulletin 13, 2 (May 1979), 14-20 Google Scholar
- 24 ROBINSON, J A A machine-oriented logic based on the resolutmn pnnclple J A CM 12, 1 (Jan 1965), 23-41. Google Scholar
- 25 ROSEN, B K Tree-mampulatmg systems and Church-Rosser theorems. J ACM 20, 1 (Jan. 1973), 160-187. Google Scholar
- 26 SIEKMANN, J Stnng-umfication, part I Essex University, Colchester, Essex, England, March 1975Google Scholar
- 27 SIEKMANN,T-umficatton, part i Umficatton of commutative terms. Interner Bencht Nr 4/76, Instttut fur Informatik I, Umvers~tat Karlsruhe, Karlsruhe, W Germany, 1976Google Scholar
- 28 SLAGLE, J R Automated theorem-proving for theories with stmphfiers, commutattvtty, and assoctatwity. J ACM 21, 4 (Oct 1974), 622-642 Google Scholar
- 29 STICK.EL, M.E. A complete umficatlon algorithm for associative-commutative funct,ons. Advance Papers 4th Int. Jomt Conf on Amficlal Intelhgence, Tbihsi, U.S.S.R., 1975, pp. 71-76 To appear in J ACM.Google Scholar
- 30 STICKEL, M.E.Mechanical theorem proving and artificial intelhgence languages. Ph.D. Dlss., Carnegie-Mellon Onw., Pittsburgh, Pa, 1977. Google Scholar
- 31 MAKANIN, G.S.The problem of solvability of equations in a free semigroup. Soviet Akad. Nauk SSSR 233, 2 (1977).Google Scholar
Index Terms
- Complete Sets of Reductions for Some Equational Theories
Recommendations
Sound and Complete Equational Reasoning over Comodels
Comodels of Lawvere theories, i.e. models in Setop, model state spaces with algebraic access operations. Standard equational reasoning is known to be sound but incomplete for comodels. We give two sound and complete calculi for equational reasoning over ...
Oriented Equational Logic Programming is Complete
We show the completeness of an extension of SLD-resolution to the equational setting. This proves a conjecture of Laurent Fribourg and shows the completeness of an implementation of his. It is the first completeness result for superposition of ...
Single Versus Simultaneous Equational Unification and Equational Unification for Variable-Permuting Theories
A clear distinction is made between the (elementary) unification problem where there is only one pair of terms to be unified, and the simultaneous unification problem, where many such pairs have to be unified simultaneously – it is shown that there ...
Comments