Depth-first Proof Search without Backtracking for
Free-variable Clausal Tableaux

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.