Resolution Games and Non-Liftable Resolution Orderings

We prove the completeness of the combination of ordered resolution and factoring for a large class of non-liftable orderings, without the need for any additional rules like saturation. This is possible because of a new proof method wich avoids making use of the standard ordered lifting theorem. This proof method is based on resolution games.

• Type: Conference
• Year: 1994
• Where: CSL
• Authors: Hans de Nivelle
• Keywords: Automated Reasoning, Certain Resolution Refinements, CSL 1994, Proof Method, Resolution Refinements