Mechanising a Proof of Craig’s Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle

DOI10.1007/978-3-540-85110-3_5MaRDI QIDQ5505488zbMATHOpenAlexFDO

Authors Peter Chapman, James McKinna, Christian Urban

Publication date 27 January 2009

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-85110-3_5

zbMATH Keywords

logicautomated reasoningformal mathematicsnominal Isabelle

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Interpolation, preservation, definability (03C40)

Recommendations

• Machine-checked interpolation theorems for substructural logics using display calculi
• On Gabbay's proof of the Craig interpolation theorem for intuitionistic predicate logic
• Craig's interpolation theorem for the intuitionistic logic and its extensions - a semantical approach
• An institution-independent proof of Craig interpolation theorem
• A semantic approach to interpolation

Cites work

• scientific article; zbMATH DE number 512787 (Why is no real title available?)
• scientific article; zbMATH DE number 2003161 (Why is no real title available?)
• scientific article; zbMATH DE number 1497485 (Why is no real title available?)
• Automated Deduction – CADE-20
• Proof theory
• State of the Union: Type Inference Via Craig Interpolation
• Structural cut elimination. I: Intuitionistic and classical logic
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(4)

• Using theory interpretation to mechanise the reals in a theorem prover
• On Gabbay's proof of the Craig interpolation theorem for intuitionistic predicate logic
• Formalized proof systems for propositional logic
• Machine-checked interpolation theorems for substructural logics using display calculi

Describes a project that uses

Uses Software

• Isabelle
• Nominal Isabelle

This page was built for publication: Mechanising a Proof of Craig’s Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle

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