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

DOI10.1007/978-3-540-85110-3_5zbMATH Open1166.68340OpenAlexW2098316338MaRDI QIDQ5505488FDOQ5505488

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

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

zbMATH Keywords

logicautomated reasoningformal mathematicsnominal Isabelle

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• Tools and Algorithms for the Construction and Analysis of Systems
• Proof theory
• Automated Deduction – CADE-20
• Title not available (Why is that?)
• Structural cut elimination. I: Intuitionistic and classical logic
• Title not available (Why is that?)
• State of the Union: Type Inference Via Craig Interpolation

Cited In (4)

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

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)