Generating Schemata of Resolution Proofs

TL;DR

This paper introduces two algorithms for extracting resolution proof schemata from closed tableaux, balancing complexity and efficiency to enhance proof analysis in propositional logic.

Contribution

It presents novel algorithms for extracting resolution proof schemata from tableaux, offering a trade-off between proof complexity and computational efficiency.

Findings

First algorithm produces complex derivations with elaborate rewrite systems.

Second algorithm yields simpler proof systems, though less efficient.

Both algorithms extend capabilities for proof analysis in propositional schemata.

Abstract

Two distinct algorithms are presented to extract (schemata of) resolution proofs from closed tableaux for propositional schemata. The first one handles the most efficient version of the tableau calculus but generates very complex derivations (denoted by rather elaborate rewrite systems). The second one has the advantage that much simpler systems can be obtained, however the considered proof procedure is less efficient.