Implementing semantic tableaux

This report describes implementions of the tableau calculus for
first-order logic. First an extremely simple implementation,
called leanTAP, is presented, which nonetheless covers the full
functionality of the calculus and is also competitive with respect
to performance. A second approach uses compilation techniques for
proof search. Improvements inculding universal variables and
lemmata are considered as well as more efficient data structures
using reduced ordered binary decision diagrams. The implementation
language is PROLOG. In all cases fully operational PROLOG code is
given. For leanTAP a formal proof of the correctness of the
implementation is given relying on the operational semantics of
PROLOG as given by the SLD-tree model.

This report will appear as a chapter in the
Handbook of Tableau-based Methods in Automated Deduction
edited by: D. Gabbay, M. D'Agostino, R. H\"{a}hnle, and
J.Posegga
published by: KLUWER ACADEMIC PUBLISHERS

Electronic availability will be discontinued after final acceptance
for publication is obtained.