Abstract
A method based on superposition on maximal literals in clauses and conditional rewriting is discussed for automatically proving theorems in first-order predicate calculus with equality. First-order formulae (clauses) are represented as conditional rewrite rules which turn out to be an efficient representation. The use of conditional rewriting for reducing search space is discussed. The method has been implemented in RRL, a Rewrite Rule Laboratory, a theorem proving environment based on rewriting techniques. It has been tried on a number of examples with considerable success. Its performance on bench-mark examples, including Schubert's Steamroller problem, SAM's lemma, and examples from set theory, compared favorably with the performance of other methods reported in the literature.
Partially supported by the National Science Foundation Grant no. CCR-8408461.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Bachmair, L., Dershowitz, N., and Hsiang, J., “Orderings for equational proofs,” Proc. IEEE Symp. Logic in Computer Science, Cambridge, MA, 336–357, 1986.
Bachmair, L., and Dershowitz, N., “Inference rules for rewrite-based first-order theorem proving,” Proc. IEEE Symp. Logic in Computer Science, Ithaca, New York, 1987.
Boyer, R.S., Locking: A restriction of resolution. Ph.D. Thesis, University of Texas, Austin, 1971.
Boyer, R.S. and Moore, J.S., A computational logic. Academic Press, New York, 1979.
Brand, D., Darringer, J.A., and Joyner, W.H., Completeness of conditional reductions. Research Report RC 7404 IBM, 1978.
Buchberger, B., “History and basic feature of the critical-pair/completion procedure,” Rewriting Techniques and Applications, Lect. Notes in Comp. Sci., Vol. 202, Springer-Verlag, Berlin, 301–324, 1985.
Chang, C-L. and Lee, R.C., Symbolic logic and mechanical theorem proving. Academic Press, New York, 1973.
Dershowitz, N., “Termination of rewriting,” J. of Symbolic Computation Vol. 3, 1987, 69–116.
Drosten K. Toward executable specifications using conditional axioms. Report 83-01, t.U. Braunschweig, 1983.
Fribourg, L., “A superposition oriented theorem prover” Theoretical Computer Science, Vol. 35, 129–164, 1985.
Fribourg, L., “SLOG: A logic programming language interpreter based on clausal superposition and rewriting,” In Proc. 1985 Intl. Symposium on Logic Programming, pp. 172–184, Boston, 1985.
Hsiang, J., Topics in automated theorem proving and program generation. Ph.D. Thesis, UIUCDCS-R-82-1113, Univ. of Illinois, Urbana-Champaigne, 1982.
Hsiang, J., “Rewrite method for theorem proving in first order theory with equality,” J. Symbolics Computation, Vol. 3, 133–151, 1987.
Hsiang, J., and Rusinowitch, M., “A new method for establishing refutational completeness in theorem proving,” Proc. 8th Conf. on Automated Deduction, LNCS No. 230, Springer-Verlag, 141–152, 1986.
Huet, G. and Oppen, D., “Equations and rewrite rules: a survey,” in: Formal languages: Perspectives and open problems. (R. Book, ed.), Academic Press, New York, 1980.
Kaplan S., Fair conditional term rewriting systems: unification, termination and confluence. LRI, Orsay, 1984.
Kapur, D. and Narendran, P., “An equational approach to theorem proving in first-order predicate calculus,” 9th IJCAI, Los Angeles, CA, August 1985.
Kapur, D., Sivakumar, G., and Zhang, H., “RRL: A Rewrite Rule Laboratory,” Proc. 8th Intl Conf. on Automated Deduction (CADE-8), Oxford, U.K., LNCS 230, Springer-Verlag, 1986.
Knuth, D., and Bendix, P., “Simple Word Problems in Universal Algebras,” in: Computational problems in abstract algebra. (Leech, ed.) Pergamon Press, 263–297, 1970.
Kowalski, R., and Hayes, P., “Semantic trees in automatic theorem proving,” in Machine Intelligence, Vol. 5, (Meltzer, B. and Michie, D., eds.) American Elsevier, 1969.
Lankford, D.S., Canonical inference. Report ATP-32, Dept. of Mathematics and Computer Sciences, Univ. of Texas, Austin, Texas, 1975.
Lankford, D.S., and Ballantyne, A.M., Decision procedures for simple equational theories with commutative-associative axioms: Complete sets of commutative-associative reductions. Memo ATP-39, Department of Mathematics and Computer Sciences, University of Texas, Austin, TX, August 1977.
Lankford, D.S., and Ballantyne, A.M., “The refutational completeness of blocked permutative narrowing and resolution,” 4th Conf. on Automated Deduction, Austin, Texas, 1979.
Lankford, D.S., Some new approaches to the theory and applications of conditional term rewriting systems. Report MTP-6, Math. Dept., Lousiana Tech. University, 1979.
Pelletier F.J., “Seventy-five problems for testing automatic theorem provers,” J. of Automated reasoning Vol. 2, 191–216, 1986.
Pletat, U., Engels, G., and Ehrich, H.D., “Operational semantics of algebraic specifications with conditional equations,” 7th, CAAP '82, LNCS, Springer-Verlag, 1982.
Reiter, R., “Two results on ordering fro resolution with merging and linear format,” JACM, 630–646, 1971.
Remy, J.L., Etudes des systemes reecriture conditionnelles et applications aux types abstraits algebriques. These d'etat, Universite Nancy I, 1982.
Peterson, G.E., “A technique for establishing completeness results in theorem proving with equality,” SIAM J. Computing Vol. 12, No. 1. 82–99, 1983.
Peterson, G.L., and Stickel, M.E., “Complete sets of reductions for some equational theories,” JACM Vol. 28 No. 2, 233–264, 1981.
Stickel, M.E., “Automated deduction by theory resolution,” J. of Automated Reasoning Vol. 1, 333–355, 1985.
Walther, C., “A mechanical solution of Schubert's steamroller by many-sorted resolution,” Proc. of the AAAI-84 National Conf. on Artificial Intelligence, Austin, Texas, 330–334, 1984.
Wos, L.R., and Robinson, G., “Paramodulation and set of support,” Proc. IRIA Symposium on Automatic Demonstration, Versailles, France, 1968, Springer-Verlag, Berlin, 276–310, 1970.
Zhang, H., Reveur 4: Etude et Mise en Oeuvre de la Reecriture Conditionelle. Thesis of "Doctorat de 3me cycle", Universite de Nancy I, France, 1984.
Zhang, H., and Remy, J.L., “Contextual rewriting,” Proc. of rewriting techniques and application, Dijon, France, 1985.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1988 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zhang, H., Kapur, D. (1988). First-order theorem proving using conditional rewrite rules. In: Lusk, E., Overbeek, R. (eds) 9th International Conference on Automated Deduction. CADE 1988. Lecture Notes in Computer Science, vol 310. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0012820
Download citation
DOI: https://doi.org/10.1007/BFb0012820
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-19343-2
Online ISBN: 978-3-540-39216-3
eBook Packages: Springer Book Archive