Towards a tableau based high performance automated theorem prover
Md. Zahidul Islam, Ahmed Shah Mashiyat, Kashif Nizam Khan, S. M. Masud Karim · 2010
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.