Duals of intuitionistic tableaus

The paper extends definitions and results of the method of tableaus, known for the classical logic, to intuitionistic logical systems. In particular, in classical proof theory (where a duality is available), it is easy to define dual tableaus and to prove their completeness. Within intuitionistic logic the tableaus (for signed formulas) were introduced by Fitting, who proved their completeness with respect to Kripke models. Here, we introduce dual intuitionistic tableaus (and dual Hintikka collections), and prove, following Fitting's method, their (adequacy and) completeness with respect to Kripke models