From 2-Sequents and Linear Nested Sequents to Natural Deduction for Normal Modal Logics
| Autor: | Simone Martini, Andrea Masini, Margherita Zorzi |
|---|---|
| Přispěvatelé: | Department of Computer Science and Engineering [Bologna] (DISI), Alma Mater Studiorum Università di Bologna [Bologna] (UNIBO), Foundations of Component-based Ubiquitous Systems (FOCUS), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Dipartimento di Informatica - Scienza e Ingegneria [Bologna] (DISI), Alma Mater Studiorum Università di Bologna [Bologna] (UNIBO)-Alma Mater Studiorum Università di Bologna [Bologna] (UNIBO), Dipartimento di Informatica, Università degli Studi di Verona, Università degli studi di Verona = University of Verona (UNIVR), Martini S., Masini A., Zorzi M. |
| Jazyk: | angličtina |
| Rok vydání: | 2021 |
| Předmět: |
Normalization (statistics)
FOS: Computer and information sciences Computer Science - Logic in Computer Science Reduction (recursion theory) General Computer Science Logic linear nested sequents [INFO.INFO-GL]Computer Science [cs]/General Literature [cs.GL] 0102 computer and information sciences Consistency (knowledge bases) Intuitionistic logic intuitionistic logic 01 natural sciences Theoretical Computer Science Computer Science::Logic in Computer Science Accessibility relation Natural deduction normalization intuitionistic logic 2-sequents linear nested sequents 0101 mathematics natural deduction Mathematics Natural deduction [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL] 010102 general mathematics [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] 2-sequents 2-sequent Formal system Logic in Computer Science (cs.LO) Algebra linear nested sequent Computational Mathematics Mathematics::Logic Modal TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES normalization 010201 computation theory & mathematics TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS F.4.1 03B22 03B45 03F05 |
| Zdroj: | ACM Transactions on Computational Logic ACM Transactions on Computational Logic, Association for Computing Machinery, 2021, 22 (3), pp.1-29. ⟨10.1145/3461661⟩ ACM Transactions on Computational Logic, 2021, 22 (3), pp.1-29. ⟨10.1145/3461661⟩ |
| ISSN: | 1529-3785 1557-945X |
| DOI: | 10.1145/3461661⟩ |
| Popis: | International audience; We extend to natural deduction the approach of Linear Nested Sequents and of 2-Sequents. Formulas are decorated with a spatial coordinate, which allows a formulation of formal systems in the original spirit of natural deduction: only one introduction and one elimination rule per connective, no additional (structural) rule, no explicit reference to the accessibility relation of the intended Kripke models. We give systems for the normal modal logics from K to S4. For the intuitionistic versions of the systems, we define proof reduction, and prove proof normalization, thus obtaining a syntactical proof of consistency. For logics K and K4 we use existence predicates (à la Scott) for formulating sound deduction rules. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|