The practicality of generating semantic trees for proofs of unsatisfiability

Abstract

In this paper, we investigate the practicality of generating semantic trees to prove the unsatisfiabi-lity of sets of clauses in first-order predicate logic. Two methods of generating semantic trees are considered. First, we consider semantic trees generated by using the canonical enumeration of Herbrand base atoms. Then, we consider semantic trees generated by selectively choosing the atoms from the Herbrand base. A comparison is made between the two approaches using the theorems from the Stickel Test Set.

Keywords:

• Herbrand universe
• Herbrand base
• unsatisfiability
• Herbrand interpretation
• Herbrand procedure
• semantic trees

C.R. Categories::

• I.2.3
• I.2.8