Rewrite methods for clausal and non-clausal theorem proving

  • Jieh Hsiang
  • Nachum Dershowitz
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 154)


Effective theorem provers are essential for automatic verification and generation of programs. The conventional resolution strategies, albeit complete, are inefficient. On the other hand, special purpose methods, such as term rewriting systems for solving word problems, are relatively efficient but applicable to only limited classes of problems.

In this paper, a simple canonical set of rewrite rules for Boolean algebra is presented. Based on this set of rules, the notion of term rewriting systems is generalized to provide complete proof strategies for first order predicate calculus. The methods are conceptually simple and can frequently utilize lemmas in proofs. Moreover, when the variables of the predicates involve some domain that has a canonical system, that system can be incorporated as rewrite rules, with the algebraic simplifications being done simultaneously with the merging of clauses. This feature is particularly useful in program verification, data type specification, and programming language design, where axioms can be expressed as equations (rewrite rules). Preliminary results from our implementation indicate that the methods are space-efficient with respect to the number of rules generated (as compared to the number of resolvents in resolution provers).


Boolean Algebra Theorem Prove Unification Algorithm Critical Pair Natural Deduction 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [Br75]
    Brand, D., Proving theorems with the modification method. SIAM J. of Computing, Vol 4, 1975.Google Scholar
  2. [Co71]
    Cook, S.A., The complexity of theorem-proving procedures. 3rd. ACM Symp. on Theory of Computing, pp151–158, 1971.Google Scholar
  3. [GrNaOrPl82]
    Greenbaum, S., Nagasaka, A., O'Rorke, P., Plaisted, D., Comparison of natural deduction and locking resolution implementations. 6th Conf. on Automated Deduction, Lecture Notes in CS, No. 138, 1982.Google Scholar
  4. [Hs82]
    Hsiang, J., Topics in automated theorem proving and program generation. Ph.D. Thesis, U. of Illinois at Urbana-Champaign, 1982.Google Scholar
  5. [HsJo82]
    Hsiang, J. & Josephson, N.A., A term rewriting theorem prover. Unpublished manuscript, 1982.Google Scholar
  6. [Hul80]
    Hullot, J.-M., A catalogue of canonical term rewriting systems. Report CSL-113, SRI International, 1980.Google Scholar
  7. [HuHu80]
    Huet, G. & Hullot, J.-M., Proofs by induction in equational theories with constructors. 21st FOCS, 1980.Google Scholar
  8. [KnBe70]
    Knuth, D.E. & Bendix, P.B., Simple word problems in universal algebra. Computational Problems in Abstract Algebra, J. Leech Ed. Pergamon Press, Oxford, 1970.Google Scholar
  9. [KoHa69]
    Kowalski, R. & Hayes, P., Semantic trees in automatic theorem proving. Machine Intelligence 4 Meltzer & Michie eds. pp87–101, 1969.Google Scholar
  10. [La75]
    Lankford, D.S., Canonical inference. Report ATP-32, Univ. of Texas at Austin, 1975.Google Scholar
  11. [LaBa77]
    Lankford, D.S. & Ballantyne, A.M., Decision procedure for simple equational theories with commutative-associative axioms. Report ATP-39, Univ. of Texas at Austin, 1977.Google Scholar
  12. [LaBa79]
    Lankford, D.S. & Ballantyne, A.M., The refutation completeness of blocked permutative narrowing and resolution. 4th Conf. on Automated Deduction, 1979.Google Scholar
  13. [PeSt81]
    Peterson, G.E. & Stickel, M.E., Complete sets of reductions for some equational theories. J.ACM Vol 28, pp233–264, 1981.Google Scholar
  14. [Pl73]
    Plotkin, G., Building in equational theories. Machine Intelligence 7 Meltzer & Michie Eds., pp73–90Google Scholar
  15. [Ro65]
    Robinson, J.A., A machine oriented logic based on resolution principle. J.ACM Vol 12, pp23–41, 1965.Google Scholar
  16. [Sl74]
    Slagle, J., Automated theorem proving with simplifiers, commutativity, associativity. J.ACM Vol 21, pp622–642, 1974.Google Scholar
  17. [SlNo73]
    Slagle, J. & Norton, Experiments with an automatic theorem prover having partial ordering inference rules. C.ACM Vol 16, pp682–688, 1973.Google Scholar
  18. [St81]
    Stickel, M.E., A unification algorithm for associative-commutative functions. J.ACM Vol 28, pp233–264, 1981.Google Scholar
  19. [St36]
    Stone, M., The theory of representations for Boolean algebra. Trans. AMS Vol 40, pp37–111, 1936.Google Scholar
  20. [WaCo80]
    Watts, D.E. & Cohen, J.K., Computer implemented set theory. American Mathematical Monthly, Vol 87, No. 7, pp557–560.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1983

Authors and Affiliations

  • Jieh Hsiang
    • 1
  • Nachum Dershowitz
    • 2
  1. 1.Department of Computer ScienceState University of New York at Stony BrookStony BrookUSA
  2. 2.Department of Computer ScienceUniversity of Illinois at Urbana-ChampaignUrbanaUSA

Personalised recommendations