Complete Sets of Reductions for Some Equational Theories

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Complete Sets of Reductions for Some Equational Theories

Full text

Pdf (1.93 MB)

Source

Journal of the ACM (JACM) archive
Volume 28 , Issue 2 (April 1981) table of contents

Pages: 233 - 264

Year of Publication: 1981

ISSN:0004-5411

Authors

Gerald E. Peterson	Department of Mathematical Sciences, University of Missouri, 8001 Natural Bridge Road, St. Lotus, MO
Mark E. Stickel	RCA David Sarnoff Research Center, Princeton, NJ

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 2, Downloads (12 Months): 50, Citation Count: 40

Additional Information:

references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/322248.322251 What is a DOI?

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	COHN, P.M. Universal Algebra. Harper and Row, New York, 1965.
	2	Nachum Dershowitz , Zohar Manna, Proving termination with multiset orderings, Communications of the ACM, v.22 n.8, p.465-476, Aug. 1979 [doi>10.1145/359138.359142]
	3	EVANS, T. On multiphcatwe systems defined by generators and relaUons. I. Normal form theorems. Proc. Cambridge Phd. Soc 47 (1951), 637-649.
	4	HINDLEY, R. An abstract Church-Rosser theorem, ii Apphcattons. J Symbohc Logzc 39 (1974), 1-21.
	5	Gérard P. Huet, unification in typed lambda calculus, Proceedings of the Symposium on Lambda-Calculus and Computer Science Theory, p.192-212, March 25-27, 1975
	6	HUET,G. Unification dans des langages d'ordre 1, 2 .... w These d'Etat, Universit6 Pans VI, 1976.
	7	Gérard Huet, Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems: Abstract Properties and Applications to Term Rewriting Systems, Journal of the ACM (JACM), v.27 n.4, p.797-821, Oct. 1980 [doi>10.1145/322217.322230]
	8	Gerard Huet , Derek C. Oppen, Equations and rewrite rules: a survey, Stanford University, Stanford, CA, 1980
	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.
	10	LANKFORD, D S. Canomcal algebraic slmphficatlon m computaUonal logic Tech. Rep, Mathemaucs Dep, Unlv of Texas, Austin, Texas, May 1975
	11	LANKFORD, D S Canonical reference Tech. Rep., Mathemaucs Dep., Umv of Texas, Austin, Texas, Dec. 1975
	12	LANKFORD, D S A umficatlon algorithm for Abehan group theory Tech Rep., Mathematics Dep, Lomslana Tech Umv, Ruston, La, January 1979.
	13	LANKFORD, D.S On proving term rewriting systems are noethenan. Tech Pep., Mathematics Dep, Louisiana Tech Umv, Ruston, La., May 1979
	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 1977
	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 1977
	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 1977
	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.
	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, 1976
	19	Zohar Manna, Introduction to Mathematical Theory of Computation, McGraw-Hill, Inc., New York, NY, 1974
	20	NEWMAN, M.H.A On theories w~th a combinatorial defmmon of "equivalence." Ann. Math 43 (1942), 223-243.
	21	PLOTKIN, G.D.Buddmg-m equational theories. Machine intelhgence 7, B. Meltzer and D Mlchle, Eds., Halsted Press, 1972, pp. 73-90.
	22	QUINE, W.V.The problem of stmphfymg truth funcnons Am. Math Monthly 59, 8 (Oct. 1952), 521-531
	23	P. Raulefs , J. Siekmann , P. Szabó , E. Unvericht, A short survey on the state of the art in matching and unification problems, ACM SIGSAM Bulletin, v.13 n.2, p.14-20, May 1979 [doi>10.1145/1089208.1089210]
	24	J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM (JACM), v.12 n.1, p.23-41, Jan. 1965 [doi>10.1145/321250.321253]
	25	Barry K. Rosen, Tree-Manipulating Systems and Church-Rosser Theorems, Journal of the ACM (JACM), v.20 n.1, p.160-187, Jan. 1973 [doi>10.1145/321738.321750]
	26	SIEKMANN, J Stnng-umfication, part I Essex University, Colchester, Essex, England, March 1975
	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, 1976
	28	James R. Slagle, Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity, Journal of the ACM (JACM), v.21 n.4, p.622-642, Oct. 1974 [doi>10.1145/321850.321859]
	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.
	30	Mark Edward Stickel, Mechanical theorem proving and artificial intelligence languages., 1977
	31	MAKANIN, G.S.The problem of solvability of equations in a free semigroup. Soviet Akad. Nauk SSSR 233, 2 (1977).

