Second FISP Meeting
Paris, June 8 to June 10, 2017
The FISP project is part of a long-term, ambitious project whose objective is to apply the powerful and promising techniques from structural proof theory to central problems in computer science for which they have not been used before, especially the understanding of the computational content of proofs, the extraction of programs from proofs and the logical control of refined computational operations.
The purpose of this second meeting is to discuss recent advances made the participants of
the "FISP project".
Juan P. Aguilera (Vienna)
Title: The Infinite Epsilon Calculus
We outline the general theory of the Epsilon Calculus for formulae of
infinite length, including its connection to various set-theoretic principles.
Andrea Aler-Tubella (Paris)
Title: Full decomposition: the rules that go through
Matthias Baaz (Vienna)
Title: Gödel logics and the fully boxed fragment of LTL
In this lecture we show that a very basic fragment of FO-LTL, the monadic
fully boxed fragment (all connectives and quantifiers are guarded by P) is not
recursively enumerable wrt validity and 1-satisfiability if three predicates are
present. This result is obtained by reduction of the fully boxed fragment of FO-LTL
to the Gödel logic G↓, the infinitely valued Gödel logic with truth values in
[0,1] such that all but 0 are isolated. The result on 1-satisfiability is in no way
symmetric to the result on validity as in classical logic: this is demonstrated by
the analysis of G↑, the related infinitely-valued Gödel logic with truth values in
[0, 1] such that all but 1 are isolated. Validity of the monadic fragment with at
least two predicates is not recursively enumerable, 1-satisfiability of the monadic
fragment is decidable. (joint work with Norbert Preining)
Emmanuel Beffara (Marseille)
Title: Describing processes and their interactions with proof theory
Francesco Genco (Vienna)
Title: From hypersequents to parallel computation: Gödel logic and beyond
Alessio Guglielmi (Bath)
Title: Proposal for a New Approach to Quantification
Delia Kesner (Paris)
Title: Quantitative Types for the Lambda-Mu Calculus
Anela Lolic (Vienna)
Title: A Sequent-Based Translation into the Epsilon Format
The optimal calculation of Herbrand disjunctions from unformalized or formalized mathematical
proofs is one of the most prominent problems of computational proof theory. 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.
We show how to connect epsilon proofs and sequent calculus derivations with cuts. This leads to
an improved notation for the epsilon formalism and a computationally improved version of the
Extended First Epsilon Theorem, which allows a nonelementary speed-up of the computation of
Kenji Miyamoto (Innsbruck)
Title: Embedding Lemma in Epsilon Calculus with Equality
Christian Retoré (Montpellier)
Title: From logical and linguistic generics to Hilbert’s tau and epsilon quantifiers
With our starting point being (universal) generics appearing in both natural
and mathematical proofs, and were further conceptualised in philosophy of language,
we introduce the tau subnector that maps a formula F to an individual term τx F
such that F (τx F ) whenever ∀xF .
We then in-troduce the dual subnector εxF which expresses the existential
quantification since F(εxF) ≡ ∃xF,
and describe its use for the semantics of indefinite and definite noun phrases.
Some logical and linguistic properties of this intriguing way to express
quantification are discussed.
David R. Sherratt (Bath)
Title: Towards an atomic abstract machine
The atomic lambda calculus is the computational interpretation of a intuitionistic
logical system with deep inference and is known for its efficiency when evaluating
terms; it is naturally fully lazy. This calculus implements full laziness through
the distributor construct, which can also be seen as the Curry-Howard
correspondence of one inference rule in said system. Abstract machines are used to
administer evaluation strategies. We discuss the idea and issues of developing an
abstract machine for the atomic lambda calculus, which mainly involve locating free
variables. We shall also discuss a variant of the calculus which overcomes these
problems, which involves the use of director strings; a mechanism used to keep
track of free variables in a term by annotating every subterm.
Sergey Slavnov (Moscow)
Title: Pomset logic and its generalizations: proof-nets and sequent calculus
We discuss noncommutative extensions of linear logic, namely, pomset logic and recently discovered semicommutative linear
logic, in which noncommutative multiplicative connectives are no longer self-dual. (The latter is not to be confused with quite
different noncommutative linear logic of Abrusci & Ruet.) These logics are defined by means of specific proof-nets, and pomset logic
appears as a certain degeneration of the other one. We introduce then ``decorated” sequent calculi for these logics, which are sound and
complete. In particular, we get a (sort of) sequent calculus formalization of pomset logic, and this is one of the key results.