Computing interpolants in implicational logics
DOI10.1016/J.APAL.2005.12.014zbMath1103.03013OpenAlexW2086309981MaRDI QIDQ2503400
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
interpolationsubstructural logicnatural deductionintuitionistic logicGentzen systemsimply typed lambda-calculusimplicational logic
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)
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