Generic Methods for Formalising Sequent Calculi Applied to Provability Logic
From MaRDI portal
Publication:4933310
DOI10.1007/978-3-642-16242-8_19zbMath1307.03033MaRDI QIDQ4933310
Publication date: 12 October 2010
Published in: Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)
Full work available at URL: http://hdl.handle.net/1885/20780
03F05: Cut-elimination and normal-form theorems
03F45: Provability logics and related algebras (e.g., diagonalizable algebras)
Related Items
A focused linear logical framework and its application to metatheory of object logics, Formalized meta-theory of sequent calculi for substructural logics, A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systems, A formally verified cut-elimination procedure for linear nested sequents for tense logic, Cut-elimination for provability logic by terminating proof-search: formalised and deconstructed using Coq, Mechanizing focused linear logic in Coq, Formalized meta-theory of sequent calculi for linear logics, Machine-Checked Interpolation Theorems for Substructural Logics Using Display Calculi, Machine-Checked Proof-Theory for Propositional Modal Logics
Uses Software