STP: a simple theorem prover for IBM-PC compatible computers

ABSTRACT

STP (Simple Theorem Prover) was conceived as a tool to help gain a better understanding of the concepts and difficulties involved in producing a generalized automated theorem prover for first-order logic, such as ITP (Interactive Theorem Prover). The project was undertaken on an IBM-PC using Turbo Pascal, version 3, mainly for reasons of hardware availability and software familiarity. ITP is the model on which STP is based. Although STP is functionally much less complex than ITP, they share the same syntax for input clauses. An additional program, called the “Skolemizer”, was developed as a user aid to transform generalized first-order logic formulae into their Skolem conjunctive normal form equivalents for input to STP or to ITP. The initial strategy used to search the solution space proved to be inadequate for the development environment, and was later expanded to include a second search strategy option. The current version of STP uses LUSH resolution plus clause factoring to do refutation proofs. It is able to solve most simple problems, but takes too long to solve significant problems. Although STP met its design goal—that of being an educational experience to develop—it needs to be extended to utilize more complex forms of resolution and other related methods. With recent advances in small computer hardware and software capabilities, these enhancements should now be possible.

REFERENCES

• Bu83: Alan Bundy, The computer modelling of mathematical reasoning, Academic Press Professional, Inc., San Diego, CA, 1985
• CM84: W F. Clocksin , Christopher S. Mellish, Programming in Prolog (2nd ed.), Springer-Verlag New York, Inc., New York, NY, 1984
• CL73: Chin-Liang Chang , Richard C. Lee , Richard Char-Tung Lee, Symbolic Logic and Mechanical Theorem Proving, Academic Press, Inc., Orlando, FL, 1997
• Ll84: J. W. Lloyd, Foundations of logic programming, Springer-Verlag New York, Inc., New York, NY, 1984
• Lo78: Donald W Loveland, Automated theorem proving: A logical basis (Fundamental studies in computer science), sole distributor for the U.S.A. and Canada, Elsevier North-Holland, 1978
• LO84: Lusk, E.L. and Overbeek, R.A. (1984). "The automated reasoning system ITP.", report ANL. 84-27, Argonne National Laboratory, Argonne, Illinois.
• Ro65: J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM (JACM), v.12 n.1, p.23-41, Jan. 1965 [doi>10.1145/321250.321253]
• St86: Mark E. Stickel, A prolog Technology Theorem Prover: Implementation by an Extended Prolog Compiler, Proceedings of the 8th International Conference on Automated Deduction, p.573-587, July 27-August 01, 1986

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Mechanical theorem proving

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications

          Nouns: Turbo Pascal

  K. Computing Milieux
  K.8 PERSONAL COMPUTING

      Nouns: IBM PC

General Terms:
Algorithms, Design, Languages