Schematic Refutations of Formula Schemata
Logic in Computer Science
2022-07-21 v3
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.
Cite
@article{arxiv.1902.08055,
title = {Schematic Refutations of Formula Schemata},
author = {David Cerna and Alexander Leitsch and Anela Lolic},
journal= {arXiv preprint arXiv:1902.08055},
year = {2022}
}
Comments
52 pages