View: session overviewtalk overviewside by side with other conferences

09:00 | Automated Reasoning In Natural Language: Current Directions ABSTRACT. TBA |

10:00 | Evidence Extraction from Parameterised Boolean Equation Systems SPEAKER: Wieger Wesselink ABSTRACT. Model checking is a technique for automatically assessing the quality of software and hardware systems and designs. Given a formalisation of both the system behaviour and the requirements the system should meet, a model checker returns either a yes or a no. In case the answer is not as expected, it is desirable to provide feedback to the user as to why this is the case. Providing such feedback, however, is not straightforward if the requirement is expressed in a highly expressive logic such as the modal $\mu$-calculus, and when the decision problem is solved using intermediate formalisms. In this paper, we show how to extract witnesses and counterexamples from parameterised Boolean equation systems encoding the model checking problem for the first-order modal $\mu$-calculus. We have implemented our technique in the modelling and analysis toolset mCRL2 and showcase our approach on a few illustrative examples. |

11:00 | SPEAKER: Eugenio Orlandelli ABSTRACT. We introduce labelled sequent calculi for quantified modal logics with non-rigid and and non-denoting terms. We prove that these calculi have the good structural properties of G3-style calculi. In particular, all rules are height-preserving invertible, weakening and contraction are height-preserving admissible and cut is admissible. Finally, we show that each calculus gives a proof-theoretic characterization of validity in the corresponding class of models. |

11:30 | An Outline for Simple Semi-automated Proof Assistants for First-order Modal Logics ABSTRACT. Most theorem provers and proof assistants are written in imperative or functional programming languages. Recently, the claim that higher-order logic programming languages might be better suited for this task was revisited and a new interpreter, as well as new proof assistants based on it, were introduced. In this paper we follow these claims and describe a concise implementation of a prototype for a semi-automated proof assistant for first-order modal logic. The aim of this paper is to encourage the development of personal proof assistants and semi-automated provers for a variety of modal calculi. |

12:00 | Labelled Connection-based Proof Search for Multiplicative Intuitionistic Linear Logic SPEAKER: Didier Galmiche ABSTRACT. We propose a connection-based characterization for multiplicative intuitionistic linear logic (MILL) which is based on labels and constraints that capture Urquhart's possible worlds semantics of the logic. We briefly recall the purely syntactic sequent calculus for MILL, which we call LMILL and then propose a sound and complete labelled sequent calculus GMILL for MILL. We then show how to translate every LMILL proof into a GMILL proof. From this translation, refining our results on BI (The logic of Bunched Implications), we show the soundness of the connection-based characterization and its completeness without the need for any notion of multiplicity. |

14:00 | Going Beyond First-Order Logic with Vampire ABSTRACT. TBA |

16:00 | Formalization of a Paraconsistent Infinite-Valued Logic ABSTRACT. Classical logics are explosive -- from a contradiction everything follows. This is problematic e.g. when reasoning about contradictory evidence. In paraconsistent logics everything does not follow from a contradiction. In this paper, formalized proofs of two meta-theorems about a propositional fragment of a paraconsistent infinite-valued higher-order logic are presented. One implies that the validity of any formula can be decided by considering a finite number of truth values and evaluating the formula in all models over these. The other implies that there is no upper bound on the size of this finite set -- it depends on the number of propositional symbols in the formula. |

16:30 | System Demonstration: The Higher-Order Prover Leo-III SPEAKER: Alexander Steen ABSTRACT. The higher-order theorem prover Leo-III will be demonstrated. |

Workshops dinner at Magdalen College. Drinks reception from 7.15pm, to be seated by 7:45 (pre-booking via FLoC registration system required; guests welcome).