Computing interpolants in implicational logics

DOI10.1016/J.APAL.2005.12.014zbMath1103.03013OpenAlexW2086309981MaRDI QIDQ2503400

Makoto Kanazawa

Publication date: 14 September 2006

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.apal.2005.12.014

zbMATH Keywords

interpolationsubstructural logicnatural deductionintuitionistic logicGentzen systemsimply typed lambda-calculusimplicational logic

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Interpolation, preservation, definability (03C40) Subsystems of classical logic (including intuitionistic logic) (03B20) Combinatory logic and lambda calculus (03B40)

Related Items (1)

On the recognizing power of the Lambek calculus with brackets

Cites Work

• Interpolants, cut elimination and flow graphs for the propositional calculus
• Principal types of BCK-lambda-terms
• A cut-elimination proof in intuitionistic predicate logic
• Interpolation property for bicartesian closed categories
• Untersuchungen über das logische Schliessen. I
• On an interpretation of second order quantification in first order intuitionistic propositional logic
• Product-free Lambek calculus and context-free grammars
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Computing interpolants in implicational logics