Goal Directed Proof Theory presents a uniform and coherent methodology
for automated deduction in non-classical logics, the relevance of which
to computer science is now widely acknowledged. The methodology is based
on goal-directed provability. It is a generalization of the logic
programming style of deduction, and it is particularly favourable for
proof search. The methodology is applied for the first time in a uniform
way to a wide range of non-classical systems, covering intuitionistic,
intermediate, modal and substructural logics. The book can also be used
as an introduction to these logical systems form a procedural
perspective.
Readership: Computer scientists, mathematicians and philosophers, and
anyone interested in the automation of reasoning based on non-classical
logics. The book is suitable for self study, its only prerequisite being
some elementary knowledge of logic and proof theory