Bottom-up procedures for minimal clause trees

Loading...
Thumbnail Image

Date

1996

Journal Title

Journal ISSN

Volume Title

Publisher

Abstract

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.

Description

Keywords

Citation

Collections