Dissertation, Technischen Universität Wien (2021)

Abstract
This thesis introduces the "method of structural refinement", which serves as a means of transforming the relational semantics of a modal and/or constructive logic into an 'economical' proof system by connecting two proof-theoretic paradigms: labelled and nested sequent calculi. The formalism of labelled sequents has been successful in that cut-free calculi in possession of desirable proof-theoretic properties can be automatically generated for large classes of logics. Despite these qualities, labelled systems make use of a complicated syntax that explicitly incorporates the semantics of the associated logic, and such systems typically violate the subformula property to a high degree. By contrast, nested sequent calculi employ a simpler syntax and adhere to a strict reading of the subformula property, making such systems useful in the design of automated reasoning algorithms. However, the downside of the nested sequent paradigm is that a general theory concerning the automated construction of such calculi (as in the labelled setting) is essentially absent, meaning that the construction of nested systems and the confirmation of their properties is usually done on a case-by-case basis. The refinement method connects both paradigms in a fruitful way, by transforming labelled systems into nested (or, refined labelled) systems with the properties of the former preserved throughout the transformation process. To demonstrate the method of refinement and some of its applications, we consider grammar logics, first-order intuitionistic logics, and deontic STIT logics. The introduced refined labelled calculi will be used to provide the first proof-search algorithms for deontic STIT logics. Furthermore, we employ our refined labelled calculi for grammar logics to show that every logic in the class possesses the effective Lyndon interpolation property.
Keywords proof theory  structural refinement  grammar logic  interpolation  intuitionistic logic  first-order logic  reachability rule  propagation rule  nested calculus  labelled calculus  decidability
Categories (categorize this paper)
Options
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

 PhilArchive page | Other versions
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

From Display to Labelled Proofs for Tense Logics.Agata Ciabattoni, Tim Lyon & Revantha Ramanayake - 2018 - In Anil Nerode & Sergei Artemov (eds.), Logical Foundations of Computer Science. Springer International Publishing. pp. 120 - 139.

Add more references

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles

From Display to Labelled Proofs for Tense Logics.Agata Ciabattoni, Tim Lyon & Revantha Ramanayake - 2018 - In Anil Nerode & Sergei Artemov (eds.), Logical Foundations of Computer Science. Springer International Publishing. pp. 120 - 139.
Proof Analysis in Intermediate Logics.Roy Dyckhoff & Sara Negri - 2012 - Archive for Mathematical Logic 51 (1-2):71-92.
Labelled Non-Classical Logics.Luca Viganò - 2000 - Boston, MA, USA: Kluwer Academic Publishers.
Intuitionistic Hybrid Logic.Torben Braüner & Valeria de Paiva - 2006 - Journal of Applied Logic 4 (3):231-255.
Interpolation in Fragments of Classical Linear Logic.Dirk Roorda - 1994 - Journal of Symbolic Logic 59 (2):419-444.
Proof Analysis: A Contribution to Hilbert's Last Problem.Sara Negri & Jan von Plato - 2011 - Cambridge and New York: Cambridge University Press.

Analytics

Added to PP index
2021-10-09

Total views
29 ( #379,902 of 2,455,621 )

Recent downloads (6 months)
29 ( #26,273 of 2,455,621 )

How can I increase my downloads?

Downloads

My notes