View: session overviewtalk overview

**Invited Presentation**

**Speaker: **Gerwin Klein

09:00 | Scaling Formal Software Verification SPEAKER: Gerwin Klein |

**PC Dinner**

16:00 | A Contextual Logical Framework SPEAKER: unknown ABSTRACT. A new logical framework with explicit linear contexts and names is presented, with the purpose of enabling direct and flexible manipulation of contexts, both for representing systems and meta-properties. The framework is a conservative extension of the logical framework LF, and builds on linear logic and contextual modal type theory. We prove that the framework admits canonical forms, and that it possesses all desirable meta-theoretic properties, in particular hereditary substitutions. As proof of concept, we give an encoding of the one-sided sequent calculus for classical linear logic and the corresponding cut-admissibility proof, as well as an encoding of parallel reduction of lambda terms with the corresponding value-soundness proof. |

16:25 | Focused labeled proof systems for modal logic SPEAKER: unknown ABSTRACT. Focused proofs are sequent calculus proofs that group inference rules into alternating negative and positive phases. These phases can then be used to define macro-level inference rules from Gentzen's original and tiny introduction and structural rules. We show here that the inference rules of labeled proof systems for modal logics can similarly be described as pairs of such negative and positive phases within the LKF focused proof system (which contains no modal connectives). In particular, we consider the system G3K of Negri for the modal logic K and define a translation from labeled modal formulas into first-order polarized formulas and show a strict correspondence between derivations in the two systems, i.e., each rule application in G3K corresponds to a bipole - a pair of a positive and a negative phases - in LKF. Since geometric axioms (when properly polarized) induce bipoles, this strong correspondence holds for all modal logics whose Kripke frames are characterized by geometric properties. We extend these results to present a focused labeled proof system for this same class of modal logics and show its soundness and completeness. This resulting proof system allows one to define a rich set of normal forms of modal logic proofs. |

16:50 | A Labelled Sequent Calculus for Intuitionistic Public Announcement Logic SPEAKER: unknown ABSTRACT. Intuitionistic Public Announcement Logic (IntPAL) proposed by Ma et al. (2014) aims for a formal expression of change of knowledge in a constructive manner. IntPAL is a combination of Public Announcement Logic (PAL) by Plaza (1989) and the intuitionistic modal logic IK by Fischer Servi (1984) and Simpson (1994). We also refer to IK for the basis of this paper. Meanwhile, Nomura et al. (2015) provided a cut-free labelled sequent calculus based on the study of Maffezioli et al. (2010). In this paper, we introduce a labelled sequent calculus for IntPAL (we call it GIntPAL) as both an intuitionistic variant of GPAL and a public announcement extension of Simpson's labelled calculus, and show that all theorems of the Hilbert axiomatization of IntPAL are also provable in GIntPAL with the cut rule. Then we prove the admissibility of the cut rule in GIntPAL and also its soundness for birelational Kripke semantics. Finally, we derive the semantic completeness of GIntPAL as a corollary of these theorems. |

17:15 | Skolemization for Substructural Logics SPEAKER: Denisa Diaconescu ABSTRACT. The usual Skolemization procedure, which removes strong quantifiers by introducing new function symbols, is in general unsound for first-order substructural logics defined based on classes of complete residuated lattices. However, it is shown here (following similar ideas of Baaz and Iemhoff for first-order intermediate logics) that first-order substructural logics with a semantics satisfying certain witnessing conditions admit a "parallel" Skolemization procedure where a strong quantifier is removed by introducing a finite disjunction or conjunction (as appropriate) of formulas with multiple new function symbols. These logics typically lack equivalent prenex forms. Also, semantic consequence does not in general reduce to satisfiability. The Skolemization theorems presented here therefore take various forms, applying to the left or right of the consequence relation, and to all formulas or only prenex formulas. |

17:40 | Automated Theorem Proving by Translation to Description Logic SPEAKER: unknown ABSTRACT. Many Automated Theorem Proving (ATP) systems for different logics, and translators for translating different logics from one to another, have been developed and are now available. Some logics are more expressive than others, and it is easier to express problems in those logics. However, their ATP systems are relatively newer, and need more development and testing in order to solve more problems in a reasonable time. To benefit from the available tools to solve more problems in more expressive logics, different ATP systems and translators can be combined. Problems in logics more expressive than CNF can be translated directly to CNF, or indirectly by translation via intermediate logics. Description Logic (DL) sits between CNF and propositional logic. Saffron a CNF to DL translator, has been developed, which fills the gap between CNF and DL. ATP by translation to DL is now an alternative way of solving problems expressed in logics more expressive than DL, by combining necessary translators from those logics to CNF, Saffron, and a DL ATP system. |