Proof-search of propositional intuitionistic logic sequents by means of classical logic calculus - Alonderis , Romas (Lietuvos matematikos rinkinys, 2008)
In the paper, we define some classes of sequents of the propositional intuitionistic logic. These are classes of primarily and α-primarily reducible sequents. Then we show how derivability of these sequents in a propositional intuitionistic logic sequent calculus LJ0 can be checked by means of a propositional classical logic sequent calculus LK0.