Schematic Refutations of Formula Schemata
David Cerna, Alexander Leitsch, and Anela Lolic
TL;DR
This paper introduces a generalized resolution calculus for schematic proofs involving infinite proof sequences, enhancing previous methods and demonstrating its application through a schematic refutation of a weak pigeonhole principle.
Contribution
It presents a new, more general framework for schematic proof calculus that improves upon earlier approaches and applies it to formalize a schematic refutation.
Findings
The new calculus generalizes previous schematic deduction methods.
It successfully formalizes a proof of a weak pigeonhole principle.
The framework supports schematic refutations of complex formulas.
Abstract
Proof schemata are infinite sequences of proofs which are defined inductively. In this paper we present a general framework for schemata of terms, formulas and unifiers and define a resolution calculus for schemata of quantifier-free formulas. The new calculus generalizes and improves former approaches to schematic deduction. As an application of the method we present a schematic refutation formalizing a proof of a weak form of the pigeon hole principle.
Click any figure to enlarge with its caption.
Figure 1
Figure 2
Figure 3
Figure 4
Figure 5
Figure 6
Figure 7Peer 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.