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 deduction; intuitionistic propositional logic; relevance logics; decision procedures; multiplicative linear logic; implicational fragments; implicative logics; affine logic; proof search algorithm; restriction on \(\lambda\)-terms
03B35: Mechanization of proofs and logical operations
03B47: Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics)
03B20: Subsystems of classical logic (including intuitionistic logic)
03B40: Combinatory logic and lambda calculus
Related Items
Studying provability in implicational intuitionistic logic, The decidability of a fragment of \(\text{BB}'\text{IW}\)-logic
Cites Work