A Natural Proof System Based on Rewriting Techniques

  • Deepak Kapur
  • Balakrishnan Krishnamurthy
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 170)


Theorem proving procedures for the propositional calculus have traditionally relied on syntactic manipulations of the formula to derive a proof. In particular, clausal theorem provers sometimes lose some of the obvious semantics present in the theorem, in the process of converting the theorem into an unnatural normal form. Most existing propositional theorem provers do not incorporate substitution of equals for equals as an inference rule. In this paper we develop a “natural” proof system for the propositional calculus, with the goal that most succinct mathematical proofs should be encodable as short formal proofs within the proof system.

The main distinctive features of NPS are:
  1. 1.

    The substitution principle for the equivalence connective is incorporated as an inference rule.

  2. 2.

    A limited version of the powerful ideas of extension, originally suggested by Tseitin, are exploited. Extension allows the introduction of auxiliary variables to stand for intermediate sub-formulas in the course of a proof.

  3. 3.

    Formulas are standardized by converting them into a normal form, while at the same time preserving the explicit semantics inherent in the formula.

  4. 4.

    A generalization of the semantic tree approach is used to perform case analysis on literals as well as sub-formulas.

  5. 5.

    Additional enhancements such as a generalization of resolution are suggested.


We show that from a complexity theoretic viewpoint NPS is at least as powerful as the resolution procedure. We further demonstrate formulas on which NPS fares better than resolution. Finally, since proofs in NPS usually resemble manual proofs, we feel that NPS is easily amenable to an interactive theorem prover.


Inference Rule Propositional Calculus Theorem Prove Proof System Conjunctive Normal Form 
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. [1]
    S.K. Abdali and D.R. Musser, “A Proof Method based on Sequents and Unification,” Unpublished Manuscript (1982), G.E. R and D Center, Schenectady, NY.Google Scholar
  2. [2]
    W. Bibel, “Tautology Testing with a Generalized Matrix Reduction Method,” Theoretical Computer Science, 8 (1979), pp.31–44.MathSciNetCrossRefzbMATHGoogle Scholar
  3. [3]
    C-L Chang and R.C. Lee, Symbolic Logic and Mechanical Theorem Proving. Academic Press (1973), New York.Google Scholar
  4. [4]
    S. A. Cook and R. A. Reckhow, “The Relative Efficiency of Propositional Proof Systems,” J. of Symbolic Logic, 44 (1979), pp. 36–50.MathSciNetCrossRefzbMATHGoogle Scholar
  5. [5]
    J. Hsiang, Topics in Automated Theorem Proving and Program Generation. Ph.D. Thesis, Department of Computer Science, University of Illinois, Urbana, Illinois.Google Scholar
  6. [6]
    J. Hsiang and N. Dershowitz, “Rewrite Methods for Clausal and Non-clausal Theorem Proving,” Proc. 10th EATCS Intl. Collq. on Automata, Languages, and Programming, (1983), Spain.Google Scholar
  7. [7]
    S.C. Kleene, An Introduction to Metamathematics. (1952), Van Nostrand, New York.zbMATHGoogle Scholar
  8. [8]
    R. Kowalski and P. Hayes, “Semantic Trees in Automatic Theorem Proving,” in Machine Intelligence 4, Meltzer and Michie, eds., Edinburgh Univ. Press, Edinburgh.Google Scholar
  9. [9]
    B. Krishnamurthy, “Short Proofs for Tricky Formulas,” Unpublished Manuscript, (1982), G.E. R and D Center, Schenectady, NY.zbMATHGoogle Scholar
  10. [10]
    B. Krishnamurthy and R. N. Moll, “Examples of Hard Tautologies in the Propositional Calculus,” Proc. of the Thirteenth ACM Symp. on Th. of Computing, (1981), pp. 28–37.Google Scholar
  11. [11]
    B. Monien and E. Speckenmeyer, “3-Satisfiability is Testable in O(1.62r) Steps,” Bericht Nr. 3/1979 (1979), GH Paderborn, Fachbereich Mathematik-Informatik.Google Scholar
  12. [12]
    J.A. Robinson, “A Machine Oriented Logic Based on the Resolution Principle,” JACM, 12 (1965), pp. 23–41.MathSciNetCrossRefzbMATHGoogle Scholar
  13. [13]
    G. S. Tseitin, “On the Complexity of Derivations in Propositional Calculus,” Structures in Constructive Mathematics and Mathematical Logic, Part II, A. O. Sliosenko, ed., (1968), pp. 115–125.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1984

Authors and Affiliations

  • Deepak Kapur
    • 1
  • Balakrishnan Krishnamurthy
    • 1
  1. 1.Computer Science BranchGeneral Electric Research and Development CenterSchenectady

Personalised recommendations