文章基本信息

标题：A Tableau Based Automated Theorem Prover Using High Performance Computing
本地全文：下载
作者：Islam, Md Zahidul ; Mashiyat, Ahmed Shah ; Khan, Kashif Nizam 等
期刊名称：Journal of Computers
印刷版ISSN：1796-203X
出版年度：2012
卷号：7
期号：3
页码：597-607
DOI：10.4304/jcp.7.3.597-607
语种：English
出版社：Academy Publisher
摘要：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, such as Semantic tableau. It is used to prove the validity of a formula by contradiction and it 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 article, we describe a detailed implementation of a sequential tableau algorithm for propositional and first order logic using a procedural language rather then logic programming language. We also illustrate a tableau based proof system in a distributed environment using the Message Passing Interface. This paper also investigates two distinct approaches for parallel and distributed implementation and describes the experimental formula generation procedure. The proposed high performance approach will un-wrap an efficient paradigm for automated theorem proving.
关键词：Automated theorem proving;high performance computing;message passing interface;semantic tableau