Exploiting parallelism: highly competitive semantic tree theorem prover

Abstract

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 semantic 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.

Sung Nam Si, Bun Dang Gu, Gu Mi Dong, Sinwon Apt, Korea; E-mail: [email protected]

Current address: Korea Telecom Research Center, Seoul, Korea.

Keywords:

• Automated reasoning
• Semantic tree
• Resolution–refutation
• Theorem proving

Notes

Sung Nam Si, Bun Dang Gu, Gu Mi Dong, Sinwon Apt, Korea; E-mail: [email protected]

Current address: Korea Telecom Research Center, Seoul, Korea.

Current address: Korea Telecom Research Center, Seoul, Korea.