scientific article; zbMATH DE number 7668109

MaRDI QIDQ5884958zbMATH OpenFDO

Authors Rajeev Goré, Ian Shillito

Publication date 24 March 2023

zbMATH Keywords

backward proof-searchcut eliminationinteractive theorem provingintuitionistic provability logicproof theory

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Cut-elimination and normal-form theorems (03F05) Provability logics and related algebras (e.g., diagonalizable algebras) (03F45)

Recommendations

• The modal logic of provability: cut-elimination
• Admissibility of structural rules for contraction-free systems of intuitionistic logic
• Structural cut elimination. I: Intuitionistic and classical logic
• Valentini's cut-elimination for provability logic resolved
• Sequent calculi for intuitionistic Gödel-Löb logic

Cited in

(3)

• Valentini's cut-elimination for provability logic resolved
• Valentini's cut-elimination for provability logic resolved
• Intuitionistic Gödel-Löb logic, à la Simpson: labelled systems and birelational semantics

This page was built for publication:

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