Efficient Algorithms to Detect and Restore Minimality, an Extension of the Regular Restriction of Resolution

摘要

A given binary resolution proof, represented as a binary tree, is said to be minimal if the resolutions cannot be reordered to generate an irregular proof. Minimality extends Tseitin's regularity restriction and still retains completeness. A linear-time algorithm is introduced to decide whether a given proof is minimal. This algorithm can be used by a deduction system that avoids redundancy by retaining only minimal proofs and thus lessens its reliance on subsumption, a more general but more expensive technique. Any irregular binary resolution tree is made strictly smaller by an operation called Surgery, which runs in time linear in the size of the tree. After surgery the result proved by the new tree is nonstrictly more general than the original result and has fewer violations of the regular restriction. Furthermore, any nonminimal tree can be made irregular in linear time by an operation called Splay. Thus a combination of splaying and surgery efficiently reduces a nonminimal tree to a minimal one. Finally, a close correspondence between clause trees, recently introduced by the authors, and binary resolution trees is established. In that sense this work provides the first linear-time algorithms that detect minimality and perform surgery on clause trees.