Abstract An inductive proof can be represented as a proof schema, i.e. as a parameterized sequence of proofs defined in a primitive recursive way. A corresponding cut-elimination method, called schematic cut-elimination by resolution, can be used to analyse these proofs, and to extract their (schematic) Herbrand sequents, even though Herbrand’s theorem in general does not hold for proofs with induction inferences. This work focuses on the most crucial part of the schematic cut-elimination method, which is to construct a refutation of a schematic formula that represents the cut-structure of the original proof schema. We develop a new framework for schematic substitutions and define a unification algorithm for resolution schemata. Moreover, we introduce a new calculus for the refutation of formula schemata that is simpler and more expressive than previous formalisms. Finally, we show that this new formalism allows the extraction of a structure from the refutation schema, called a Herbrand system, which represents its Herbrand sequent.

An inductive proof can be represented as a proof schema, i.e. as a parameterized sequence of proofs defined in a primitive recursive way. A corresponding cut-elimination method, called schematic CERES, can be used to analyze these proofs, and to extract their (schematic) Herbrand sequents, even though Herbrand’s theorem in general does not hold for proofs with induction inferences. This work focuses on the most crucial part of the schematic cut-elimination method, which is to construct a refutation of a schematic formula that represents the cut-structure of the original proof schema. Moreover, we show that this new formalism allows the extraction of a structure from the refutation schema, called a Herbrand schema, which represents its Herbrand sequent.

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.

Abstract We present a new method of computing Herbrand disjunctions. The up-to-date most direct approach to calculate Herbrand disjunctions is based on Hilbert’s epsilon formalism (which is in fact also the oldest framework for proof theory). The algorithm to calculate Herbrand disjunctions is an integral part of the proof of the extended first epsilon theorem. This paper introduces a more abstract form of epsilon proofs, the function variable proofs. This leads to a computational improved version of the extended first epsilon theorem, which allows a nonelementary speed up of the computation of Herbrand disjunctions. As an application, sequent calculus proofs are translated into function variable proofs and a variant of the axiom of global choice is shown to be removable from proofs in Neumann–Bernays–Gödel set theory.

In this paper we present an algorithmic method of lemma introduction. Given a proof in predicate logic with equality the algorithm is capable of introducing several universal lemmas. The method is based on an inversion of Gentzen’s cut-elimination method for sequent calculus. The first step consists of the computation of a compact representation (a so-called decomposition) of Herbrand instances in a cut-free proof. Given a decomposition the problem of computing the corresponding lemmas is reduced to the solution of a second-order unification problem (the solution conditions). It is shown that that there is always a solution of the solution conditions, the canonical solution. This solution yields a sequence of lemmas and, finally, a proof based on these lemmas. Various techniques are developed to simplify the canonical solution resulting in a reduction of proof complexity. Moreover, the paper contains a comprehensive empirical evaluation of the implemented method and gives an application to a mathematical proof.

We define a new method for proof mining by CERES (cut-elimination by resolution) that is concerned with the extraction of expansion trees in first-order logic (see Miller in Stud Log 46(4):347-370, 1987) with equality. In the original CERES method expansion trees can be extracted from proofs in normal form (proofs without quantified cuts) as a post-processing of cut-elimination. More precisely they are extracted from an ACNF, a proof with at most atomic cuts. We define a novel method avoiding proof normalization and show that expansion trees can be extracted from the resolution refutation and the corresponding proof projections. We prove that the new method asymptotically outperforms the standard method (which first computes the ACNF and then extracts an expansion tree). Finally we compare an implementation of the new method with the old one; it turns out that the new method is also more efficient in our experiments.

International audience

We show an effective cut-free variant of Glivenko's theorem extended to formulas with weak quantifiers: "There is an elementary function f such that if φ is a cut-free LK proof of ⊢ A with symbol complexity ≤ c, then there exists a cut-free LJ proof of ⊢ ⊯ ⊯ A with symbol complexity ≤ f(c)". This follows from the more general result: "There is an elementary function f such that if φ is a cut-free LK proof of A ⊢ with symbol complexity ≤ c, then there exists a cut-free LJ proof of A ⊢ with symbol complexity ≤ f(c)". The result is proved using a suitable variant of cut-elimination by resolution (CERES) and subsumption.

We define a generalization CERESω of the first-order cut-elimination method CERES to higher-order logic. At the core of CERESω lies the computation of an (unsatisfiable) set of sequents CS(π) (the characteristic sequent set) from a proof π of a sequent S. A refutation of CS(π) in a higher-order resolution calculus can be used to transform cut-free parts of π (the proof projections) into a cut-free proof of S. An example illustrates the method and shows that CERESω can produce meaningful cut-free proofs in mathematics that traditional cut-elimination methods cannot reach.

