The smallest and most efficient resolution based proof of a theorem is represented by a minimal clause tree, proposed by Horton and Spencer. A clause tree T is minimal if and only if it contains no legal tautology paths and no legal unchosen merge paths. A characterization of minimal clause trees is given in terms of derivations. A subsumption relationship between resolution based procedures is defined and all such procedures are shown to be subsumed by clause tree procedures. Three classes of procedures are proposed which produce only minimal clause trees. The first performs surgery on any clause tree that is produced to reduce it to a minimal clause tree. The second avoids any resolution that produces a clause tree on which surgery can be performed, but leaf to internal node paths are allowed to be chosen. The third, and most restrictive, avoids any resolution that produces a non-minimal clause tree. Keywords: theorem proving, reasoning (resolution), search.
Zircon - This is a contributing Drupal Theme Design by WeebPal.
