Second FISP Meeting
Paris, June 8 to June 10, 2017
Overview
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".
Invited Speakers
Participants
Programme
Time |
Thursday 8 June 2017 |
09:00-9:30 |
Welcome and Coffee
|
9:30-10:30 |
Simona Ronchi Della Rocca: Proof normalisation and
approximation
|
10:30-10:45 |
Break
|
10:45-11:25 |
Giselle Reis: Ceres in intuitionistic logic
|
11:25-12:05 |
Francesco Genco: From hypersequents to parallel computation: Gödel logic and beyond
|
12:05-14:00 |
Lunch
|
14:00-15:00 |
Sergey Slavnov: Pomset logic and its generalizations: proof-nets and sequent calculus
|
15:00-15:30 |
Break
|
15:30-16:10 |
Andrea Aler-Tubella: Full decomposition: the rules that go through
|
16:10-16:50 |
Anupam Das: On the linear fragment of classical propositional logic
|
16:50-17:00 |
Break
|
17:00-17:40 |
Delia Kesner: Quantitative Types for the Lambda-Mu Calculus
|
17:40-19:30 |
Open discussion
|
19:30- |
Dinner
|
Time |
Friday 9 June 2017 |
09:00-9:30 |
Welcome and Coffee
|
9:30-10:30 |
Christian Retoré: From logical and linguistic generics to Hilbert's tau and epsilon quantifiers
|
10:30-10:45 |
Break
|
10:45-11:25 |
Juan P. Aguilera: The Infinite Epsilon Calculus
|
11:25-12:05 |
Kenji Miyamoto: Embedding Lemma in Epsilon Calculus with Equality
|
12:05-14:00 |
Lunch
|
14:00-15:00 |
Emmanuel Beffara: Describing processes and their interactions with proof theory
|
15:00-15:30 |
Break
|
15:30-16:10 |
Matthias Baaz: Gödel logics and the fully boxed fragment of LTL
|
16:10-16:50 |
Anela Lolic: A Sequent-Based Translation into the Epsilon Format
|
16:50-17:00 |
Break
|
17:00-17:40 |
David R. Sherratt: Towards an atomic abstract machine
|
17:40-19:30 |
Open discussion
|
Time |
Saturday 10 June 2017 |
09:00-9:30 |
Welcome and Coffee
|
9:30-10:30 |
Alessio Guglielmi: Proposal for a New Approach to Quantification
|
10:30-10:45 |
Break
|
10:45-11:25 |
Ulysse Gérard: Separating Functional Computation from Relations
|
11:25-12:05 |
Nicolas Guenot: Problems with proof systems for multi-conclusion logics
|
12:05-14:00 |
Lunch
|
14:00-19:30 |
Open discussion
|
Abstracts of
Talks
-
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
abstract tba
-
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
abstract tba
-
Anupam Das (Lyon)
Title: On the linear fragment of classical propositional logic
I will present a recent line of work, joint with Lutz Straßburger, on
the sound linear implications of classical propositional logic (CPL),
where variables may only occur once in the premiss and conclusion. This
fragment includes inferences such as 'switch' and 'medial' from deep
inference systems, and coincides with the 'multiplicative' fragment of
computability logic, due to Japaridze, and Blass' game semantics for
linear logic. Linear inferences already form a coNP-complete set, i.e.
they can express all of CPL, and our main result is that they admit no
sound complete axiomatisation by any polynomial-time decidable subset of
linear inferences, unless coNP=NP. The proof itself brings techniques
and invariants from graph theory and Boolean function theory to the
area, and constitutes a rich framework for reasoning about linear
inferences in general.
-
Francesco Genco (Vienna)
Title: From hypersequents to parallel computation: Gödel logic and beyond
abstract tba
-
Ulysse Gérard (Paris)
Title: Separating Functional Computation from Relations
The logical foundations of arithmetic generally start with a
quantificational logic of relations. Of course, one often wishes to
have a formal treatment of functions within this setting. Both
Hilbert and Church added to logic choice operators (such as the
epsilon operator) in order to coerce relations that happen to encode
functions into actual functions. Others have extended the term
language with confluent term rewriting in order to encode functional
computation as rewriting to a normal form. We take a different
approach that does not extend the underlying logic with either choice
principles or with an equality theory. Instead, we use the familiar
two-phase construction of focused proofs and capture functional
computation entirely within one of these phases. As a result, our
logic remains purely relational even when it is computing functions.
(joint work with Dale Miller)
-
Nicolas Guenot
Title: Problems with proof systems for multi-conclusion logics
I'll discuss in this talk different approaches to the design of proof systems
for multi-conclusion logics (eg. linear logic or classical logic), and comment
on their benefits and drawbacks, in particular when it comes to canonicity.
Then, I'll describe a work in progress attempting to establish a satisfactory
generalisation of natural deduction to the multi-conclusion setting.
-
Alessio Guglielmi (Bath)
Title: Proposal for a New Approach to Quantification
abstract tba
-
Delia Kesner (Paris)
Title: Quantitative Types for the Lambda-Mu Calculus
abstract tba
-
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
Herbrand disjunctions.
-
Kenji Miyamoto (Innsbruck)
Title: Embedding Lemma in Epsilon Calculus with Equality
abstract tba
-
Giselle Reis (Qatar)
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.
-
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
language
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.
-
Simona Ronchi Della Rocca (Turin)
Title: Proof normalisation and
approximation
abstract tba
-
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.
Venue
Organization