ИСТИНА

This paper is a result of the analysis of the efficiency of natural deduction proof search and the major weaknesses affecting it. We introduce new analytic strategies based on a new concept "Truth Set of Support". We present a combined proof search algorithm for classical propositional logic where a crucially new step is the guidance of the searching procedure by "Truth sets of Support" and establish the correctness. We describe the implementation of this new search technique and exemplify its advantages on the strong version of the Pigeon Hole Principle.