Elimination of self-resolving clauses (Q1383994)

The paper deals with an investigation of a problem in programming languages and also in logical axiomatization concerning recursiveness. The author solves the question of how to eliminate clause sets that may contain self-resolving clauses like symmetry or transitivity, or even clauses like condensed detachment. The method proposed consists in transforming the other clauses in such a way that they encode sufficiently much of the information contained in the eliminated clause set. It is shown how the transformation can be found for a given clause set, and how to guarantee its soundness and completeness. By investigating the elimination of self-resolving clauses some interesting results can be achieved, e.g., modifying and improving the search behavior of automated theorem provers, eliminating loops in logic programs, parallelizing simple closure computation algorithms, and automating complexity analysis.