Theory and Logic

The workshop "Proof Theory: Herbrand's Theorem revisited" will take place on 25.-27.5.2017 at TU Wien and is co-organized by the Kurt Gödel Society.

Herbrand's theorem belongs to the greatest results in logic of the 20th century. This result had a major impact on proof theory and automated deduction. The purpose of this workshop is to discuss recent developments in Herbrand-based logical inference and its applications.

Successful "Proof Theory: Herbrand's Theorem revisited" Workshop

(picture taken during the excursion)

Invited Speakers

Rosalie Iemhoff
Pavel Pudlák

Format

Invited speakers 1h; other contributions will last 25 minutes

Schedule

Venue

Seminar room "Gödel", Favoritenstr. 9, access from the inner courtyard
TU Wien

Abstracts

speaker: Juan Aguilera

title: The Infinite Epsilon Calculus

We define the analog of the epsilon calculus for formulae of countable length. Under suitable set-theoretic assumptions, it can be shown to satisfy the epsilon theorem and the cut-elimination theorem.

speaker: Federico Aschieri

title: Games Semantics and the Complexity of Cut-Elimination

In modern game semantics two research lines have run in parallel for quite a while, to such an extent they are often mistakenly considered different semantics. They are the logical tradition of Coquand and the computer science tradition of Hyland-Ong. It turns out that these two traditions combined together provide all the tools we need for a new, very refined complexity analysis of several computational phenomenons. We are speaking of: first-order cut-elimination, normalization in natural deduction, interaction between Herbrand expansion trees and any other dialogical process game semantics can model and apply to. In particular, we present abstract complexity results about Coquand-Hyland-Ong game semantics; we provide a novel method to bound the length of interactions between strategies and to measure precisely the tower of exponentials defining the worst-case complexity. These abstract combinatorial results apply then directly to cut-elimination thanks to expansion trees, yielding sharper measures and estimates than the traditional ones.

speaker: Matthias Baaz

title: Short Herbrand Disjunctions generated by unusual forms of cut-elimination

An elementary cut-elimination procedure is presented for LJ-derivations without v and prenex cuts only.(Proofs of this form admit mid-sequents!) As a corrolary we develop a new cut-elimination procedure for LJ (with v), which is always elementary when the number of iterated quantifiers is fixed, i.e. without nonelementary impact of the iteration of ->.
This is joint work with Christian Fermüller.

speaker: David Cerna

title: Proof Schemata: Clausal Analysis, Multiple parameters, and Induction Over Partial-orders

Proof schemata have proven to be essential to efforts attempting to push Herbrand's theorem into the realm of inductive proof theory. So far two systems for schematic cut-elimination have been introduced, one which is incomplete, but can handle the formalization of complex arguments, and one which is complete but can only handle the formalization of arguments too structurally simple to be of mathematical interest. Though, both systems allow the extraction of a Herbrand sequent, only the weaker of the two can do so automatically and without much effort. We discuss recent work focused on the discovery of a middle ground between the two systems and attempts to go beyond the one parameter case. Our clausal analysis of proof schemata provides a simplified characteristic clause set and a calculus for proof schema construction allows us to extend the method beyond one parameter and complete induction.

speaker: Gabriel Ebner

title: Complexity of decision problems on TRATGs

Totally rigid acyclic tree grammars (TRATGs) describe the behavior of quantifier inferences under cut-elimination in proofs with Pi_1-cuts. We determine the complexity of the membership, containment, disjointness, and equivalence problems on this class of grammars. Each of these is equivalent to a problem concerning the Herbrand sequent after cut-elimination. Our complexity results transfer to the corresponding proof-theoretic problems.

speaker: Stefan Hetzl

title: Some observations on the logical foundations of inductive theorem proving

The subject of automated inductive theorem proving in computer science has developed rather independently of the study of arithmetical theories in mathematical logic. However, the use of model-theoretic techniques can provide unprovability results of interest to the automation of inductive theorem proving.
We study several aspects of automated inductive theorem proving from a logical point of view, in particular 1. the choice of a proof shape and 2. the choice of an induction rule. Concerning 2. we clarify the relationship between various notions of inductiveness that have been considered in the computer science literature.
This is joint work with Tin Lok "Lawrence" Wong.

speaker: Rosalie Iemhoff

title: Quantifiers and functions in intuitionistic logic

Quantification in intuitionistic logic differs considerably from quantification in classical logic. This is particularly striking in the context of Skolemization and Herbrand’s theorem. In recent years there has emerged quite some work on the extent to which Skolem’s methods can be applied in nonclassical logics, and several alternative approaches have been developed. This talk is a survey of these results, with an emphasis on intuitionistic logic.

speaker: Roman Kuznets

title: Herbrand's Phenomena in Justification Logic

Justification logic is a refinement of modal logic that views the modality as an existential quantifier over justifications. Thus, both modal and justification logic can be viewed as sublanguages of the same first-order language with terms ranging over justifications. In the talk we explore how Herbrandization emerged as a stepping stone in proving the Realization Theorem, one of the central results in justification logic, providing its connection to modal logic.

speaker: Alexander Leitsch

title: Extracting Herbrand Systems in the schematic CERES method

