Machine-Checked Interpolation Theorems for Substructural Logics Using Display Calculi

DOI10.1007/978-3-319-40229-1_31zbMath1476.03007OpenAlexW2484729803MaRDI QIDQ2817943

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)

Related Items

A formally verified cut-elimination procedure for linear nested sequents for tense logic

Uses Software

• Isabelle/HOL

Cites Work

• Unnamed Item
• Harmonious logic: Craig's interpolation theorem and its descendants
• Display logic
• Craig Interpolation in Displayable Logics
• Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
• Machine Checking Proof Theory: An Application of Logic to Logic
• Generic Methods for Formalising Sequent Calculi Applied to Provability Logic
• Quantified Invariant Generation Using an Interpolating Saturation Prover

This page was built for publication: Machine-Checked Interpolation Theorems for Substructural Logics Using Display Calculi