A new reduction rule for the connection graph proof procedure (Q1114445)

The connection graph proof procedure (CGPP) is extended from one-valued variables to set-valued variables. Finding the set of values for clause variables, and checking which links can be removed, is performed during the extended unification procedure. In this context a new reduction rule is introduced (called v-rule), leading to refined link removals in CGPP. The author argues that the introduced v-rule preserves the refutation confluence property of the resulted CGPP. A proof system containing the v-rule has been implemented by the author in PROLOG, and successfully compared with other priviously existing proof systems on the Schubert's steamroller problem. The relation of this approach to order-sorted logic is pointed out. We suggest the (not only) formal connection with the (linguistic) feature structure unification algorithms (and grammars). Despite the extra-cost involved by the v-rule administration of clause variable values, the system proves to be prominent considering execution time, while generating the fewest number of derived clauses.