The cut-elimination method CERES (for first- and higher-order classical logic) is based on the notion of a characteristic clause set (or a characteristic formula) X, which is extracted from an LK-proof and is always unsatisfiable. A resolution refutation of X can be used as a skeleton for a proof with atomic cuts only (atomic cut normal form). This is achieved by replacing clauses from the resolution refutation by the corresponding projections of the original proof. We present a generalization of CERES (called CERESs) to first-order proof schemata. Proof schemata are parameterized sequences of first-order proofs constructed using primitive recursive definitions. We define a schematic version of the sequent calculus, called LKS, and devise algorithms to extract schematic characteristic formulas and schematic projections from these proof schemata. We also define a schematic resolution calculus for constructing ground refutations of schemata of formulas, which can be applied to refute the schematic characteristic formulas. Finally the projection schemata and the refutation schemata are plugged together and one obtains a schematic representation of proofs with only quantifier-free cuts (ICNF-schemata). From the ICNF-schemata we can obtain so-called Herbrand systems, i.e. schematic descriptions of (infinite sequences of) Herbrand sequents. Hence CERESs yields a method to extend Herbrand's theorem to inductively defined proofs. This is joint work with Nicolas Peltier and Daniel Weller.

speaker: Michael Lettmann

title: Algorithmic Introduction of \Pi_2-cuts

Cut-free proofs in a classical first-order sequent calculus can be compressed by the introduction of cut. We discuss an algorithmic approach to introduce \Pi_2-cuts from grammars representing the Herbrand sequent of a cut-free proof. The method employs a novel unification technique based on grammars. We show that, by the proposed algorithm, we can achieve an exponential proof compression. Finally, we present an implementation of the algorithm which, given a grammar, constructs a proof with a \Pi_2-cut.

speaker: Tomer Libal

title: Redundancy Elimination in Higher-order Theorem Proving

A key reason for the success of first-order forward search methods like resolution is their utilization of optimization techniques. Among these optimizations, redundancy elimination is among the most important ones. Unfortunately, most methods for first-order redundancy elimination cannot be easily lifted to the higher-order case. We will discuss some of the reasons and suggest possible ways for extending these methods to the higher-order case.

speaker: Anela Lolic

title: Expansion Trees from Non-Normalized Proofs with CERES

We define a new method for proof mining by CERES that is concerned with the extraction of expansion trees. 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 the expansion tree). This is joint work with Alex Leitsch.

speaker: Pavel Pudlak

title: Random formulas and random proofs

Random formulas drawn from particular probability distributions are tautologies with high probability. For example, random 3-DNF with n variables and 5n clauses is a tautology with high probability. I will discuss the question whether it is possible to make use of random formulas to derive "useful" tautologies. The evidence so far is that the answer is no. The negative results are based on random proof systems, in particular random resolution. These proof systems prove random tautologies with short proofs, but other tautologies that are known to be hard for these proof systems remain hard also when randomness is used.

speaker: Revantha Ramanayake

title: Decidability arguments using cutfree proof calculi

We describe our work-in-progress attempting to prove the decidability of monoidal t-norm logic MTL using its hypersequent proof calculus. A non-constructive semantic proof has been presented for this logic but it does not yield complexity bounds. Finding a syntactic proof is technically interesting because the hypersequent calculus is elegant. Moreover, the problem is general in the sense that the problematic interaction between the external contraction rule and a communication rule has an analogue in other hypersequent calculi as well. A further motivation is that the decidability of Involutive MTL (a straightforward extension of the MTL hypersequent calculus) is open. We believe that there is much scope for abstracting/expressing the decision problem via proof calculi in familiar mathematical terms, to make it examinable and interesting to a wider community. A long term aim is to develop a toolkit of methods for investigating decidability via syntactic calculi. Joint work with Michael Drmota.

speaker: Giselle Reis

title: Ceres in intuitionistic logic

Ceres is a cut-elimination method that transforms a proof P with cuts into a proof with atomic cuts by merging parts of P with a resolution refutation of a clause set, obtained from the cuts in P. The adaptation of this method to intuitionistic logic poses some challenges, as structural restrictions on intuitionistic calculi are often violated by the operations. In this talk we will present Ceres-i, a modification of Ceres that can be successfully applied to intuitionistic proofs, resulting, this time, in cut-free proofs. The structural violations resulting from resolution are avoided by substituting this step with a new operation called proof resolution. We also show that the method is complete for LJ. This is joint work with David Cerna, Alexander Leitsch and Simon Wolfsteiner.

speaker: Martin Riener

title: Producing Skolem Expansion Trees with the CERES omega method: A case study

The CERES omega method for cut-elimination in higher-order logic adds an additional layer of complexity to the CERES method for first-order logic. At its core lies the calculus LKskc which introduces strong quantifiers from skolem terms without an eigenvariable condition. Therefore, additional post-processing steps are required to reconstruct an LK proof. We propose the use of skolem-expansion trees as alternate data-structure to LK and investigate how far these post-processing steps are necessary. A formalization of the infinite pigeon hole principle serves as a case study for our results.

Participants

Juan Aguilera
Federico Aschieri
Matthias Baaz
Paolo Baldi
David Cerna
Gabriel Ebner
Francesco Genco
Danny Arlen de Jesús Gómez Ramírez
Francesca Gulisano
Stefan Hetzl
Roman Kuznets
Alexander Leitsch
Michael Lettmann
Tomer Libal
Anela Lolic
Hugo Moeneclaey
Revantha Ramanayake
Giselle Reis
Martin Riener
Jannik Vierling

Program Committee

Matthias Baaz
Stefan Hetzl
Alexander Leitsch