A formalization of Sambins's normalization for GL

DOI10.1002/MALQ.19930390116zbMath0803.03035OpenAlexW2111048265WikidataQ126258839 ScholiaQ126258839MaRDI QIDQ4304806

Edward Hermann Haeusler, Luiz Carlos Pereira

Publication date: 31 August 1994

Published in: Mathematical Logic Quarterly (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1002/malq.19930390116

zbMATH Keywords

sequent calculuscut-eliminationrecursive functiondecision proceduremodal logic of provabilitymechanization of proof proceduresnormalization theorem for GL

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Mechanization of proofs and logical operations (03B35) Cut-elimination and normal-form theorems (03F05) First-order arithmetic and fragments (03F30)

Cites Work

• Proof methods for modal and intuitionistic logics
• The modal logic of provability. The sequential approach
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A formalization of Sambins's normalization for GL