This work is motivated by the need for efficient question-answering methods for Horn clause logic and its non-classical extensions - formalisms which are of great importance for the purpose of knowledge representation. The methods presented in this thesis are particularly suited for the kind of ‘‘computable specifications’’ that occur in areas such as logic programming and deductive databases.

The subject of study is a resolution-based technique, called tabulated resolution, which provides a procedural counterpart to the so-called well-founded semantics. Our study is carried out in two steps.

First we consider only classical Horn theories. We introduce a framework called the search forest which, in contrast to earlier formalizations of tabulated resolution for Horn theories, strictly separates between search space and search. We prove the soundness and completeness of the search space and provide some basic strategies for traversing the space. An important feature of the search forest is that it clarifies the relationship between a particular tabulation technique, OLDT-resolution, and the transformational bottom-up method called ‘‘magic templates’’.

Secondly, we generalize the notion of a search forest to Horn theories extended with the non-monotonic connective known as negation as failure. The tabulation approach that we propose suggests a new procedural counterpart to the well-founded semantics which, in contrast to the already existing notion of SLS-resolution, deals with loops in an effective way. We prove some essential results for the framework, including its soundness and completeness.