Prefixed tableaus and nested sequents

DOI10.1016/J.APAL.2011.09.004MaRDI QIDQ409323zbMATH OpenOpenAlexFDO

Authors Melvin Fitting

Publication date 13 April 2012

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.apal.2011.09.004

zbMATH Keywords

deep reasoningmodal logicnested sequentprefixed tableau

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Proof theory in general (including proof-theoretic semantics) (03F03) Structure of proofs (03F07)

Recommendations

• Nested sequents for intuitionistic logics
• Modular sequent systems for modal logic
• Sequentialising nested systems
• On nested sequents for constructive modal logics
• Proof search in nested sequent calculi

Cites work

• Deep sequent systems for modal logic
• Explicit provability and constructive semantics
• First-order intensional logic
• First-order modal logic
• Handbook of modal logic
• scientific article; zbMATH DE number 1114348 (Why is no real title available?)
• scientific article; zbMATH DE number 755666 (Why is no real title available?)
• scientific article; zbMATH DE number 1395652 (Why is no real title available?)
• scientific article; zbMATH DE number 3274715 (Why is no real title available?)
• Introducing Justification into Epistemic Logic
• Justification logic. Reasoning with reasons
• Proof analysis in modal logic
• Proof methods for modal and intuitionistic logics
• Single step tableaux for modal logics. Computational properties, complexity and methodology
• Strongly analytic tableaux for normal modal logics
• Tableau methods for modal and temporal logics
• Tableau methods of proof for modal logics
• Tableaux and Hypersequents for Justification Logic
• The logic of proofs, semantically

Cited in

(30)

• Reflecting on social influence in networks
• Maehara-style modal nested calculi
• Multicomponent proof-theoretic method for proving interpolation properties
• Efficient local reductions to basic modal logic
• Local is best: efficient reductions to modal logic \textsf{K}
• Local reductions for the modal cube
• Proofs and countermodels in non-classical logics
• \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments
• Nested sequents for intuitionistic logics
• Focused and Synthetic Nested Sequents
• Inducing syntactic cut-elimination for indexed nested sequents
• Nested sequent calculi for conditional logics
• Algebra, proof theory and applications for a logic of propositions, actions and adjoint modal operators
• On height and happiness
• Through an inference rule, darkly
• Labeled sequent calculus for justification logics
• Hypersequent rules with restricted contexts for propositional modal logics
• Linear Nested Sequents, 2-Sequents and Hypersequents
• Labeled sequent calculi for modal logics and implicit contractions
• Inducing syntactic cut-elimination for indexed nested sequents
• Modal interpolation via nested sequents
• Certification of prefixed tableau proofs for modal logic
• A general proof certification framework for modal logic
• Cut Elimination for Extended Sequent Calculi
• Tableaux and interpolation for propositional justification logics
• A natural deduction calculus for \textbf{S4.2}
• Refined tableau systems for some modal logics of confluence
• Nested sequent calculi for some modal logics with non-standard modalities
• Nested sequents or tree-hypersequents -- a survey
• Agent interpolation in distributed systems

This page was built for publication: Prefixed tableaus and nested sequents

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