The bounded proof property via step algebras and step frames
From MaRDI portal
Publication:741087
DOI10.1016/J.APAL.2014.07.005zbMATH Open1361.03013OpenAlexW2000108579MaRDI QIDQ741087FDOQ741087
Silvio Ghilardi, Nick Bezhanishvili
Publication date: 10 September 2014
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.2014.07.005
Recommendations
- Bounded proofs and step frames
- One-step Heyting algebras and hypersequent calculi with the bounded proof property
- Steps towards a proof-theoretical semantics
- Logic of Proofs for Bounded Arithmetic
- On Extending Bounded Proofs to Inductive Proofs
- Proving consistency of equational theories in bounded arithmetic
- On the provability logic of bounded arithmetic
- Axiomatizing proof tree concepts in bounded arithmetic
- scientific article; zbMATH DE number 2196511
- scientific article; zbMATH DE number 4006236
Modal logic (including the logic of norms) (03B45) Cut-elimination and normal-form theorems (03F05) Other algebras related to logic (03G25)
Cites Work
- Modal logic
- Structural proof theory. With an appendix by Aarne Ranta
- Admissibility of logical inference rules
- Canonical rules
- A unified semantic framework for fully structural propositional sequent systems
- Algebraic proof theory for substructural logics: cut-elimination and completions
- MacNeille completions of FL-algebras
- Model theory.
- Tools and techniques in modal logic
- Normal forms in modal logic
- Continuity, freeness, and filtrations
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- The modal logic of provability. The sequential approach
- Title not available (Why is that?)
- The modal logic of provability: cut-elimination
- Algorithmic correspondence and completeness in modal logic. I. The core algorithm SQEMA
- Gentzen calculi for modal propositional logic
- Bounded Proofs and Step Frames
- Correspondence between Modal Hilbert Axioms and Sequent Rules with an Application to S5
- Constructing Cut Free Sequent Systems with Context Restrictions Based on Classical or Intuitionistic Logic
- Title not available (Why is that?)
- From Frame Properties to Hypersequent Rules in Modal Logics
- Title not available (Why is that?)
- Title not available (Why is that?)
- Algorithmic correspondence and canonicity for distributive modal logic
- A uniform semantic proof for cut-elimination and completeness of various first and higher order logics.
- Algebraic aspects of cut elimination
- Modal frame correspondences and fixed-points
- Elementary canonical formulae: extending Sahlqvist's theorem
- Sahlqvist formulas in hybrid polyadic modal logics
- Kripke Semantics for Basic Sequent Systems
- Topology and duality in modal logic
- A Cook's Tour of the Finitary Non-Well-Founded Sets
- Sahlqvist correspondence for modal mu-calculus
- A new proof of Sahlqvist's theorem on modal definability and completeness
- Minimal predicates, fixed-points, and definability
- Title not available (Why is that?)
- An algebraic theory of normal forms
- Unified Correspondence
- A modal sequent calculus for a fragment of arithmetic
- On modal systems having arithmetical interpretations
- Elementary canonical formulae: a survey on syntactic, algorithmic, and model-theoretic aspects
- Finitely generated free Heyting algebras via Birkhoff duality and coalgebra
- Title not available (Why is that?)
- Cut Elimination for Shallow Modal Logics
- Free Modal Algebras: A Coalgebraic Perspective
- A Cut‐Free Calculus For Dummett's LC Quantified
- Title not available (Why is that?)
- The logic of transitive and dense frames: from the step-frame analysis to full cut-elimination
- Free Modal Algebras Revisited: The Step-by-Step Method
- On generalizing free algebras for a functor
Cited In (6)
- Algebraic proof theory: hypersequents and hypercompletions
- BOUNDED-ANALYTIC SEQUENT CALCULI AND EMBEDDINGS FOR HYPERSEQUENT LOGICS
- Lattice logic as a fragment of (2-sorted) residuated modal logic
- COMPLETE ADDITIVITY AND MODAL INCOMPLETENESS
- Modal translation of substructural logics
- Hypersequent rules with restricted contexts for propositional modal logics
Uses Software
This page was built for publication: The bounded proof property via step algebras and step frames
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q741087)
