Generic Methods for Formalising Sequent Calculi Applied to Provability Logic

DOI10.1007/978-3-642-16242-8_19zbMath1307.03033MaRDI QIDQ4933310

Rajeev Goré, Jeremy E. Dawson

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

zbMATH Keywords

proof theory; provability logic; interactive theorem proving; cut admissibility

Mathematics Subject Classification ID

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

• Isabelle/HOL
• Abella