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.

• Type: Conference
• Year: 2005
• Where: TABLEAUX
• Authors: Philipp Correll, Gernot Stenz
• Keywords: Artificial Intelligence, Automated Theorem Provers, Disconnection Tableau Proofs, Resolution Inferences, TABLEAUX 2005