×

zbMATH — the first resource for mathematics

Exploiting parallelism: Highly competitive semantic tree theorem prover. (English) Zbl 1082.68103
Summary: Semantic trees have often been used as a theoretical tool for showing the unsatisfiability of clauses in first-order predicate logic. Their practicality has been overshadowed, however, by other strategies. In this paper, we introduce unit clauses derived from resolutions when necessary to construct a semantic tree, leading to a strategy that combines the construction of semantic trees with resolution-refutation. The parallel semantic tree theorem prover, called PrHERBY, combines semantis trees and resolution-refutation methods. The parallel system is scalable by strategically selecting atoms with the help of dedicated resolutions. In addition, a parallel grounding scheme allows each system to have its own instance of generated atoms, thereby increasing the possibility of success. The PrHERBY system presented performs significantly better and generally finds proof using fewer atoms than the semantic tree prover, HERBY and its parallel version PHERBY.
MSC:
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Software:
Gandalf; HERBY; HOL; PrHERBY; TPTP
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Al-Anjawi A, ICCI2000 (2000)
[2] Almulla M, Ph.D. Thesis, School of Computer Science, McGill University (1995)
[3] DOI: 10.1080/00207169608804524 · Zbl 1001.68513 · doi:10.1080/00207169608804524
[4] Almulla M Newborn M (1998) http://www.cs.miami.edu/ tptp/CASC/15
[5] DOI: 10.1145/321607.321618 · Zbl 0212.34202 · doi:10.1145/321607.321618
[6] Chang CL, Symbolic Logic and Mechanical Theorem Proving, Academic Press (1973) · Zbl 0263.68046
[7] Giest A, A User’s Guide and Tutorials for Networked Parallel Computing, MIT Press (1994)
[8] Hurd J (1999) Integrating gandalf and HOL, TPHOLs’99 LNCS 1690 311 321
[9] Kim CK, Ph.D. Thesis, School of Computer Science, McGill University (2004)
[10] Kim CK Newborn M (2003) Competitive semantic tree theorem prover with resolutions, EuroPVM/MPI
[11] Korf RE, Artificial Intelligence pp 97– (1985)
[12] Newborn M (1998) http://www.cs.miami.edu/ tptp/CASC/15/SystemDescriptions.html#TGTP
[13] Newborn M, Automated Theorem Proving: Theory and Practice, Springer-Verlag (2001) · Zbl 0963.68176 · doi:10.1007/978-1-4613-0089-2
[14] DOI: 10.1007/BF02432151 · Zbl 0642.68147 · doi:10.1007/BF02432151
[15] Plaisted DA, Ph.D. Thesis, Stanford University (1976)
[16] DOI: 10.1016/S0923-0459(97)80012-2 · doi:10.1016/S0923-0459(97)80012-2
[17] DOI: 10.1023/A:1005806324129 · Zbl 0910.68197 · doi:10.1023/A:1005806324129
[18] DOI: 10.1023/A:1018976510663 · Zbl 0913.68190 · doi:10.1023/A:1018976510663
[19] DOI: 10.1145/7531.8928 · Zbl 0639.68093 · doi:10.1145/7531.8928
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.