article

Free access

Complete Sets of Reductions for Some Equational Theories

Authors:

Gerald E. Peterson,

Mark E. StickelAuthors Info & Claims

Journal of the ACM (JACM), Volume 28, Issue 2

Pages 233 - 264

https://doi.org/10.1145/322248.322251

Published: 01 April 1981 Publication History

PDF eReader

References

[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.

Crossref

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.

Crossref

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

Crossref

Google Scholar

[8]

HUET, G., AND OPPEN, D C Equations and rewrite rules. Tech Rep. CSL-II, SRI International, Menlo Park, Cahf, 1980.

Crossref

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 1975

Google Scholar

[11]

LANKFORD, D S Canonical reference Tech. Rep., Mathemaucs Dep., Umv of Texas, Austin, Texas, Dec. 1975

Google 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 1979

Google 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 1977

Google 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 1977

Google 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 1977

Google 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, 1976

Google Scholar

[19]

MANNA, Z Mathemat, cal Theory of Computatmn McGraw-Hill, New York, 1974.

Crossref

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-531

Google 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

Crossref

Google Scholar

[24]

ROBINSON, J A A machine-oriented logic based on the resolutmn pnnclple J A CM 12, 1 (Jan 1965), 23-41.

Crossref

Google Scholar

[25]

ROSEN, B K Tree-mampulatmg systems and Church-Rosser theorems. J ACM 20, 1 (Jan. 1973), 160-187.

Crossref

Google Scholar

[26]

SIEKMANN, J Stnng-umfication, part I Essex University, Colchester, Essex, England, March 1975

Google 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, 1976

Google Scholar

[28]

SLAGLE, J R Automated theorem-proving for theories with stmphfiers, commutattvtty, and assoctatwity. J ACM 21, 4 (Oct 1974), 622-642

Crossref

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.

Crossref

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

Cited By

View all

Ringeissen CVigneron L(2024)Combined Abstract Congruence Closure for Theories with Associativity or CommutativityLogic-Based Program Synthesis and Transformation10.1007/978-3-031-71294-4_5(82-98)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1007/978-3-031-71294-4_5
Jouannaud J(2023)Confluence of Terminating Rewriting ComputationsThe French School of Programming10.1007/978-3-031-34518-0_11(265-306)Online publication date: 11-Oct-2023
https://doi.org/10.1007/978-3-031-34518-0_11
Bonchi FGadducci FKissinger ASobocinski PZanasi F(2022)String Diagram Rewrite Theory I: Rewriting with Frobenius StructureJournal of the ACM10.1145/350271969:2(1-58)Online publication date: 10-Mar-2022
https://dl.acm.org/doi/10.1145/3502719
Show More Cited By

Index Terms

Complete Sets of Reductions for Some Equational Theories
1. Mathematics of computing
  1. Discrete mathematics
2. Theory of computation
  1. Randomness, geometry and discrete structures

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

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

Journal of the ACM Volume 28, Issue 2

April 1981

229 pages

ISSN:0004-5411

EISSN:1557-735X

DOI:10.1145/322248

Issue’s Table of Contents

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 April 1981

Published in JACM Volume 28, Issue 2

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

332
Total Citations
View Citations
915
Total Downloads

Downloads (Last 12 months)123
Downloads (Last 6 weeks)12

Reflects downloads up to 04 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Ringeissen CVigneron L(2024)Combined Abstract Congruence Closure for Theories with Associativity or CommutativityLogic-Based Program Synthesis and Transformation10.1007/978-3-031-71294-4_5(82-98)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1007/978-3-031-71294-4_5
Jouannaud J(2023)Confluence of Terminating Rewriting ComputationsThe French School of Programming10.1007/978-3-031-34518-0_11(265-306)Online publication date: 11-Oct-2023
https://doi.org/10.1007/978-3-031-34518-0_11
Bonchi FGadducci FKissinger ASobocinski PZanasi F(2022)String Diagram Rewrite Theory I: Rewriting with Frobenius StructureJournal of the ACM10.1145/350271969:2(1-58)Online publication date: 10-Mar-2022
https://dl.acm.org/doi/10.1145/3502719
Dupont BMalbos P(2022)Coherent confluence modulo relations and double groupoidsJournal of Pure and Applied Algebra10.1016/j.jpaa.2022.107037226:10(107037)Online publication date: Oct-2022
https://doi.org/10.1016/j.jpaa.2022.107037
Eker S(2022)Associative unification in MaudeJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2021.100747126(100747)Online publication date: Apr-2022
https://doi.org/10.1016/j.jlamp.2021.100747
Liu YNicolescu RSun J(2022)Towards automated deduction in cP systemsInformation Sciences: an International Journal10.1016/j.ins.2021.12.035587:C(435-449)Online publication date: 1-Mar-2022
https://dl.acm.org/doi/10.1016/j.ins.2021.12.035
Bonacina M(2022)Set of Support, Demodulation, Paramodulation: A Historical PerspectiveJournal of Automated Reasoning10.1007/s10817-022-09628-066:4(463-497)Online publication date: 1-Nov-2022
https://dl.acm.org/doi/10.1007/s10817-022-09628-0
Meseguer JSkeirik S(2022)On Ground Convergence and Completeness of Conditional Equational Program HierarchiesRewriting Logic and Its Applications10.1007/978-3-031-12441-9_10(191-211)Online publication date: 2-Apr-2022
https://dl.acm.org/doi/10.1007/978-3-031-12441-9_10
Durán FEker SEscobar SMartí-Oliet NMeseguer JRubio RTalcott C(2022)Equational Unification and Matching, and Symbolic Reachability Analysis in Maude 3.2 (System Description)Automated Reasoning10.1007/978-3-031-10769-6_31(529-540)Online publication date: 8-Aug-2022
https://dl.acm.org/doi/10.1007/978-3-031-10769-6_31
Guilloud SKunčak V(2022)Equivalence Checking for Orthocomplemented Bisemilattices in Log-Linear TimeTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-030-99527-0_11(196-214)Online publication date: 2-Apr-2022
https://dl.acm.org/doi/10.1007/978-3-030-99527-0_11
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

References

Cited By

Index Terms

Recommendations

Sound and Complete Equational Reasoning over Comodels

Oriented Equational Logic Programming is Complete

Single Versus Simultaneous Equational Unification and Equational Unification for Variable-Permuting Theories

Comments

Information

Published In

Publisher

Publication History

Permissions

Check for updates

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

PDF

eReader

Login options

Full Access

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations