Craig interpolation is a fundamental property of classical and non-classic logics with a plethora of applications from philosophical logic to computer-aided verification. The question of which interpolants can be obtained from an interpolation algorithm is of profound importance. Motivated by this question, we initiate the study of completeness properties of interpolation algorithms. An interpolation algorithm I is complete if, for every semantically possible interpolant C of an implication A → B , there is a proof P of A → B such that C is logically equivalent to I ( P ) . We establish incompleteness and different kinds of completeness results for several standard algorithms for resolution and the sequent calculus for propositional, modal, intuitionistic, and first-order logic.

We consider a class of formula equations in first-order logic, Horn formula equations, which are defined by a syntactic restriction on the occurrences of predicate variables. Horn formula equations play an important role in many applications in computer science. We state and prove a fixed-point theorem for Horn formula equations in first-order logic with a least fixed-point operator. Our fixed-point theorem is abstract in the sense that it applies to an abstract semantics which generalises standard semantics. We describe several corollaries of this fixed-point theorem in various areas of computational logic, ranging from the logical foundations of program verification to inductive theorem proving.

Abstract Second-order quantifier-elimination is the problem of finding, given a formula with second-order quantifiers, a logically equivalent first-order formula. While such formulas are not computable in general, there are practical algorithms and subclasses with applications throughout computational logic. One of the most prominent algorithms for second-order quantifier elimination is the SCAN algorithm which is based on saturation theorem proving. In this paper we show how the SCAN algorithm on clause sets can be extended to solve a more general problem: namely, finding an instance of the second-order quantifiers that results in a logically equivalent first-order formula. In addition we provide a prototype implementation of the proposed method. This work paves the way for applying the SCAN algorithm to new problems in application domains such as modal correspondence theory, knowledge representation, and verification.

Craig interpolation is a fundamental property of logics with a plethora of applications from philosophical logic to computer-aided verification. The question of which interpolants can be obtained from an interpolation algorithm is of profound importance. Motivated by this question, we initiate the study of completeness properties of interpolation algorithms. An interpolation algorithm ℐ is complete if, for every interpolant C of an implication A → B, there is a proof P of A → B such that C is logically equivalent to ℐ(P). We establish incompleteness and different kinds of completeness results for several standard algorithms for resolution and the sequent calculus for propositional, modal, and first-order logic.

We consider a typical integration of induction in saturation-based theorem provers and investigate the effects of Skolem symbols occurring in the induction formulas. In a practically relevant setting we establish a Skolem-free characterization of refutation in saturation-based proof systems with induction. Finally, we use this characterization to obtain unprovability results for a concrete saturation-based induction prover.

The notion of clause set cycle abstracts a family of methods for automated inductive theorem proving based on the detection of cyclic dependencies between clause sets. By discerning the underlying logical features of clause set cycles, we are able to characterize clause set cycles by a logical theory. We make use of this characterization to provide practically relevant unprovability results for clause set cycles that exploit different logical features.

This article examines the computational content of the classical Gentzen sequent calculus. There are a number of well-known methods that extract computational content from first-order logic but applying these to the sequent calculus involves first translating proofs into other formalisms, Hilbert calculi or Natural Deduction for example. A direct approach which mirrors the symmetry inherent in sequent calculus has potential merits in relation to proof-theoretic considerations such as the (non-)confluence of cut elimination, the problem of cut introduction, proof compression and proof equivalence. Motivated by such applications, we provide a representation of sequent calculus proofs as higher order recursion schemes. Our approach associates to an LK proof π of ⇒∃vF, where F is quantifier free, an acyclic higher order recursion scheme H with a finite language yielding a Herbrand disjunction for ∃vF. More generally, we show that the language of H contains all Herbrand disjunctions computable from π via a broad range of cut elimination strategies.

Abstract We present formula equations—first-order formulas with unknowns standing for predicates—as a general formalism for treating certain questions in logic and computer science, like the Auflösungsproblem and loop invariant generation. In the case of the language of affine terms over $\mathbb{Q}$, we translate a quantifier-free formula equation into an equivalent statement about affine spaces over $\mathbb{Q}$, which can then be decided by an iteration procedure.

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.

Abstract Herbrand’s theorem is one of the most fundamental insights in logic. From the syntactic point of view, it suggests a compact representation of proofs in classical first- and higher-order logics by recording the information of which instances have been chosen for which quantifiers. This compact representation is known in the literature as Miller’s expansion tree proof. It is inherently analytic and hence corresponds to a cut-free sequent calculus proof. Recently several extensions of such proof representations to proofs with cuts have been proposed. These extensions are based on graphical formalisms similar to proof nets and are limited to prenex formulas. In this paper, we present a new syntactic approach that directly extends Miller’s expansion trees by cuts and also covers non-prenex formulas. We describe a cut-elimination procedure for our expansion trees with cut that is based on the natural reduction steps and shows that it is weakly normalizing.

