Extending the Regular Restriction of Resolution to Non-Linear Subdeductions

Abstract

A binary resolution proof, represented as a binary tree, is irregular if some atom is resolved away and reappears on the same branch. We develop an algorithm, linear in the size of the tree, which detects whether reordering the resolutions in a given proof will generate an irregular proof. If so, the given proof is not minimal. A deduction system that keeps only minimal proofs retains completeness. We report on an initial implementation. Introduction 1 The regular restriction of resolution (Tseitin 1969) states that a resolution step resolving on a given literal should not be used to deduce a clause containing that literal. That is, both steps should not be in the same branch (or linear subdeduction) of the proof tree. We extend this restriction so that it applies steps to that are not on one branch, but can be made linear by rotating edges of the tree, as long as those rotations do not weaken the proof. If a proof cannot be made irregular by rotations, we call it minimal. The first ...