Abstract – A lot of mathematical and logical problems cannot be easily solved by simple manual theorem proving methods. This is because of the sheer complexity of those problems. A computer based theorem prover can tackle such problems and give a fast and accurate response

because of its computational advantage over humans. The Automated Theorem Proving system will compute problems of first order clausal logic using refutation technique.

Index Terms - Automated Reasoning, First Order Logic, Resolution

1. INTRODUCTION

The very first computers were developed for mathematical calculations. With the advancement in technology, computers became more powerful and their applications more diverse. Computers that were initially just number crunching machines could now be programmed to reason.

Automated theorem proving is one of the most challenging branches of automated reasoning. It is used for tackling problems which manual theorem proving techniques may fail to solve. It has been used widely in mathematical logic, computer science and integrated circuit design and

verification.

2. DEFINITIONS

• Atomic Formula: A formula with no deeper propositional structure.

• Literal: A literal is an atomic formula or its negation.

• Clause: A clause is a finite disjunction of literals. A clause can be empty and is represented by [].

• Ground Literal, Clause: A literal or clause with no variable in it.

3. THE PROVER

The automated theorem prover is a first order clausal logic system. The input is a set of clauses which include the axioms and clauses to be proved. It uses the principle of resolution [1] to create inferences in order to provide a solution for the problem.

4. RESOLUTION PRINCIPLE

The resolution principle states that if S is any finite set of clauses and Rn(S) is the nth resolution of S, then S is unsatisfiable if and only if Rn(S) contains [] for some n>=0. [1]

This principle is applied by using the negation of the clause to be proved in the set of clauses and then create new clauses by unification. [1] 

5. SEARCH STRATEGY

The resolution principle, if applied directly, creates a lot of redundant and needless clauses and the number of clauses can  run into thousands depending upon the input set of clauses. So a search strategy is used to prevent the generation of some clauses without affecting the result.

The Set of Support [2] strategy is used in which the set of support is given a level bound which restricts the number of clauses allowed in the set of support. Additionally, the number

of literals per clause is also limited.