Machine-checked interpolation theorems for substructural logics using display calculi

DOI10.1007/978-3-319-40229-1_31MaRDI QIDQ2817943zbMATH OpenOpenAlexFDO

Authors James Brotherston, Rajeev Goré, Jeremy E. Dawson

Publication date 5 September 2016

Published in Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-40229-1_31

zbMATH Keywords

Craig interpolationdisplay logicinteractive theorem proving

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) Interpolation, preservation, definability (03C40) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Craig interpolation in displayable logics
• Mechanising a Proof of Craig’s Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle
• A new machine-checked proof of strong normalisation for display logic
• scientific article; zbMATH DE number 1927419
• scientific article; zbMATH DE number 2222017

Cites work

• Craig interpolation in displayable logics
• Display logic
• Generic methods for formalising sequent calculi applied to provability logic
• Harmonious logic: Craig's interpolation theorem and its descendants
• scientific article; zbMATH DE number 1927419 (Why is no real title available?)
• Machine Checking Proof Theory: An Application of Logic to Logic
• Quantified Invariant Generation Using an Interpolating Saturation Prover
• Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory

Cited in

(4)

• A formally verified cut-elimination procedure for linear nested sequents for tense logic
• A new machine-checked proof of strong normalisation for display logic
• Craig interpolation in displayable logics
• Mechanising a Proof of Craig’s Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle

Describes a project that uses

Uses Software

• Isabelle/HOL

This page was built for publication: Machine-checked interpolation theorems for substructural logics using display calculi

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