Clause trees provide a basis for reasoning procedures .that use binary resolution. In this paper binary resolution trees are used as the data structure for implementing these procedures. Several properties of these procedures are explored: size, stages, minimality, disequalities, activity and rank. Procedures for uniquely building all minimal clause trees are introduced. Ordinary subsumption within these procedures does not preserve completeness, but contracting subsumption, a new restricted form of subsumption that relates to clause trees, can be integrated. The minimal restriction and unique construction address the problem of redundancy with binary resolution.
Zircon - This is a contributing Drupal Theme Design by WeebPal.
