Towards a tableau based high performance automated theorem prover

摘要

Automated Theorem Proving systems are enormously powerful computer programs capable of solving immensely difficult problems. The extreme capabilities of these systems lie on some well-established proof systems. Semantic tableau is such a proof system used to prove the validity of a formula by contradiction and can produce a counterexample if it fails. It can also be used to prove whether a formula is a logical consequence of a set of formulas. Tableau can be used in propositional logic, predicate logic, modal logic, temporal logic, and in other non-classical logics. In this paper, we describe the implementation of a sequential tableau algorithm for propositional logic using a procedural programming language rather then logic programming language. We also propose a tableau based proof system in a distributed environment using the message passing interface. Successful implementation of the proposed high performance approach will un-wrap an efficient paradigm for automated theorem proving.