A new machine-checked proof of strong normalisation for display logic

MaRDI QIDQ2843910zbMATH OpenFDO

Authors Rajeev Goré, Jeremy E. Dawson

Publication date 27 August 2013

Full work available at URL http://www.sciencedirect.com/science/article/pii/S1571066104810041

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Cut-elimination and normal-form theorems (03F05)

Recommendations

• Machine-checked interpolation theorems for substructural logics using display calculi
• On strong normalization in proof-graphs for propositional logic
• A unified display proof theory for bunched logic
• A verified proof checker for higher-order logic
• scientific article; zbMATH DE number 1301758
• scientific article; zbMATH DE number 1405619
• A direct proof of strong normalization for full constructive second-order logic
• A new technique for verifying and correcting logic programs
• On correctness of normal logic programs
• scientific article; zbMATH DE number 2085284

Cited in

(6)

• Some general results about proof normalization
• Hypersequent and display calculi -- a unified perspective
• Embedding display calculi into logical frameworks: Comparing Twelf and Isabelle
• Machine-checked interpolation theorems for substructural logics using display calculi
• scientific article; zbMATH DE number 1301758 (Why is no real title available?)
• scientific article; zbMATH DE number 1927419 (Why is no real title available?)

Describes a project that uses

Uses Software

• Isabelle/HOL

This page was built for publication: A new machine-checked proof of strong normalisation for display logic

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