id: 04083032
dt: j
an: 04083032
au: Munch, Klaus Heje
ti: A new reduction rule for the connection graph proof procedure.
so: J. Autom. Reasoning 4, No.4, 425-444 (1988).
py: 1988
pu: Springer, Dordrecht
la: EN
cc: 
ut: automated theorem proving; connection graphs; resolution; order-sorted
    logic
ci: 
li: doi:10.1007/BF00297248
ab: 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.
rv: N.Curteanu