Inference Engine

• Full name: SNARK - SRI New Automated Reasoning Kit
• URL: http://www.ai.sri.com/~stickel/snark.html
• Version: 1.0
• Source(s):
  • Name: SNARK development team
  • Member(s):
    • Name: Mark E. Stickel
    • URL: http://www.ai.sri.com/~stickel/
    • Name: Richard Waldinger
    • URL: http://www.ai.sri.com/~waldinge/
• Inference Rule(s):
  • Name: Assumption
  • Description in English: An assumption specified by the user for the purpose of performing a specific query.
  • Rule Specification: |- p;; (Sent p)
  • Specification Language: Proof Protocol for Deductive Reasoning (PPDR)

  ---

  • 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: 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: Negated Conclusion
  • Description in English: In systems that use proof by contradiction, the negation of the statement to be proved.

  ---

  • 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: Direct assertion
  • Description in English: Direct assertion of a sentence, possibly by loading a sentence (or a set of sentences) from an existing knowledge base.
  • Rule Specification: |- p;; (Sent p)
  • Specification Language: Proof Protocol for Deductive Reasoning (PPDR)
  • Example in English: One might load the statement from the wines ontology that RedWine is a subclass of Wine.

(Registration details...)

Copyright 2009 Inference Web group.
All Rights Reserved.