Journal of Symbolic Computation
Bernhard Beckert
We analyse the problem of constructing a deterministic proof procedure
for free-variable clausal tableaux that performs depth-first proof
search without backtracking; and we present a solution based on a
fairness strategy. That strategy uses weight orderings and a notion of
tableau subsumption to avoid proof cycles and it employs reconstruction
steps to handle the destructiveness of free-variable calculi.