Clause Trees and Factor Paths
Loading...
Files
Date
1994
Authors
Journal Title
Journal ISSN
Volume Title
Publisher
Abstract
The concept of a clause is generalized to that of a clause tree which shows how the clause can be proved from a set of input clauses. Procedures are provided to find factorizations and tautologies at build time using the internal structure of the tree. Model Elimination and SLI are specializations of this technique. Other resolution-based proof procedures, including bottom-up ones, could include these concepts to make better procedures. One example top-down procedure, ALPOC, has been implemented as part of Stickel's PTTP system.
Content areas: automated reasoning, theorem proving, disjunctive logic programming