---
title: "Consequence-Finding Based on Ordered Linear Resolution"
authors:
  - "Katsumi Inoue"
doi: ""
url: "https://ijcai.org/proceedings/1991/24"
pdf: "https://ijcai.org/proceedings/1991/0024.pdf"
venue: "Proceedings of the Twelfth International Joint Conference on Artificial Intelligence"
year: 1991
pages: "158-163"
track: "Automated Reasoning"
keywords:
---

# Consequence-Finding Based on Ordered Linear Resolution

Katsumi Inoue

*Proceedings of the Twelfth International Joint Conference on Artificial Intelligence*, pages 158-163.

## Abstract

Since linear resolution with clause ordering is incomplete for consequence-finding, it has been used mainly for proof-finding. In this paper, we re-evaluate consequence-finding. Firstly, consequence-finding is generalized to the problem in which only interesting clauses having a certain property (called characteristic clauses) should be found . Then, we show how adding a skip rule to ordered linear r es olution makes it complete for consequence-finding in this general sense. Compared with set-of-support resolution, the proposed method generates fewer clauses to find such a subset of consequences. In the propositional case, this is an elegant tool for computing the prime implicants/implicates. The importance of the results lies in their applicability to a wide class of AI problems including procedures for nonmonotonic and abductive reasoning and truth maintenance systems.