Goal-Driven Inference Search in Classical Propositional Logic Alexander Lyaletski and Andrey Paskevich Kyiv, Ukraine Abstract Two goal-driven strategies for inference search in propositional logic are presented in the form of special sequent calculi. Some results on their soundness and completeness are given, and comparison of these calculi is made. It is shown that no one of them is preferable to another in the sense of constructing minimal inferences.