Proof finding algorithms for implicational logics
Logics considered here include implicational fragments of intuitionistic propositional logic, relevance logics \(R_{\rightarrow}\), \(T_{\rightarrow}\) and \(T_{\rightarrow}-W\), multiplicative linear logic and affine logic. For each of them a restriction on \(\lambda\)-terms providing an equivalent natural deduction formulation is stated, then a corresponding proof search algorithm is described.
scientific article; zbMATH DE number 1495205