Proof finding algorithms for implicational logics (Q1575928)

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.