An algorithm for reasoning about equality

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

An algorithm for reasoning about equality

Full text

Pdf (303 KB)

Source

Communications of the ACM archive
Volume 21 , Issue 7 (July 1978) table of contents

Pages: 583 - 585

Year of Publication: 1978

ISSN:0001-0782

Author

Robert E. Shostak

Stanford Research Institute, Menlo Park, CA

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 5, Downloads (12 Months): 34, Citation Count: 19

Additional Information:

abstract 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/359545.359570 What is a DOI?

ABSTRACT

A simple technique for reasoning about equalities that is fast and complete for ground formulas with function symbols and equality is presented. A proof of correctness is given as well.

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	Ackermann, W. Solvable Cases of the Decision Problem, North- Holland Publishing Co., Amsterdam, 1954, pp. 102-103.
	2	Elliott Mendelson, Introduction to mathematical logic (3rd ed.), Wadsworth Publ. Co., Belmont, CA, 1987
	3	Oppen, D., and Nelson, G. Fast Decision Algorithms Based on Union and Find. Proceedings of 8th Symposium on Foundations of Computer Science, Princeton, N.J., Nov. 1977.
	4	Robinson, G., and Wos, L. Paramodulation and Theorem- Proving in First-order Theories with Equality. Machine Intelligence 4, D. Michie and B. Meltzer, Eds., American Elsivier, N.Y., 1969 pp. 135-150.
	5	Robert Endre Tarjan, Efficiency of a Good But Not Linear Set Union Algorithm, Journal of the ACM (JACM), v.22 n.2, p.215-225, April 1975 [doi>10.1145/321879.321884]

CITED BY 19

	Greg Nelson , Derek C. Oppen, Fast Decision Procedures Based on Congruence Closure, Journal of the ACM (JACM), v.27 n.2, p.356-364, April 1980
	Robert E. Shostak, Deciding Combinations of Theories, Journal of the ACM (JACM), v.31 n.1, p.1-12, Jan. 1984
	Christoph M. Hoffmann , Michael J. O'Donnell, Pattern Matching in Trees, Journal of the ACM (JACM), v.29 n.1, p.68-95, Jan. 1982
	Peter J. Downey , Ravi Sethi , Robert Endre Tarjan, Variations on the Common Subexpression Problem, Journal of the ACM (JACM), v.27 n.4, p.758-771, Oct. 1980
	David McAllester, On the complexity analysis of static analyses, Journal of the ACM (JACM), v.49 n.4, p.512-537, July 2002
	David A. McAllester, Automatic recognition of tractability in inference relations, Journal of the ACM (JACM), v.40 n.2, p.284-303, April 1993
	John Rushby, Theorem proving for verification, Modeling and verification of parallel processes, Springer-Verlag New York, Inc., New York, NY, 2001
	Nicolas Peltier, Constructing decision procedures in equational clausal logic, Fundamenta Informaticae, v.54 n.1, p.17-65, January 2003
	Robert Givan , David Mcallester, Polynomial-time computation via local inference relations, ACM Transactions on Computational Logic (TOCL), v.3 n.4, p.521-541, October 2002
	Vincent J. Digricoli , Malcolm C. Harrison, Equality-based binary resolution, Journal of the ACM (JACM), v.33 n.2, p.253-289, April 1986
	Steven Eker , Narciso Martí-Oliet , José Meseguer , Alberto Verdejo, Deduction, Strategies, and Rewriting, Electronic Notes in Theoretical Computer Science (ENTCS), v.174 n.11, p.3-25, July, 2007
	Robert Nieuwenhuis , Albert Oliveras, Fast congruence closure and extensions, Information and Computation, v.205 n.4, p.557-580, April, 2007
	Y. André , A. C. Caron , D. Debarbieux , Y. Roos , S. Tison, Path constraints in semistructured data, Theoretical Computer Science, v.385 n.1-3, p.11-33, October, 2007
	Anatoli Degtyarev , Andrei Voronkov, What You Always Wanted to Know about Rigid E-Unification, Journal of Automated Reasoning, v.20 n.1-2, p.47-80, April 1998
	Alessandro Armando , Maria Paola Bonacina , Silvio Ranise , Stephan Schulz, New results on rewrite-based satisfiability procedures, ACM Transactions on Computational Logic (TOCL), v.10 n.1, p.1-51, January 2009
	Olga Tveretina , Wieger Wesselink, EufDpll - A Tool to Check Satisfiability of Equality Logic Formulas, Electronic Notes in Theoretical Computer Science (ENTCS), 225, p.405-420, January, 2009
	Rakesh Verma, Complexity of Normal Form Properties and Reductions for Term Rewriting Problems Complexity of Normal Form Properties and Reductions for Term Rewriting Problems, Fundamenta Informaticae, v.92 n.1-2, p.145-168, January 2009
	Karl-Hans Blasius, Equality reasoning in clause graphs, Proceedings of the Eighth international joint conference on Artificial intelligence, p.936-939, August 08-12, 1983, Karlsruhe, West Germany
	Vincent J. Digricoli, The management of heuristic search in boolean experiments with RUE resolution, Proceedings of the 9th international joint conference on Artificial intelligence, p.1154-1161, August 18-23, 1985, Los Angeles, California