Coinductive proof search for polarized logic with applications to full intuitionistic propositional logic

José Espírito Santo, Ralph Matthes, Luís Pinto

The approach to proof search dubbed "coinductive proof search" (CoIPS), and previously developed by the authors for implicational intuitionistic logic, is in this paper extended to…