Focused and Synthetic Nested Sequents

DOI10.1007/978-3-662-49630-5_23MaRDI QIDQ2811354zbMATHOpenAlexFDO

Authors Kaustuv Chaudhuri, Sonia Marin, Lutz Straßburger

Publication date 10 June 2016

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-662-49630-5_23

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Cut-elimination and normal-form theorems (03F05)

Recommendations

• Focusing Strategies in the Sequent Calculus of Synthetic Connectives
• Focusing and higher-order abstract syntax
• Prefixed tableaus and nested sequents
• Grafting hypersequents onto nested sequents
• Nested sequents for intuitionistic logics
• scientific article; zbMATH DE number 7668098
• Nested sequent calculi for conditional logics
• A Focused Sequent Calculus for Higher-Order Logic
• scientific article; zbMATH DE number 2051680
• Modal interpolation via nested sequents

Cites work

• scientific article; zbMATH DE number 956466 (Why is no real title available?)
• A judgmental reconstruction of modal logic
• A logical characterization of forward and backward chaining in the inverse method
• A multi-focused proof system isomorphic to expansion proofs
• Axioms vs hypersequent rules with context restrictions: theory and applications
• Cut elimination in nested sequents for intuitionistic modal logics
• Cut-free sequent calculi for some tense logics
• Deep sequent systems for modal logic
• Display logic
• Focused labeled proof systems for modal logic
• Focused natural deduction
• Focusing Strategies in the Sequent Calculus of Synthetic Connectives
• Focusing and higher-order abstract syntax
• Focusing and polarization in linear, intuitionistic, and classical logics
• Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional Logic
• Label-free modular systems for classical and intuitionistic modal logics
• Logic Programming with Focusing Proofs in Linear Logic
• Modal logic for philosophers
• Modular focused proof systems for intuitionistic modal logics
• Prefixed tableaus and nested sequents
• Proof analysis in modal logic
• Proof search in nested sequent calculi
• Structural focalization
• The Method of Tree-Hypersequents for Modal Propositional Logic
• The focused calculus of structures
• Uniform proofs as a foundation for logic programming

Cited in

(12)

• Hypersequent rules with restricted contexts for propositional modal logics
• Reductive logic, proof-search, and coalgebra: a perspective from resource semantics
• Proof search in nested sequent calculi
• Focusing Strategies in the Sequent Calculus of Synthetic Connectives
• Modular focused proof systems for intuitionistic modal logics
• A general proof certification framework for modal logic
• Linking focusing and resolution with selection
• Grafting hypersequents onto nested sequents
• scientific article; zbMATH DE number 6863852 (Why is no real title available?)
• Focused proof-search in the logic of bunched implications
• MOIN: A Nested Sequent Theorem Prover for Intuitionistic Modal Logics (System Description)
• The focused calculus of structures

Describes a project that uses

Uses Software

• Imogen

This page was built for publication: Focused and Synthetic Nested Sequents

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2811354)