2005 | OriginalPaper | Chapter
Proof Output and Transformation for Disconnection Tableaux
Authors : Philipp Correll, Gernot Stenz
Published in: Automated Reasoning with Analytic Tableaux and Related Methods
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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.