Analyzing the selection of the herbrand base process for building a Smart Semantic Tree Theorem Prover

Shenaiber, Nourah (2015). Analyzing the selection of the herbrand base process for building a Smart Semantic Tree Theorem Prover. University of Birmingham. Ph.D.

Preview

Shenaiber15PhD.pdf
PDF - Accepted Version
Download (1MB)

Abstract

Traditionally, semantic trees have played an important role in proof theory for validating the unsatisfiability of sets of clauses. More recently, they have also been used to implement more practical tools for verifying the unsatisfiability of clause sets in first-order predicate logic. The method ultimately relies on the Herbrand Base, a set used in building the semantic tree. The Herbrand Base is used together with the Herbrand Universe, which stems from the initial clause set in a particular theorem. When searching for a closed semantic tree, the selection of suitable atoms from the Herbrand Base is very important and should be carried out carefully by educated guesses in order to avoid building a tree using atoms which are irrelevant for the proof. In an effort to circumvent the creation of irrelevant ground instances, a novel approach is investigated in this dissertation. As opposed to creating the ground instances of the clauses in S in a strict syntactic order, the values will be established through calculations which are based on relevance for the problem at hand. This idea has been applied and accordingly tested with the use of the Smart Semantic Tree Theorem Prover (SSTTP), which provides an algorithm for choos- ing prominent atoms from the Herbrand Base for utilisation in the generation of closed semantic trees. Part of this study is an empirical investigation of this prover performance on first-order problems without equality, as well as whether or not it is able to compete with modern theorem provers in certain niches. The results of the SSTTP are promising in terms of finding proofs in less time than some of the state-of-the-art provers. However, it can not compete with them in terms of the total number of the solved problems.

Type of Work:

Thesis (Doctorates > Ph.D.)

Award Type:

Doctorates > Ph.D.

Supervisor(s):