A Classification of Non-liftable Orders for Resolution

In this paper we study the completeness of resolution when it is restricted by a non-liftable order and by weak subsumption. A non-liftable order is an order that does not satisfy A B A B. Clause c1 weakly subsumes c2 if c1 c2, and is a renaming substitution. We show that it is natural to distinguish 2 types of non-liftable orders and 3 types of weak subsumption, which correspond naturally to the 2 types of nonliftable orders. Unfortunately all natural combinations are not complete. The problem of the completeness of resolution with non-liftable orders was left open in ([Nivelle96]). We will also give some good news: Every non-liftable order is complete for clauses of length 2, and can be combined with weak subsumption.

• Type: Conference
• Year: 1997
• Where: CADE
• Authors: Hans de Nivelle
• Keywords: CADE 1997, Logical Reasoning, Non-liftable Order, Nonliftable Orders, Weak Subsumption