Let be a set of program clauses. Assume a
selection function, which gives for a given goal one of its subgoals .
Further assume a goal and a selection
function which selects . Let be a
variant of a clause in , such that and have no
variable in common. If is most general unifier of and
, the goal
Let be a set of program clauses, a goal clause and a
selection function. For every correct answer substitution for , there is an -computed answer substitution for and a substitution , such that
In the Section on Propositional Logic we already explained
propositional tableaux and its variants, like the connection calculus
and model elimination. In this section we will give model elimination
in the first order case. Note that we need one more inference rule,
the reduction rule, in this case
A clause (normalform) tableau for a set of clauses is a tableau
for , whose nodes are literals from and which is constructed by
a (possibly infinite) sequence of applications of the following rules:
The tree consisting of root and immediate successors , where is a new variant of a clause from is a tableau for (initialisation rule).
Let be a tableau for , a branch of , and an new variant of a clause from , such that the link-condition with mgu is satisfied. If the tree is constructed by extending by the subtrees , then is a tableau for (expansion rule).
Let be a tableau for , a branch of , a leaf of , and , such that and have a mgu , than is a tableau for (reduction rule).
The following are three possible link conditions:
Weak link condition: There is a literal and , such that and have a mgu
Strong link condition: There is a leaf of , and , such that and have a mgu .
Analog to the propositional case the different link conditions result
in different calculi:
The empty condition results in a clause normal form tableau calculus.
The weak condition results in a connection calculus.
The strong link condition results in a model elimination calculus.