Hyperresolution for resolution logics

There is a wide variety of reasoning tasks that require an application of a non-classical logic. In the past, much of the research in the area of Automated Reasoning (AR) has concentrated on the development of reasoning programs for classical logic. Since non-classical logics are usually more complex, there has been less research on automated reasoning for non-classical logics. Most of the recent research in automated reasoning has attempted to find better speedup techniques, since the reasoning tasks can be computationally complex. The most popular among the logical methodologies for an automated reasoning task is the resolution rule introduced by Robinson (12) in 1965. Hyperresolution is among the most efficient refinements of resolution in classical logic. Hyperresolution allows reasoning tasks to be solved faster by restricting the applications of the resolution rule and by efficiently controlling the size of the search space. This thesis generalizes hyperresolution to resolution proof systems for the so-called "resolution logics". Furthermore, the notion of a non-clausal hyperrefutation (PI-refutation) is introduced and studied. I show that hyperresolution is both sound and complete in the domain of resolution logics. As in its classical counterpart, the new variant of hyperresolution blocks many redundant formulas from being created and added to the search space. Theoretical results reported in this thesis are supported with a number of examples.