Session 9B

Chair: Jens Otten

• 16:30: Adam Pease. A Programmer’s Text Editor for a Logical Theory: The SUMOjEdit Editor (system description).     See abstract ...
  ABSTRACT. SUMOjEdit is a programmer’s text editor for the SUO-KIF language and SUMO theory. Modern procedural programming is done in a text editor with tool support. Development of ontologies and taxonomies has often been done in graphical editors, leading many developers to employ only logics of very limited expressiveness that can be manipulated visually. Developers in the theorem proving community typically work in text editors but without the same degree of tool support that most programmers rely on. Beginners working with SUMO make some very predictable errors in syntax, logical formulation, and use of the library of theories. Many of these errors can be flagged during editing, resulting in reduced time to become a productive developer. An editor designed for working with SUMO has the potential to aid beginners and experienced SUMO developers.
• 16:45: Giselle Reis, Zan Naeem, Mohammed Hashim. Sequoia: a playground for logicians (system description).     See abstract ...
  ABSTRACT. Sequent calculus is a pervasive technique for studying logics and their properties due to the regularity of rules, proofs, and meta-property proofs across logics. However, even simple proofs can be large, and writing them by hand is often messy. Moreover, the combinatorial nature of the calculus makes it easy for humans to make mistakes or miss cases. Sequoia aims to alleviate these problems.
  Sequoia is a web-based application for specifying sequent calculi and performing basic reasoning about them. The goal is to be a user-friendly program, where logicians can specify and "play" with their calculi. For that purpose, we provide an intuitive interface where inference rules can be input in LaTeX and are immediately rendered with the corresponding symbols. Users can then build proof trees in a streamlined and minimal-effort way, in whichever calculus they defined. In addition to that, we provide checks for some of the most important meta-theoretical properties, such as weakening admissibility and identity expansion, given that they proceed by the usual structural induction. In this sense, the logician is only left with the tricky and most interesting cases of each analysis.
• 17:00: Tiziano Dalmonte, Nicola Olivetti, Gian Luca Pozzato. HYPNO: Theorem Proving with Hypersequent Calculi for Non-Normal Modal Logics (system description).     See abstract ...
  ABSTRACT. We present HYPNO (HYpersequent Prover for NOn-normal modal logics), a Prolog-based theorem prover and countermodel generator for non-normal modal logics. HYPNO implements some hypersequent calculi recently introduced for the basic system E and its extensions with axioms M, N, and C. It is inspired by the methodology of LeanTAP, so that it does not make use of any ad-hoc control mechanism. Given a formula, HYPNO provides either a proof in the calculus or a countermodel, directly built from an open saturated branch. Preliminary experimental results show that the performances of HYPNO are very promising with respect to other theorem provers for the same class of logics.
• 17:15: Marianna Girlando, Lutz Straßburger. Moin: A Nested Sequent Theorem Prover for Intuitionistic Modal Logics (system description).     See abstract ...
  ABSTRACT. We present a simple Prolog prover for intuitionistic modal logics based on nested sequent proof systems. We have implemented single-conclusion (Genzten-style) nested sequent systems and multi-conclusion nested sequent systems (Maehara-style) for all logics in the intuitionistic modal IS5-cube. While the single-conclusion system are better investigated and have an internal cut-elimination, the multi-conclusion systems can provide a counter model in case the proof search fails. To our knowledge this is the first automated theorem prover for intuitionistic modal logics. For wider usability of our system, we also implemented all classical normal modal logics in the S5-cube.
• 17:30: Anne Baanen. A Lean tactic for normalising ring expressions with exponents (short paper).     See abstract ...
  ABSTRACT. This paper describes the design of the normalising tactic ring_exp for the Lean prover. This tactic improves on existing tactics by extending commutative rings with a binary exponent operator. An inductive family of types represents the normal form, enforcing various invariants. The design can also be extended with more operators.
• 17:45: Michael Kohlhase, Florian Rabe, Claudio Sacerdoti Coen, Jan Frederik Schaefer. Logic-Independent Proof Search in Logical Frameworks (short paper).     See abstract ...
  ABSTRACT. Logical frameworks enable prototyping and analyzing logical systems as well as developing logic-independent implementations. An important question is to what extent the latter can include a logic-independent automated theorem prover. On the one hand, many theorem proving innovations can be generalized to much larger classes of logics than they were originally developed for. On the other hand, most practically competitive provers critically use logic-specific optimizations. Indeed, logical framework-induced fully logic-independent proof support is generally limited to proof checking and simple search.
  In order to investigate this question more deeply, we build a suite of highly modular definitions of a variety of logics in a logical framework and generate Prolog-based theorem provers for each of them. We emphasize generality of the method and try to avoid taking any logic-specific knowledge into account. Our generated provers support natural deduction proof search, including back-chaining, as well as tableau provers and model generators. Even though these efforts have only just started, we are already able to use the latter in a system for natural language understanding that combines grammatical with semantic processing.