Ordered semantic hypertableaux

Abstract

A family of tableau methods, called ordered semantic hyper (OSH) tableau methods for first-order theories with function symbols, is presented. These methods permit semantic information to guide the search for a proof. They also may make use of orderings on literals, clauses, and interpretations to guide the search. In a typical tableau, the branches represent conjunctions of literals, and the tableau represents the disjunction of the branches. An OSH tableau is as usual except that each branch B has an interpretation I0[B] associated with it, where I0 is an interpretation supplied at the beginning and I0[B] is the interpretation most like I0 that satisfies B. Only clauses that I0[B] falsifies may be used to expand the branch B, thus restricting the kinds of tableau that can be constructed. This restriction guarantees the goal sensitivity of these methods if I0 is properly chosen. Certain choices of I0 may produce a purely bottom-up tableau construction, while others may result in goal-oriented evaluation for a given query. The choices of which branch is selected for expansion and which clause is used to expand this branch are examined and their effects on the OSH tableau methods considered. A branch reordering method is also studied, as well as a branch pruning technique called complement modification, that adds additional literals to branches in a soundness-preserving manner. All members of the family of OSH tableaux are shown to be sound, complete, and proof convergent for refutations. Proof convergence means that any allowable sequence of operations will eventually find a proof, if one exists. OSH tableaux are powerful enough to be treated as a generalization of several classes of tableau discussed in the literature, including forward chaining and backward chaining procedures. Therefore, they can be used for efficient query processing.