Sciweavers

TABLEAUX
2005
Springer

Proof Output and Transformation for Disconnection Tableaux

13 years 9 months ago
Proof Output and Transformation for Disconnection Tableaux
For applications of first-order automated theorem provers in a wider verification context it is essential to provide a means of presenting and checking automatically found proofs. In this paper we present a new method of transforming disconnection tableau proofs found by the prover system DCTP into a series of resolution inferences representing a resolution refutation of the proof problem.
Philipp Correll, Gernot Stenz
Added 28 Jun 2010
Updated 28 Jun 2010
Type Conference
Year 2005
Where TABLEAUX
Authors Philipp Correll, Gernot Stenz
Comments (0)