Proof finding algorithms for implicational logics

DOI10.1016/S0304-3975(99)00174-7zbMath0972.03022MaRDI QIDQ1575928

Martin W. Bunder

Publication date: 23 August 2000

Published in: Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

natural deductionintuitionistic propositional logicrelevance logicsdecision proceduresmultiplicative linear logicimplicational fragmentsimplicative logicsaffine logicproof search algorithmrestriction on \(\lambda\)-terms

Mathematics Subject Classification ID

Related Items (4)

The decidability of a fragment of \(\text{BB}'\text{IW}\)-logic ⋮ Unnamed Item ⋮ Studying provability in implicational intuitionistic logic ⋮ Pre-grammars and inhabitation for a subset of rank 2 intersection types

Cites Work

• Unnamed Item
• Unnamed Item
• Intuitionistic propositional logic is polynomial-space complete
• BCK and BCI logics, condensed detachment and the 2-property
• Lambda terms definable as combinators
• Über Tautologien, in Welchen Keine Variable Mehr Als Zweimal Vorkommt

This page was built for publication: Proof finding algorithms for implicational logics