Schematic Refutations of Formula Schemata
- PDF / 711,145 Bytes
- 47 Pages / 439.37 x 666.142 pts Page_size
- 65 Downloads / 220 Views
Schematic Refutations of Formula Schemata David M. Cerna1,2
· Alexander Leitsch3 · Anela Lolic3
Received: 19 December 2019 / Accepted: 29 October 2020 © The Author(s) 2020
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. Keywords Schematic proofs · Resolution · Induction · Schematic formulas
1 Introduction Recursive definitions of functions play a central role in computer science, particularly in functional programming. While recursive definitions of proofs are less common they are of increasing importance in automated proof analysis. Proof schemata, i.e. recursively defined infinite sequences of proofs, serve as an alternative formulation of induction. Prior to the formalization of the concept, an analysis of Fürstenberg’s proof of the infinitude of primes [5] suggested the need for a formalism quite close to the type of proof schemata we will discuss in this paper. The underlying method for this analysis was CERES [6] (cut-elimination by resolution) which, unlike reductive cut-elimination, can be applied to recursively defined proofs by extracting a schematic unsatisfiable formula and constructing a recursively defined refutation. Moreover, Herbrand’s theorem can be extended to an expressive fragment of proof schemata, that is those formalizing k-induction [11,14]. Unfortunately, the construction of recursively defined refutations is a highly complex task. In previous work [14] a superposition
B
Anela Lolic [email protected] David M. Cerna [email protected]; [email protected] Alexander Leitsch [email protected]
1
The Czech Academy of Science, Institute of Computer Science (CAS ICS), Prague, Czechia
2
Research Institute for Symbolic Computation, Johannes Kepler University, Linz, Austria
3
Institute of Logic and Computation, TU Wien, Vienna, Austria
123
D. Cerna et al.
calculus for certain types of formulas was used for the construction of refutation schemata, but only works for a weak fragment of arithmetic and is hard to use interactively. The key to proof analysis using CERES in a first-order setting is not the particularities of the method itself, but the fact that it provides a bridge between automated deduction and proof theory. In the schematic setting, where the proofs are recursively defined, a bridge over the chasm has been provided [11,14], but there has not been much development on the other side to reap the benefits of. The few existing results about automated deduction for recursively defined formulas barely provide the necessary expressive power to analyse significant mathematical argumentation. Applying the earlier constructions to a weak mathematical statement such as th
Data Loading...