In this paper we study the logical foundations of automated inductive theorem proving. To that aim we first develop a theoretical model that is centered around the difficulty of finding induction axioms which are sufficient for proving a goal. Based on this model, we then analyze the following aspects: the choice of a proof shape, the choice of an induction rule and the language of the induction formula. In particular, using model-theoretic techniques, we clarify the relationship between notions of inductiveness that have been considered in the literature on automated inductive theorem proving.

This volume contains selected papers from the workshop ‘Concepts and Meaning’ held on 2–5 May 2012 at the Vienna University of Technology in honour of the 60th birthday of Alexander Leitsch. Alexander Leitsch made substantial contributions to a variety of different research areas including automated deduction, computability theory, proof theory and formal mathematics. The broad scope of his research interests is reflected in the contents of this special issue that features the following papers (in alphabetic order): ... A common thread that runs through Alexander Leitsch' scientific work is his mastery of syntactic precision rooted in the conviction that the syntactic form not only captures but even determines the semantic meaning of concepts, hence also the title of this special issue. In addition to his scientific activities he is also an inspiring colleague and a dedicated and enthusiastic teacher as witnessed by generations of his students who are now successful in academia as well as in industry, some of which are represented in this volume.

In this article, we deal with the following problem which we call Boolean unification with predicates: For a given formula F[X] in first-order logic with equality containing an n-ary predicate variable X⁠, is there a quantifier-free formula G[x1,…,xn] such that the formula F[G] is valid in first-order logic with equality? We obtain the following results. Boolean unification with predicates for quantifier-free F is Π2P-complete. In addition, there exists an EXPTIME algorithm which for an input formula F[X]⁠, given as above, constructs a formula G such that F[G] being valid in first-order logic with equality, if such a formula exists. For F of the form ∀y¯F′[X,y¯] with F′ quantifier-free, we prove that Boolean unification with predicates is already undecidable. The same holds for F of the form ∃y¯F′[X,y¯] for F′ quantifier-free. Instances of Boolean unification with predicates naturally occur in the context of automated theorem proving. Our results are relevant for cut-introduction and the automated search for induction invariants.

We present an algorithm to optimally compress a finite set of terms using a vectorial totally rigid acyclic tree grammar. This class of grammars has a tight connection to proof theory, and the grammar compression problem considered in this article has applications in automated deduction. The algorithm is based on a polynomial-time reduction to the MaxSAT optimization problem. The crucial step necessary to justify this reduction consists of applying a term rewriting relation to vectorial totally rigid acyclic tree grammars. Our implementation of this algorithm performs well on a large real-world dataset.

The sequent calculus is often criticized for requiring proofs to contain large amounts of low-level syntactic details that can obscure the essence of a given proof. Because each inference rule introduces only a single connective, sequent proofs can separate closely related steps—such as instantiating a block of quantifiers—by irrelevant noise. Moreover, the sequential nature of sequent proofs forces proof steps that are syntactically non-interfering and permutable to nevertheless be written in some arbitrary order. The sequent calculus thus lacks a notion of canonicity : proofs that should be considered essentially the same may not have a common syntactic form. To fix this problem, many researchers have proposed replacing the sequent calculus with proof structures that are more parallel or geometric. Proof-nets, matings and atomic flows are examples of such revolutionary formalizms. We propose, instead, an evolutionary approach to recover canonicity within the sequent calculus, which we illustrate for classical first-order logic. The essential element of our approach is the use of a multi-focused sequent calculus as the means for abstracting away low-level details from classical cut-free sequent proofs. We show that, among the multi-focused proofs, the maximally multi-focused proofs that collect together all possible parallel foci are canonical. Moreover, if we start with a certain focused sequent proof system, such proofs are isomorphic to expansion proofs —a well known, minimalistic and parallel generalization of Herbrand disjunctions—for classical first-order logic. This technique appears to be a systematic way to recover the ‘essence of proof’ from within sequent calculus proofs.

Recently a new connection between proof theory and formal language theory was introduced. It was shown that the operation of cut elimination for proofs in first-order predicate logic involving Pi_1-cuts corresponds to computing the language of a particular class of regular tree grammars. The present paper expands this connection to the level of Pi_2-cuts. Given a proof pi of a Sigma_1 formula with cuts only on Pi_2 formulæ, we show there is associated to pi a natural context-free tree grammar whose language is finite and yields a Herbrand disjunction for pi.

Abstract We consider the following problem: Given a proof of the Skolemization of a formulaF, what is the length of the shortest proof ofF? For the restriction of this question to cut-free proofs we prove corresponding exponential upper and lower bounds.

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.

Abstract We study cut-elimination in first-order classical logic. We construct a sequence of polynomial-length proofs having a non-elementary number of different cut-free normal forms. These normal forms are different in a strong sense: they not only represent different Herbrand-disjunctions but also differ in their prepositional structure. This result illustrates that the constructive content of a proof in classical logic is not uniquely determined but rather depends on the chosen method for extracting it.