Bottom up procedures to construct each minimal clause tree once

Description

Bottom up procedures are introduced for constructing only minimal clause trees. Two general methods are proposed. The first performs surgery on each non-minimal clause tree; the second ignores non-minimal clause trees and retains only minimal ones. By ranking open leaves and activating/deactivating leaves according to the ranking, the second method constructs each minimal clause tree exactly once. Methods for incorporating subsumption are described and a prototype system for propositional logic is compared against OTTER.