# A Natural Proof System Based on Rewriting Techniques

## Abstract

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.

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

- 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.
Formulas are standardized by converting them into a normal form, while at the same time preserving the explicit semantics inherent in the formula.

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

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

## Keywords

Inference Rule Propositional Calculus Theorem Prove Proof System Conjunctive Normal Form## Preview

Unable to display preview. Download preview PDF.

## References

- [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]W. Bibel, “Tautology Testing with a Generalized Matrix Reduction Method,”
*Theoretical Computer Science*, 8 (1979), pp.31–44.MathSciNetCrossRefzbMATHGoogle Scholar - [3]C-L Chang and R.C. Lee,
*Symbolic Logic and Mechanical Theorem Proving.*Academic Press (1973), New York.Google Scholar - [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]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]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]S.C. Kleene,
*An Introduction to Metamathematics*. (1952), Van Nostrand, New York.zbMATHGoogle Scholar - [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]B. Krishnamurthy, “Short Proofs for Tricky Formulas,” Unpublished Manuscript, (1982), G.E. R and D Center, Schenectady, NY.zbMATHGoogle Scholar
- [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]B. Monien and E. Speckenmeyer, “3-Satisfiability is Testable in O(1.62
^{r}) Steps,” Bericht Nr. 3/1979 (1979), GH Paderborn, Fachbereich Mathematik-Informatik.Google Scholar - [12]J.A. Robinson, “A Machine Oriented Logic Based on the Resolution Principle,”
*JACM*, 12 (1965), pp. 23–41.MathSciNetCrossRefzbMATHGoogle Scholar - [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