Proof-search of propositional intuitionistic logic sequents by means of classical logic calculus

Abstract

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 LJ₀ can be checked by means of a propositional classical logic sequent calculus LK₀.