Date of Award
12-2008
Document Type
Dissertation
Degree Name
Doctor of Philosophy (PhD)
Legacy Department
Computer Science
Committee Chair/Advisor
Stevenson, D. E
Committee Member
Hedetniemi , Steve T
Committee Member
Jacobs , David P
Committee Member
Warner , Daniel D
Abstract
An automatic theorem prover is a computer program that proves theorems without the assistance of a human being. Theorem proving is an important basic tool in proving theorems in mathematics, establishing the correctness of computer programs, proving the correctness of communication protocols, and verifying integrated circuit designs.
This dissertation introduces two new categories of theorem provers, one for classical propositional logic and another for intuitionistic propositional logic. For each logic a container property and generalized algorithm are introduced.
Many methods have been developed over the years to prove theorems in propositional logic. This dissertation describes and presents example proofs for five of these methods: natural deduction, Kripke tableau, analytic tableau, matrix, and resolution. Each of these methods uses refutation to prove a theorem. In refutation, the proposed theorem is assumed to be false. The theorem prover is successful, only if the analysis of this assumption leads to a contradiction.
Each of these methods, except resolution, share a common algorithm. To prove this, the container is introduced. A data structure used by a method is a container, if it meets a set of properties.
A generalized algorithm that proves theorems is introduced. Since each step in this algorithm uses only operations that are provided by the container. The steps it performs can be translated to any method that can be described using a container. This allows the data structures representing a partial proof in one method, to be transformed into the data structures representing the “same ” proof in another method. This can be very beneficial in a situation where another method would be more efficient in advancing the proof. In addition to being able to switch between methods, an heuristic for one method can be examined to see if it can be applied to the other methods.
This development is repeated for intuitionistic logic. Each of these methods, except resolution, is modified to prove theorems in intuitionistic logic. An intuitionistic container is presented. Each one of the intuitionistic methods is proven to have the properties of the intuitionistic container. Lastly, a generalized algorithm using the intuitionistic container is presented. This algorithm proves theorems in intuitionistic logic. Examples showing successful and unsuccessful proof attempts are presented.
Recommended Citation
Doyle, Edward, "Two Categories of Refutation Decision Procedures for Classical and Intuitionistic Propositional Logic" (2008). All Dissertations. 324.
https://tigerprints.clemson.edu/all_dissertations/324