Wednesday 15 November
9:50 Invited talk: Gian Luca Pozzato
10:50 Coffe break
11:15 Marianna Girlando
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
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
restaurant, O'2 Pointus
Friday 17 November
10:00 Agata Ciabattoni
10:45 Coffe break
11:10 Luigi Santocanale
11:55 End of session
List of talks
Goedel Logic and beyond: from Hypersequents to Parallel Computation
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).
Multi-contextual structures and label-free calculi for Intuitionistic
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).
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).
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.
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).
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.
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).
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.
On a syntactic proof of decidability for the logic of bunched
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.