License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2022.2
URN: urn:nbn:de:0030-drops-162834
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16283/
Go to the corresponding LIPIcs Volume Portal

Tiu, Alwen

A Methodology for Designing Proof Search Calculi for Non-Classical Logics (Invited Talk)

pdf-format:
LIPIcs-FSCD-2022-2.pdf (0.5 MB)

Abstract

In this talk I present a methodology for designing proof search calculi for a wide range of non-classical logics, such as modal and tense logics, bi-intuitionistic (linear) logics and grammar logics. Most of these logics cannot be easily formalised in the traditional Gentzen-style sequent calculus; various structural extensions to sequent calculus seem to be required. One of the more expressive extensions of sequent calculus is Belnap’s display calculus, which allows one to formalise a very wide range of logics and which provides a generic cut-elimination method for logics formalised in the calculus. The generality of display calculus derives partly from the pervasive use of structural rules to capture properties of the underlying semantics of the logic of interest, such as various frame conditions in normal modal logics, that are not easily captured by introduction rules alone. Unlike traditional sequent calculi, the subformula property in display calculi does not typically give an immediate bound on the search space (assuming contraction is absent) in proof search, as new structures may be created and their creation may not be driven by any introduction rules for logical connectives. This line of work started out as an attempt to "tame" display calculus, to make it more proof search friendly, by eliminating or restricting the use of structural rules. Two key ideas that make this possible are the adoption of deep inference, allowing inference rules to be applied inside a nested structure, and the use of propagation rules in place of structural rules. A brief survey of the applications of this methodology to a wide range of logics is presented, along with some directions for future work.

BibTeX - Entry

@InProceedings{tiu:LIPIcs.FSCD.2022.2,
  author =	{Tiu, Alwen},
  title =	{{A Methodology for Designing Proof Search Calculi for Non-Classical Logics}},
  booktitle =	{7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
  pages =	{2:1--2:4},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-233-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{228},
  editor =	{Felty, Amy P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2022/16283},
  URN =		{urn:nbn:de:0030-drops-162834},
  doi =		{10.4230/LIPIcs.FSCD.2022.2},
  annote =	{Keywords: Proof theory, Sequent calculus, Display calculus, Nested sequent calculus, Deep inference}
}

Keywords: Proof theory, Sequent calculus, Display calculus, Nested sequent calculus, Deep inference
Collection: 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)
Issue Date: 2022
Date of publication: 28.06.2022

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI