Elimination of Self-Resolving Clauses

It is shown how self-resolving clauses like symmetry or transitivity, or even clauses like condensed detachment, can faithfully be deleted from the clause set thus eliminating or at least reducing recursiveness and circularity in clause sets. Possible applications are reducing the search space for automated theorem provers, eliminating loops in Prolog programs, parallelizing simple closure computation algorithms and supporting automated complexity analysis. Contents

• Type: Journal
• Year: 1998
• Where: JAR
• Authors: Hans Jürgen Ohlbach
• Keywords: Clause Sets, Closure Computation Algorithms, JAR 1998, Self-resolving Clauses