Declarative Rule

• Name: Binary Resolution
• Description in English: "Binary resolution always focuses on two clauses and one literal in each. To admit a conclusion, the literals must be opposite in sign and alike in predicate, and there must exist a unifier (substitution of terms for variables) to otherwise make them identical. If a conclusion results, it is obtained by applying the unifier to the two clauses excluding the two literals in focus, and taking the union of the transformed literals."
• Rule Specification: '(or ' A ')'; '(or' B ')' |- '(or ' A + B - A.i - B.j ')';; (Lit A B) ; (= {A.i} {'(not ' B.j ')'})
• Specification Language: Proof Protocol for Deductive Reasoning (PPDR)
• Example in English: Suppose we have as axioms the following clauses:

  (or (mortal ?x) (not (human ?x)))
  (human Socrates)
  

  By substituting "Socrates" for "?x", the second literal of the first clause is made identical with the negation of the sole literal of the second clause. The opposed literals are resolved, leaving as a conclusion the resolvent

  (mortal Socrates)
  

• 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.