Reasoning in the Presence of Inconsistency

In this paper, we propose a logic which is nontrivial in the presence of inconsistency. The logic is based on the resolution principle and coincides with the classical logic when premises are consistent. Some results of interesting to Automated Theorem Proving are a sound and sometimes complete three-valued semantics for the resolution rule and a refutation process which is much in the spirit of the problem reduction format.