Declarative Rule

• Name: Hyperresolution
• Description in English: "Hyperresolution focuses on two or more clauses, requiring that one of the clauses (the nucleus) contain at least one negative literal and the remaining (the satellites) contain no negative literals. Briefly, a conclusion is yielded if a unifier (substitution of terms for variables can be found that, when applied, makes identical (except for sign) pairs of literals, one negative literal from the nucleus with one positive from a satellite. The conclusion is yielded by, ignoring the paired literals, applying the unifier simultaneously to the nucleus and the satellites and taking the union of the resulting literals. Otter"s implementation of hyperresolution has two extra features. First, it can be restricted so that only ``largest"" literals in satellites can be resolved; this restriction can reduce redundancy for non-Horn clauses. Second, the negative literals in the nuclei can be evaluable instead of resolvable; This allows some amount of "programming" of Otter using built-in operations."
• Example in English: Suppose we have as axioms the following clauses:

     (or (love ?x ?y) (hate ?x ?y))
     (or (not (try-kill ?x ?y)) (not (love ?x ?y)))
     (try-kill Marcus Caesar)
  

  By substituting "Marcus" for "?x" and "Caesar" for "?y", we may treat the second clause as the nucleus and the first and third clauses as satellites. The opposed literals are resolved, leaving as a conclusion the resolvent

  (hate Marcus Caesar)
  

• Source(s):
  • Name: A Summary of Inference Rules Used by Argonne Automated Deduction Software
  • URL: http://www-unix.mcs.anl.gov/AR/inf_rules.html

  ---

  • Name: Otter development team
  • Member(s):
    • Name: Larry Wos
    • URL: http://www-unix.mcs.anl.gov/~wos/
    • Name: Olga Shumsky Matlin
    • URL: http://www-unix.mcs.anl.gov/~matlin/
    • Name: Ewing (Rusty) Lusk
    • URL: http://www-fp.mcs.anl.gov/~lusk/
    • Name: Ross Overbeek
    • Name: William McCune
    • URL: http://www-unix.mcs.anl.gov/~mccune/

(Registration details...)

Copyright 2009 Inference Web group.
All Rights Reserved.