Goal-directed proof theory

Abstract

This report is the draft of a book about goal directed proof theoretical formulations of non-classical logics. It evolved from a response to the existence of two camps in the applied logic (computer science/artificial intelligence) community. There are those members who believe that the new non-classical logics are the most important ones for applications and that classical logic itself is now no longer the main workhorse of applied logic, and there are those who maintain that classical logic is the only logic worth considering and that within classical logic the Horn clause fragment is the most important one. The book presents a uniform Prolog-like formulation of the landscape of classical and non-classical logics, done in such away that the distinctions and movements from one logic to another seem simple and natural; and within it classical logic becomes just one among many. This should please the non-classical logic camp. It will also please the classical logic camp since the goal directed formulation makes it all look like an algorithmic extension of Logic Programming. The approach also seems to provide very good compuational complexity bounds across its landscape.