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

  1. Agata Ciabattoni
    Goedel Logic and beyond: from Hypersequents to Parallel Computation
  2. 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.
  3. Didier Galmiche
    Multi-contextual structures and label-free calculi for Intuitionistic Modal Logics
    Slides.
  4. 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.
  5. 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.
  6. 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.
  7. 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.
  8. 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.
  9. 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.
  10. 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.
  11. Revantha Ramanayake
    On a syntactic proof of decidability for the logic of bunched implication BI
  12. 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.