Generating Schemata of Resolution Proofs
Vincent Aravantinos, Nicolas Peltier

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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSemantic Web and Ontologies · Logic, Reasoning, and Knowledge · Advanced Database Systems and Queries
