Cut elimination for GLS using the terminability of its regress process

DOI10.1007/S10992-015-9368-4MaRDI QIDQ288243zbMATH OpenOpenAlexFDO

Authors Jude Brighton

Publication date 25 May 2016

Published in Journal of Philosophical Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10992-015-9368-4

zbMATH Keywords

modal logiccut-eliminationGentzen-style logicGLregress trees

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Cut-elimination and normal-form theorems (03F05) Provability logics and related algebras (e.g., diagonalizable algebras) (03F45)

Recommendations

• Towards an algorithmic construction of cut-elimination procedures
• Sufficient conditions for cut elimination with complexity analysis
• scientific article; zbMATH DE number 1722668
• scientific article; zbMATH DE number 5872255
• scientific article; zbMATH DE number 1678397
• Cut-Elimination for SBL
• Cutting method for some multidimensional stationary problems
• Computer Aided Verification
• Degeneracy removal in cutting plane methods for disjoint bilinear programming
• Generalized \(\gamma\)-valid cut procedure for concave minimization

Cites work

• scientific article; zbMATH DE number 1497485 (Why is no real title available?)
• scientific article; zbMATH DE number 3241254 (Why is no real title available?)
• On some proof theoretical properties of the modal logic GL
• Provability interpretations of modal logic
• Solution of a problem of Leon Henkin
• The modal logic of provability. The sequential approach
• The modal logic of provability: cut-elimination
• Valentini's cut-elimination for provability logic resolved

Cited in

(7)

• Tautology elimination, cut elimination, and S5
• Cut-elimination for provability logic by terminating proof-search: formalised and deconstructed using Coq
• Valentini's cut-elimination for provability logic resolved
• Valentini's cut-elimination for provability logic resolved
• Cut elimination by unthreading
• A Syntactic Proof of Cut‐Elimination For GL_lin
• A proof theory for the logic of provability in true arithmetic

This page was built for publication: Cut elimination for GLS using the terminability of its regress process

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