| Summary: | Semantic trees have served as a theoretical tool for confirming the unsatisfiability of clauses in first-order predicate logic, but it has seemed impractical to use them in practice. In this thesis we experimentally investigated the practicality of generating semantic trees for proofs of unsatisfiability. We considered two ways of generating semantic trees. First, we looked at semantic trees generated using the canonical enumeration of atoms from the Herbrand base of the given clauses. Then, we considered semantic trees generated by selectively choosing the atoms from the Herbrand base using an improved semantic tree generator, AISTG. A comparison was made between the two approaches using the theorems from the "Stickel Test Set". In underlying the practicality of using semantic tree generators as mechanical theorem provers, another comparison was made between the AISTG and a resolution-refutation theorem prover "The Great Theorem Prover".
|
|---|
