Inference Engine

• Full name: Otter
• URL: http://www-unix.mcs.anl.gov/AR/otter/
• Version: 3.2
• Source(s):
  • 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/
• Inference Rule(s):
  • 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/

  ---

  • Name: Factoring
  • Description in English: "Factoring always focuses on one clause at a time and on two literals in that clause. An application of factoring yields a conclusion if and only if the two literals in focus are alike in sign and if there exists a unifier (substitution of terms for variables) whose use makes the two literals identical. The conclusion is obtained by applying the unifier to the clause and merging the identical literals. In Otter, factoring is implemented in two ways: as an inference rule as described in the preceding paragraph, and as a simplification rule, which applies when the conclusion is logically equivalent to the original clause."

  ---

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

  ---

  • Name: Negative Paramodulation
  • Description in English: "The inference rule negative paramodulation reasons from negated equalities rather than equalities. The rule is sound if the functions involved satisfy certain cancellation-like properties. For example, from A<>B and AC=D, we can derive BC<>D by negative paramodulation provided that right cancellation holds for product."
  • Source(s):
    • Name: Negative Paramodulation, Proceedings of CADE-8, Lecture Notes in Computer Science 230, pp. 229-239
    • Author(s):
      • Name: Larry Wos
      • URL: http://www-unix.mcs.anl.gov/~wos/

      ---

      • Name: William McCune
      • URL: http://www-unix.mcs.anl.gov/~mccune/
    • Publisher:
      • Name: Springer-Verlag Heidelberg
      • URL: http://www.springer.de/

  ---

  • Name: Paramodulation
  • Description in English: "Paramodulation always focuses on two clauses, requiring that one of the clauses contain at least one literal asserting the equality of two expressions. For an application of paramodulation to succeed, there must exist a unifier (substitution of terms for variables) that, when used, makes identical one argument of a chosen positive equality literal in one clause and one chosen term in the other clause. If r is the chosen argument, s the other argument of the positive equality literal, t the chosen term, and U the unifier, the conclusion is obtained by applying U to both clauses, then replacing U(t) with U(s), and finally, except for the positive equality literal, taking the union of the transformed remaining literals. (With the exception of reflexivity, x = x, the nature of paramodulation permits the omission of the usual axioms for equality.) Because of the potential fecundity of using paramodulation (from being term-oriented rather than literal-oriented), various restriction strategies are recommended. They include restricting the choice of argument (in the positive equality literal) to just the lefthand argument, to just the righthand argument, and to arguments that are not merely a variable. Also recommended is restricting the chosen term to one that is not merely a variable. "
  • Example in English: Suppose we have as axioms the following clauses:

    (or (not (author Moby-Dick ?x)) (= Melville ?x))
    (American Melville)
    

    Paramodulation allows us to conclude:

    (or (not (author Moby-Dick ?x)) (American ?x))
    

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

  ---

  • Name: Unit Deletion
  • Description in English: "Unit Deletion acts rather like demodulation, automatically removing a literal in a clause when a unit clause exists that unifies with the literal, that is opposite in sign, and such that the unification does not affect the variables in the literal in question."
  • 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/

  ---

  • Name: UR-Resolution
  • Description in English: "UR-Resolution focuses on two or more clauses, requiring that one of the clauses (the nucleus) contain at least two literals and the remaining (the satellites) contain exactly one literal. Briefly, a conclusion is yielded if a unifier (substitution of terms for variables can be found that, when applied, makes identical (except for being opposite in sign) pairs of literals, one literal from the nucleus with one 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. "
  • 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.