"Goal-directed proof theory" offers a unified and coherent methodology for automated deduction in non-classical logics. This methodology, based on goal-oriented reasoning, represents a generalization of the logic programming deduction style and is particularly advantageous for proof search. For the first time, this methodology is applied in a unified manner to a variety of non-classical systems, including intuitionistic, intermediate, modal, and substructural logics. The book also serves as an introduction to these logical systems from a procedural perspective. It is aimed at computer scientists, mathematicians, philosophers, and anyone interested in the automation of thinking based on non-classical logics. It is suitable for self-study, with the only prerequisite being a basic knowledge of logic and proof theory.