A Tableau Based Automated Theorem Prover Using High Performance Computing

被引:0
作者
Islam, Md Zahidul [1 ]
Mashiyat, Ahmed Shah [2 ]
Khan, Kashif Nizam [1 ]
Karim, S. M. Masud [1 ]
机构
[1] Khulna Univ, Comp Sci & Engn Discipline, Khulna, Bangladesh
[2] St Francis Xavier Univ, Dept Math Stat & Comp Sci, Antigonish, NS, Canada
关键词
Automated theorem proving; high performance computing; message passing interface; semantic tableau;
D O I
10.4304/jcp.7.3.597-607
中图分类号
TP39 [计算机的应用];
学科分类号
081203 ; 0835 ;
摘要
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 counter example 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 firstorder 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.
引用
收藏
页码:597 / 607
页数:11
相关论文
共 28 条
  • [1] One-pass tableaux for computation tree logic
    Abate, Pietro
    Gore, Rajeev
    Widmann, Florian
    [J]. LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING, PROCEEDINGS, 2007, 4790 : 32 - +
  • [2] Astrachan L. O., 1991, TECH REP
  • [3] Beckert B., 1996, Automated Deduction - Cade-13. 13th International Conference on Automated Deduction. Proceedings, P303
  • [4] Ben-Ari M., 1981, POPL 81 PROC 8 ACM S, P164, DOI [10.1145/567532.567551, DOI 10.1145/567532.567551]
  • [5] Bose S., 1989, Proceedings. Fourth Annual Symposium on Logic in Computer Science (Cat. No.89CH2753-2), P80, DOI 10.1109/LICS.1989.39161
  • [6] Carpenter B, MPIJAVA HOME PAGE
  • [7] COMPUTATIONAL ASPECTS OF THE PENTIUM AFFAIR
    COE, T
    MATHISEN, T
    MOLER, C
    PRATT, V
    [J]. IEEE COMPUTATIONAL SCIENCE & ENGINEERING, 1995, 2 (01): : 18 - 30
  • [8] del Cerro L. F., 2001, Automated Reasoning. First International Joint Conference, IJCAR 2001. Proceedings (Lecture Notes in Artificial Intelligence Vol.2083), P453
  • [9] Fensel D., 1996, P 10 BANFF KNOWL ACQ, P18
  • [10] FITTING M, 1996, 1 ORDER LOGIC AUTOMA