CITED BY 40

	Jean-Pierre Jouannaud , Helene Kirchner, Completion of a set of rules modulo a set of equations, Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.83-92, January 15-18, 1984, Salt Lake City, Utah, United States
	Mikael Rittri, Using types as search keys in function libraries, Proceedings of the fourth international conference on Functional programming languages and computer architecture, p.174-183, September 11-13, 1989, Imperial College, London, United Kingdom
	Timothy B. Baird , Ralph W. Wilkerson, Termination via conditional reductions, Proceedings of the 19th annual conference on Computer Science, p.53-60, April 1991, San Antonio, Texas, United States
	Tie-Cheng Wang, Z-module reasoning: an equality-oriented proving method with built-in ring axioms, Journal of the ACM (JACM), v.40 n.3, p.558-606, July 1993
	Mark E. Stickel, A Unification Algorithm for Associative-Commutative Functions, Journal of the ACM (JACM), v.28 n.3, p.423-434, July 1981
	Ralph W. Wilkerson , Blayne E. Mayfield, The role of term symmetry in E-completion procedures, Proceedings of the 1990 ACM annual conference on Cooperation, p.134-139, February 20-22, 1990, Washington, D.C., United States
	Reinhard Bündgen, Completion of integral polynomials by AC-term completion, Proceedings of the 1991 international symposium on Symbolic and algebraic computation, p.70-78, July 15-17, 1991, Bonn, West Germany
	F. Winkler, Knuth-Bendix procedure and Buchberger algorithm: a synthesis, Proceedings of the ACM-SIGSAM 1989 international symposium on Symbolic and algebraic computation, p.55-67, July 17-19, 1989, Portland, Oregon, United States
	Wray L. Buntine , Hans-Jürgen Bürckert, On solving equations and disequations, Journal of the ACM (JACM), v.41 n.4, p.591-629, July 1994
	Leo Bachmair , Nachum Dershowitz, Equational inference, canonical proofs, and proof orderings, Journal of the ACM (JACM), v.41 n.2, p.236-276, March 1994
	Uwe Waldmann, Cancellative abelian monoids and related structures in refutational theorem proving (Part I), Journal of Symbolic Computation, v.33 n.6, p.777-829, June 2002
	Peter Borovanský , Claude Kirchner , Hélène Kirchner , Pierre-Etienne Moreau, ELAN from a rewriting logic point of view, Theoretical Computer Science, v.285 n.2, p.155-185, 28 August 2002
	J. Avenhaus , Th. Hillenbrand , B. Löchner, On using ground joinable equations in equational theorem proving, Journal of Symbolic Computation, v.36 n.1-2, p.217-233, July 2003
	Johannes Grabmeier , Erich Kaltofen , Volker Weispfenning, Cited References, Computer algebra handbook, Springer-Verlag New York, Inc., New York, NY, 2003
	C. Kirchner , H. Kirchner, Constrained equational reasoning, Proceedings of the ACM-SIGSAM 1989 international symposium on Symbolic and algebraic computation, p.382-389, July 17-19, 1989, Portland, Oregon, United States
	Patrick Viry, Equational rules for rewriting logic, Theoretical Computer Science, v.285 n.2, p.487-517, 28 August 2002
	Guillem Godoy , Robert Nieuwenhuis, Superposition with completely built-in Abelian groups, Journal of Symbolic Computation, v.37 n.1, p.1-33, January 2004
	Henrik Linnestad, Fatal steps of Knuth-Bendix completion, Nordic Journal of Computing, v.3 n.2, p.131-143, Summer 1996
	Venkatesh Choppella , Christopher T. Haynes, Source-tracking unification, Information and Computation, v.201 n.2, p.121-159, September 15, 2005
	S. J. Garland , J. V. Guttag , J. J. Horning, Debugging Larch Shared Language Specifications, IEEE Transactions on Software Engineering, v.16 n.9, p.1044-1057, September 1990
	Paolo Baldan , Clara Bertolissi , Horatiu Cirstea , Claude Kirchner, A rewriting calculus for cyclic higher-order term graphs, Mathematical Structures in Computer Science, v.17 n.3, p.363-406, June 2007
	Leo Bachmair , Ashish Tiwari , Laurent Vigneron, Abstract Congruence Closure, Journal of Automated Reasoning, v.31 n.2, p.129-168, 2003
	Gilles Dowek , Therese Hardin , Claude Kirchner, HOL-λσ: an intentional first-order expression of higher-order logic, Mathematical Structures in Computer Science, v.11 n.1, p.21-45, February 2001
	Nachum Dershowitz , Claude Kirchner, Abstract canonical presentations, Theoretical Computer Science, v.357 n.1, p.53-69, 25 July 2006
	Maria Paola Bonacina , Nachum Dershowitz, Abstract canonical inference, ACM Transactions on Computational Logic (TOCL), v.8 n.1, p.6-es, January 2007
	Marc Aiguier , Diane Bahrami, Structures for Abstract Rewriting, Journal of Automated Reasoning, v.38 n.4, p.303-351, May 2007
	Bernd Löchner , Thomas Hillenbrand, A phytography of WALDMEISTER, AI Communications, v.15 n.2,3, p.127-133, August 2002
	Frédéric Blanqui, Definitions by rewriting in the Calculus of Constructions, Mathematical Structures in Computer Science, v.15 n.1, p.37-92, February 2005
	Hélène Kirchner , Pierre-Etienne Moreau, Promoting rewriting to a programming language: a compiler for non-deterministic rewrite programs in associative-commutative theories, Journal of Functional Programming, v.11 n.2, p.207-251, March 2001
	Gilles Dowek , Thérèse Hardin , Claude Kirchner, Theorem Proving Modulo, Journal of Automated Reasoning, v.31 n.1, p.33-72, 2003
	Quang Huy Nguyen , Claude Kirchner , Hélène Kirchner, External Rewriting for Skeptical Proof Assistants, Journal of Automated Reasoning, v.29 n.3-4, p.309-336, 2002
	P. Baldan , C. Bertolissi , H. Cirstea , C. Kirchner, Towards a Sharing Strategy for the Graph Rewriting Calculus, Electronic Notes in Theoretical Computer Science (ENTCS), 204, p.111-127, April, 2008
	Stephan Falke , Deepak Kapur, Operational Termination of Conditional Rewriting with Built-in Numbers and Semantic Data Structures, Electronic Notes in Theoretical Computer Science (ENTCS), 237, p.75-90, April, 2009
	Santiago Escobar , José Meseguer , Ralf Sasse, Variant Narrowing and Equational Unification, Electronic Notes in Theoretical Computer Science (ENTCS), v.238 n.3, p.103-119, June, 2009
	Jean-Pierre Jouannaud , Helene Kirchner , Jean-Luc Remy, Church-rosser properties of weakly terminating term rewriting systems, Proceedings of the Eighth international joint conference on Artificial intelligence, p.909-915, August 08-12, 1983, Karlsruhe, West Germany
	Nachum Dershowitz , Jien Hsiang , N. Alan Josephson , David A. Plaisted, Associative-commutative rewriting, Proceedings of the Eighth international joint conference on Artificial intelligence, p.940-944, August 08-12, 1983, Karlsruhe, West Germany
	K. Blasius , N. Fisinger , J. Siekmann , G. Smolka , A. Herold , C. Walther, The Markgraf Karl refutation procedure, Proceedings of the 7th international joint conference on Artificial intelligence, p.511-518, August 24-28, 1981, Vancouver, BC, Canada
	Deepak Kapur , Paliath Narendran, An equational approach to theorem proving in first-order predicate calculus, Proceedings of the 9th international joint conference on Artificial intelligence, p.1146-1153, August 18-23, 1985, Los Angeles, California
	David A. Plaisted , Yunshan Zhu, Equational reasoning using AC constraints, Proceedings of the 15th international joint conference on Artifical intelligence, p.108-113, August 23-29, 1997, Nagoya, Japan
	Nachum Dershowitz, Synthesis by completion, Proceedings of the 9th international joint conference on Artificial intelligence, p.208-214, August 18-23, 1985, Los Angeles, California