We investigate cut elimination in propositional substructural logics. The problem is to decide whether a given calculus admits (reductive) cut elimination. We show that for commutative single-conclusion sequent calculi containing generalised knotted structural rules and arbitrary logical rules the problem can be decided by resolution-based methods. A general cut-elimination proof for these calculi is also provided.

Building on previous results that show that hyperresolution refinements may usefully be employed as decision proceduresfor a wide range of decidable classes of clause sets we present methods for constructing models for such sets of clauses. We show how to generate finite sets of atoms that respresent Herbrand models using hyperresolution. We demonstrate that these atomic representations of models enjoy features that provide a basis for various applications in automated theorem proving. In particular, we show that the equivalence of atomic representations is decidable and that arbitrary clauses can beevaluated effectively w.r.t. to the represented models. For the investigated classes we may focus on atoms with a linear term structure and show that, for this important subcase, finite models can be extracted from the sets of atoms generated by hyperresolution. We emphasize that, in contrast to model theoretic approaches, no backtracking is needed in our proof theoretic model constructing algorithm.

We investigate the effects of different types of translations of first-order formulas to clausal form on minimal proof length. We show that there is a sequence of unsatisfiable formulassuch that the length of all refutations of non-structural clause forms of F/sub n/ is non-elementary (in the size of F/sub n/), but there are refutations of structural clause forms of F/sub n/ that are of elementary (at most triple exponential) length.>

The impact of Skolemization on the complexity of proofs in the sequent calculus is investigated. It is shown that prefix Skolemization may result in a nonelementary increase of Herbrand complexity (i. e. the minimal number of constituents in a Herbrand disjunction) versus structural Skolemization. Moreover it is shown that restricting the range of quantifiers never increases Herbrand complexity. The results provide a general mathematical justification for minimizing the range of quantifiers (by means of shifting) before Skolemization of formulas.

Although problem reduction is a very important tool in mathematical practice, relatively little attention has been paid to problem reduction in automated theorem proving. A systematical treatment of different problem reduction methods can be found in [BI71] and [Lo78]. (In [BI71] we find unary and binary reduction rules. In the unary case we reduce a problem E to a problem E', where E is provable (refutable) if E' is; for binary reduction we have to produce problems E1, E2 out of E such that E is provable (refutable) if both E1, E2 are provable (refutable).) In finding stronger reduction strategies, one has to give up completeness of the split of E into E1, E2; that means, we only require that the provability of E1 and E2 implies that of E. The authors therefore propose problem reduction based on a splitting rule of the form C → C', where C ∼ C1 n C2, C' ∼ C1 n C'2, C'2 ∼ C2 {× ← ƒ(y1,…yn)}, {x,y1,…yn} is the set of variables both in C1 and C2 and ƒ is a new function symbol up to this point not occurring in any clause. Note that the Herbrand universe is extended by ƒ and consequently C' is not derivable from C by usual resolution methods! As (∀y1) … (∀yn(∀x) (C1 n C2) → (∀y1) … (∀yn ((∀x) C1 n (∃x) (C2) is valid in first order predicate logic and C1 n C'2 is the Skolemization of the implied formula, splitting of this kind is correct. For reasons of efficiency (reduction of search space and restriction of compound terms) the authors restrict the application of the rule above to sequences of applications (called Q-reduction) completely separating the variables in C1 and C2. Finally the authors construct a sequence of clause sets Cn having resolution proofs exponential in n only, but application of the new reduction rule reduces the problem to two problems linear in n. Thus it turns out that the introduction of (elementary) quantificational rules into clause logic can strongly influence the structure of proofs and the performance of theorem provers.

The costs of subsumption algorithms are analyzed by an estimation of the maximal number of unification attempts (worst-case unification complexity) made for deciding whether a clause C subsumes a clause D . For this purpose the clauses C and D are characterized by the following parameters: number of variables in C , number of literals in C , number of literals in D , and maximal length of the literals. The worst-case unification complexity immediately yields a lower bound for the worst-case time complexity. First, two well-known algorithms (Chang-Lee, Stillman) are investigated. Both algorithms are shown to have a very high worst-case time complexity. Then, a new subsumption algorithm is defined, which is based on an analysis of the connection between variables and predicates in C . An upper bound for the worst-case unification complexity of this algorithm, which is much lower than the lower bounds for the two other algorithms, is derived. Examples in which exponential costs are reduced to polynomial costs are discussed. Finally, the asymptotic growth of the worst-case complexity for all discussed algorithms is shown in a table (for several combinations of the parameters).