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
Zircon - This is a contributing Drupal Theme Design by WeebPal.
