Schedule

Talks and Abstracts

Speaker: Juan P. Aguilera
Title: Hyperarithmetic Reduction Properties
Abstract:
We define transfinite forms of consistency which admit analogues of Beklemishev’s reduction property. This leads to ordinal analyses of subsystems of Second-Order Arithmetic at various regions of the hyperarithmetic hierarchy, such as ACA_0^+. This is joint work with D. Fernández-Duque.

Speaker: Matthias Baaz
Title: Globally sound calculi and Andrew's Skolemization
Abstract:
In this lecture we describe LK+ and LK++ which are sound but admit certain unsound subderivations. These calculi are based on weakened Eigenvariable conditions. In general, Skolemization even in the cut-free case for LK+ and LK++ is only possible by the introduction of additional cuts. I contrast, Andrew's Skolemization allows for a a direct transformation for LK+ and LK++ proofs and an immediate Deskolemization into LK++. This explains, why it is so hard to transform eg resolution proofs with Andrew's Skolemization into LK-derivations: there is no elementary bound for the length of the corresponding cut-free LK-proof, cuts have to be introduced as in the soundness argument for LK+ and LK++ (joint work with Juan Aguilera using an idea of Stfan Hetzl concerning Andrew's Skolemization).

Speaker: Guillaume Burel
Title: Linking Focusing and Resolution with Selection
Abstract:
Focusing and selection are techniques that shrink the proof-search space for respectively sequent calculi and resolution. To bring out a link between them, we generalize them both: we introduce a sequent calculus where each occurrence of an atomic formula can have a positive or a negative polarity; and a resolution method where each literal, whatever its sign, can be selected in input clauses. We prove the equivalence between cut-free proofs in this sequent calculus and derivations of the empty clause in that resolution method. Such a generalization is not semi-complete in general, which allows us to consider complete instances that correspond to theories of any logical strength. We present three complete instances: first, our framework allows us to show that ordinary focusing corresponds to hyperresolution and semantic resolution; the second instance is deduction modulo theory and the related framework called superdeduction; and a new setting, not captured by any existing framework, extends deduction modulo theory with rewriting rules having several left-hand sides, which restricts even more the proof-search space.

Speaker: Jan Bydžovský
Title: The number of axioms
Abstract:
This is a join work with Juan P. Aguilera and Matthias Baaz. It is a classical result in first-order proof-theory that the number of steps in a cut-free sequent proof of a sequent S can not be bounded by an elementary function in terms of the size of S. But what about the number of axioms? We show that the same non-elementary lower bound holds for the number of different axioms in a cut-free proof of S.

Speaker: David M. Cerna
Title: An ordering for flexible and finite representation of infinite sequences of proofs
Abstract:
An early result concerning finite representation of infinite sequences of proofs was presented by J. R. Shoenfield's in a paper entitled "On a Restricted ω-Rule". In this paper a restriction of the ω-rule to sequences of proofs whose Gödel encoding can be described by a primitive recursive function was shown provability equivalent to the unrestricted ω-rule. Unfortunately, restricting the ω-rule in this way also restricts the variety of proofs which may be formulated. We present a formulation of primitive recursion developed specifically for the finite representation of infinite sequences of proofs without the need of an encoding of the sequences as a primitive recursive function. Rather we develop a so called call graph and decorate it with derivations constructed using a formal calculus (LK-calculus, resolution, etc.). Some properties of this system currently being investigated are, the extractability of Herbrand information, the capabilities of the approach with respect to inductive theorem proving, can such finitely represented proof allow cut-elimination for expressive fragments of arithmetic such as Σ2-induction.

Speaker: Gabriel Ebner
Title: Computational complexity of grammars for proofs with induction
Abstract:
Formal grammars are a versatile tool to analyze the Herbrand content of proofs. In this tradition, Eberhard and Hetzl 2015 assign grammars to proofs of universal statements containing an induction inference. For every instance of the universal statement, there is a language generated by this grammar, and this language is isomorphic to a Herbrand disjunction obtained via reductive cut-elimination. In this talk, we determine the complexity of various decision problems on such induction grammars: e.g. given two induction grammars, how difficult is it to compute whether one language is a subset of the other? These complexity results transfer to corresponding proof-theoretic problems about Herbrand sequents after cut- and induction-elimination.

Speaker: Eduardo Fermé
Title: Belief Change. Introduction and Overview
Abstract: It is an introductory talk. This talk was an attempt to summarize (in 45 minutes) the major developments in 30 years of AGM-inspired research.

Speaker: Marco Garapa
Title: Shielded Base Contractions
Abstract:
The one which is currently considered the standard model in the belief change literature is known as AGM model and has been originally presented in 1985. In that framework, each belief of an agent is represented by a sentence and the belief state of an agent is represented by a logically closed set of (belief-representing) sentences. These sets are called belief sets. Not long after its publication, several variants of that model started to appear in the literature. From among those proposals we highlight (for being the ones that are directly related to this lecture): (i) The use of sets of sentences not (necessarily) closed under logical consequence —the so-called belief bases— rather than belief sets to represent the belief states of an agent; (ii) Classes of, so-called, non-prioritized operators, which are operators that do not satisfy the success postulate. In this lecture we study a kind of non-prioritized contraction operator on belief bases —known as shielded base contractions. We present several classes of shielded base contractions and their axiomatic characterizations. Additionally we present the interrelations (in the sense of inclusion) among all those classes.

Speaker: Laura Kovacs
Title: Verifying Relational Properties using Trace Logic
Abstract:
We present a logical framework for the verification of relational properties in imperative programs. Our work is motivated by relational properties which come from security applications and often require reasoning about formulas with quantifier-alternations. Our framework reduces verification of relational properties of imperative programs to a validity problem into trace logic, an expressive instance of first-order predicate logic. Trace logic draws its expressiveness from its syntax, which allows expressing properties over computation traces. Its axiomatization supports fine-grained reasoning about intermediate steps in program execution, notably loop iterations. We present an algorithm to encode the semantics of programs as well as their relational properties in trace logic, and then show how first-order theorem proving can be used to reason about the resulting trace logic formulas. Our work is implemented in the tool Rapid and evaluated with examples coming from the security field. This is a joint work with Gilles Barthe, Renate Eilers, Pamina Georgiou, Bernhard Gleiss, and Matteo Maffei.

Speaker: Alexander Leitsch
Title: A Clausal Analysis of Cut-Elimination
Abstract:
The purpose of this talk is to illustrate the impact of resolution-based concepts to the analysis of cut-elimination methods in first-order logic. Gentzen's cut-elimination procedure consists in proof rewriting based on shifting of inferences and replacing cuts by others with lower logical complexity. In this talk we show that the Gentzen elimination method (without the axiom rule) is redundant in the following sense: given the characteristic clause set of an LK-proof p (denoted by CL(p)), as defined by the method CERES (cut-elimination by resolution), any Gentzen reduction step on a proof p yields a proof p' such that CL(p) subsumes CL(p'), for the common subsumption relation in automated deduction. Therefore, also for the atomic cut normal form p of p, we obtain that CL(p) subsumes CL(p). The construction of a CERES normal form of p is then obtained by computing a resolution refutation of CL(p) subsuming a standard resolution refutation of CL(p*). Subsumption and resolution can also be extended to cut-free proofs and thus to the CERES proof projections. This extension can be used to prove the completeness of intuitionistic CERES. It can be shown that resolution in CERES can be restricted to some kind of indexed resolution (which is complete for characteristic clause sets only); this refinement may turn out to be useful in practice by providing a strong compression of the search space for the correponding resolution theorem prover.

Speaker: Anela Lolic
Title: Herbrand Sequent Extraction
Abstract:
We present a method that extracts Herbrand sequents and expansion proofs from proofs without generating a normal form, i.e. a proof with at most quantifier-free cuts. The method is based on specific features of the CERES method, more precisely on the construction of a proof projection and a refutaion of the characteristic formula. Moreover, the method can be extended to a schematic setting, where induction is represented by the use of proof schemata. This is joint work with Alexander Leitsch and David Cerna.

Speaker: Dale Miller
Title: A proof theory for model checking and arithmetic
Abstract:
Linear logic has revealed a great deal about proofs in classical and intuitionistic logics. For example, Andreoli’s focused proof system for linear logic has been extended to focused proof systems for both classical and intuitionistic logics. Such proof systems provide both flexible normal forms of proofs and control on the structural rule of contraction. In this talk, I describe some initial work on moving such linear logic techniques from logic to both Peano and Heyting arithmetics. An initial step in this direction has been the recent work by Baelde where least and greatest fixed points have been added to MALL (multiplicative additive linear logic). The resulting logic and focused proof systems have been used to describe a proof theory behind model checking. Focusing proof systems for arithmetic have also been shown to form a basis for separating computation from deduction. I will also describe recent progress on applying lessons learned from linear logic to more conventional topics arithmetic.

Speaker: Mateus de Oliveira Oliveira
Title: On the Width of Regular Classes of Finite Structures
Abstract:
In this work, we introduce the notion of decisional width of a finite relational structure and the notion of regular-decisional width of a regular class of finite structures. Our main result states that the first-order theory of any regular-decisional class of finite structures is decidable. Building on the proof of this decidability result, we show that the problem of counting satisfying assignments for a first-order logic formula in a structure is fixed-parameter tractable when parameterized by the width parameter and can be solved in quadratic time with respect to the length of the input representation of the structure. This is joint work with Alexsander Andrade de Melo.

Speaker: Jakob Rath
Title: Subsumption Demodulation in First-Order Theorem Proving
Abstract:
Demodulation is an important simplification rule in saturation-based theorem proving that performs rewriting using unit equalities. However, in certain problem encodings, particularly ones coming from software verification, many useful equalities appear with side conditions. We present (forward) subsumption demodulation, a generalization of demodulation to non-unit clauses, and discuss its implementation in the theorem prover Vampire along with experimental results.

Speaker: Maurı́cio D. L. Reis
Title: On Multiple Belief Change
Abstract:
The central goal underlying the research area of logic of belief change (also known as belief revision) is the study of the changes which can occur in the belief state of a rational agent when he receives new information. The standard model of belief change was proposed by Alchourrón, Gärdenfors and Makinson in 1985 and is, nowadays, known as the AGM model. Assuming that the belief state of an agent is modeled by a theory (also known as belief set), i.e. a logically closed set of sentences, this framework essentially provides a definition for contractions - i.e. functions that receive a sentence (representing the new information received by the agent), and return a theory which is a subset of the original one that does not contain the received sentence. In this lecture we shall present some constructive definitions of theory contractions and discuss the generalization of those models to the case of multiple contraction.

Speaker: Andrei Voronkov
Title: Induction in Saturation-Based Proof Search
Abstract:
Many applications of theorem proving, for example program verification and analysis, require first-order reasoning with both quantifiers and theories such as arithmetic and datatypes. There is no complete procedure for reasoning in such theories but the state-of-the-art in automated theorem proving is still able to reason effectively with real-world problems from this rich domain. In this paper we contribute to a missing part of the puzzle: automated induction inside a saturation-based theorem prover.

Our goal is to incorporate lightweight automated induction in a way that complements the saturation-based approach, allowing us to solve problems requiring a combination of first-order reasoning, theory reasoning, and inductive reasoning. We implement a number of techniques and heuristics and evaluate them within the Vampire theorem prover. Our results show that these new techniques enjoy practical success on real-world problems.

Giles Reger (The University of Manchester)
Andrei Voronkov (EasyChair / The University of Manchester)