# Program

### Wednesday 15 November

9:30 Welcome

9:50 Invited talk: Gian Luca Pozzato

10:50 Coffe break

11:15 Marianna Girlando

12:00 Lunch

14:00 Tiziano Dalmonte

14:45 Tym Lyon

15:30 Coffee break

15:45 Didier Galmiche

16:30 Busisness meeting

17:20 End of session

### Thursday 16 November

9:50 Invited talk: Marcus Kracht

10:50 Coffe break

11:15 Pierre Kimmel

12:00 Lunch

14:00 Dominique Larchey-Wendling

14:45 Denis Lugiez

15:30 Coffee break

15:45 Revantha Ramanayake

16:30 Working session

17:20 End of session

20:00 Workshop Dinner
at CNTL
restaurant, O'2 Pointus

### Friday 17 November

10:00 Agata Ciabattoni

10:45 Coffe break

11:10 Luigi Santocanale

11:55 End of session

12:00 Lunch

### List of talks

Agata Ciabattoni

Goedel Logic and beyond: from Hypersequents to Parallel Computation

Tiziano Dalmonte

Semantic based labelled sequent calculi for non-normal modal logics

We present some external calculi for the basic non-normal modal
logics. All calculi are cut-free, sound and complete with respect to
the corresponding semantic. The calculi are also terminating and we
conjecture of optimal complexity. Moreover we show that some existing
internal calculi for the same logics can be easily translated into our
ones. We highlight some open problems and directions of research.
(Joint work with Nicola Olivetti and Sara Negri).

Slides.

Didier Galmiche

Multi-contextual structures and label-free calculi for Intuitionistic
Modal Logics

Slides.

Marianna Girlando

Equivalence between internal and labelled sequent calculi for Lewis' conditional logic V

We take into account logic V, the basic system of Lewis' family of
counterfactual conditional logics. This logic extends the language of
classical propositional logic by means of the comparative plausibility
operator "A is at least as plausible as B". Comparative plausible is
equivalent to counterfactual conditional, but simpler to treat. An
internal sequent caculus for V was presented in Girlando, Lellmann,
Pozzato and Olivetti (2016). We introduce a labelled sequent calculus
for the system, on the basis of Negri and Olivetti (2015); the
calculus is sound, complete and cut-free. We show how the two calculi
are equivalent, providing a translation from the internal to the
labelled sequent calculus and an inverse translation in the other
direction. The equivalence result is particularly interesting since by
their mutual correspondence we acheive a better understanding of both
the internal and the external calculus, and a deeper insight of the
derivations construction in both calculi. (Joint work with Sara Negri
and Nicola Olivetti).

Slides.

Pierre Kimmel

Internalizing labels in BI logics

Introduced by Arthur Prior and developed by Patrick Blackburn,
hybrid logics are extensions of modal logics (especially temporal
ones) where the syntax allows to anchor a formula to a specific
modal world. We propose a similar work on BI logic where additional
symbols anchor formulae to specific resources. This addition not
only extends expressiveness in a very practical way, but it also
leads to an axiomatization of several BI variants with the same
syntax and semantics. Finally, we propose a tableaux method
to reason on this new logic. (Joint work with Didier Galmiche).

Slides.

Marcus Kracht

Reduction functions

Given an axiomatic extension L + P of a modal logic L the problem of derivability in L + P can be reduced to derivability in L as follows. Q is a theorem of L + P iff there is a finite set f(Q) of theorems of L + P such that Q follows from f(Q) in L. The map sending Q to f(Q) is called a reduction function. If f is effective then decidability of L + P follows from decidability of L. In this talk I shall give an overview of the background and uses of reduction functions.

Slides.

Dominique Larchey-Wendling

Constructive decision via redundance-free proof-search

We describe a generic method to establish constructive decidability of a logic
when that logic can be represented within the framework of redundancy-free proof-search.
A redundancy relation is a binary relation between sequents: typically, a sequent T
is redundant over a sequent S if S can be obtained from T by repeated contractions.
When redundancy is well-chosen, it may satisfy the two following properties:

(a) Curry's lemma: any proof of a sequent T redundant over S
can be "contracted" into a proof of S;

(b) Kripke's lemma: redundancy is a well quasi order (WQO).

In case where both (a) and (b) are satisfied, we build a constructive
decision algorithm for the corresponding logic in the form of a mechanized
Coq term. We illustrate this result with the cases of implicational intuitionistic
logic and implicational relevance logic. This positively solves some questions
about finding constructive decision procedures for relevance logic (Riche 2005).

Slides.

Tym Lyon

From Labelled to Display Proofs for Tense Logics

An effective translation is introduced for transforming proofs in a display calculus to proofs in a labelled calculus for tense logics. The labelled proofs in the image of the translation are shown to consist of labelled sequents whose underlying directed graph possesses certain properties. Proofs of formulae in the labelled calculus G3Kt for the tense logic Kt are shown to be precisely those in the image of the translation.

Slides.

Denis Lugiez

On Symbolic Heaps Modulo Permission Theories

We address the entailment problem for separation logic with symbolic
heaps admitting list predicates and permissions for memory cells
that are essential to express ownership of a heap region. In the
permission-free case, the entailment problem is known to be in P.
Herein, we design new decision procedures for solving the
satisfiability and entailment problems that are parameterised by the
permission theories. This permits the use of solvers dealing with
the permission theory at hand, independently of the shape analysis.
We also show that the entailment problem without list predicates is
coNP-complete for several permission models, such as counting
permissions and binary tree shares but the problem is in P for
fractional permissions. Furthermore, when list predicates are
added, we prove that the entailment problem is coNP-complete when
the entailment problem for permission formulae is in coNP, assuming
the write permission can be split into as many read permissions as
desired. Finally, we show that the entailment problem for any
Boolean permission model with infinite width is
coNP-complete. (Joint work with S. Demri and E. Lozes).

Slides.

Gian Luca Pozzato

Proof Methods and Theorem Proving for nonclassical logics

In this talk I will recall proof methods (tableaux and sequent calculi) recently introduced for some nonclassical logics, in particular conditional and preferential logics. Conditional logics have a long history, and recently they have found interesting applications in several areas of artificial intelligence and knowledge representation, including belief revision and update, the representation of causal inferences in action planning, the formalization of hypothetical queries in deductive databases.
I will describe some theorem provers implementing such proof methods, inspired by the methodology of leanTAP: the idea is that each axiom or rule of the calculi is implemented by a Prolog clause of the program. The resulting code is therefore simple and compact. Loop-checking machineries are employed in order to obtain decision procedures for the logics under consideration, whereas heuristics and parallel computations are involved in order to improve the efficiency of the theorem provers.

Slides.

Revantha Ramanayake

On a syntactic proof of decidability for the logic of bunched
implication BI

Luigi Santocanale

Decidability of the equational theory of the natural join and the inner union

The natural join and the inner union operations combine relations of a database. Tropashko and Spight realized that these two operations are the meet and join operations in a class of lattices, known by now as the relational lattices. They proposed then lattice theory as an algebraic approach to the theory of databases, alternative to the relational algebra. Previous works proved that the quasiequational theory of these latticesâ€”that is, the set of definite Horn sentences valid in all the relational latticesâ€”is undecidable, even when the signature is restricted to the pure lattice signature. We shall expose the main ideas behind our proof that the equational theory of relational lattices is decidable.

Slides.