Proof finding algorithms for implicational logics
From MaRDI portal
Publication:1575928
DOI10.1016/S0304-3975(99)00174-7zbMath0972.03022MaRDI QIDQ1575928
Publication date: 23 August 2000
Published in: Theoretical Computer Science (Search for Journal in Brave)
natural deductionintuitionistic propositional logicrelevance logicsdecision proceduresmultiplicative linear logicimplicational fragmentsimplicative logicsaffine logicproof search algorithmrestriction on \(\lambda\)-terms
Mechanization of proofs and logical operations (03B35) Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Subsystems of classical logic (including intuitionistic logic) (03B20) Combinatory logic and lambda calculus (03B40)
Related Items
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