Generic Methods for Formalising Sequent Calculi Applied to Provability Logic

DOI10.1007/978-3-642-16242-8_19zbMath1307.03033OpenAlexW1823478466MaRDI 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 theoryprovability logicinteractive theorem provingcut admissibility

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Provability logics and related algebras (e.g., diagonalizable algebras) (03F45)

Related Items (9)

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 ⋮ Formalized meta-theory of sequent calculi for linear logics ⋮ Machine-Checked Proof-Theory for Propositional Modal Logics ⋮ Formalized meta-theory of sequent calculi for substructural logics ⋮ Machine-Checked Interpolation Theorems for Substructural Logics Using Display Calculi ⋮ Mechanizing focused linear logic in Coq ⋮ A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systems ⋮ A focused linear logical framework and its application to metatheory of object logics

Uses Software

• Isabelle/HOL
• Abella

This page was built for publication: Generic Methods for Formalising Sequent Calculi Applied to Provability Logic