Inference Engine

• Full name: JTP - KSL Java Theorem Prover
• URL: http://www.ksl.stanford.edu/software/JTP/
• Source(s):
  • Name: KSL JTP Inference engine development team
  • Member(s):
    • Name: Gleb Frank
    • URL: http://xenon.stanford.edu/~gkfrank/
    • Name: Jessica Jenkins
    • URL: http://www-ksl.stanford.edu/people/jessicaj/
    • Name: Richard Fikes
    • URL: http://www.ksl.stanford.edu/people/bio/fikes.html
    • Affiliation(s):
      • Name: Knowledge Systems Laboratory, Stanford University
      • URL: http://www.KSL.Stanford.EDU
• 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: Demodulation
  • Description in English: "The demodulation rule takes an equality statement x = y and any sentence with a nested term that unifies with x and derives the same sentence with y substituted for the nexted term."
  • Example in English: "If b.a=c is inferred in the presence of (x^(-1))^(-1)=x, substitution immediately yields obviously related inferences such as (b^(-1))^(-1).a=c."
  • Source(s):
    • Name: The Concept of Demodulation in Theorem Proving, JACM 14(4), pp. 698-709
    • Author(s):
      • Name: Daniel F. Carson

      ---

      • Name: George A. Robinson

      ---

      • Name: Leon Shalla

      ---

      • Name: Larry Wos
      • URL: http://www-unix.mcs.anl.gov/~wos/

  ---

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

  ---

  • Name: Frame Meta Information
  • Description in English:

    Given a triple (property subject value), a Frame Meta Information proof step derives information for use by JTP's frame system, including that subject is a frame, property is a slot, and the frame subject has property as one of its slots.

  • Example in English:

    Given the literal (subClassOf CRAB SHELLFISH) derive the literal (:has-slot CRAB subClassOf)

  • Source(s):
    • Name: Knowledge Systems Laboratory, Stanford University
    • URL: http://www.KSL.Stanford.EDU

  ---

  • Name: Function Rule
  • Description in English: This proof step is used when the goal has been proved through some form of procedural attachment.
  • Example in English: The goal (+ 3 2) would be solved by an arithmetic module, and the proof returned would be a FunctionProofStep.

  ---

  • Name: Generalized Modus Ponens
  • Description in English: For atomic sentences si, si" and r, where there is a substitution T such that subst(T,si")=subst(T,si) for all i: s1",s2",...,sn",(s1^s2^...^sn => r) implies subst(T,r)
  • Rule Specification: A; '(implies (and ' A ')' q ')' |- q;; (Sent A q)
  • Specification Language: Proof Protocol for Deductive Reasoning (PPDR)
  • Source(s):
    • Name: Artificial Intelligence: A Modern Approach
    • URL: http://www.cs.berkeley.edu/~russell/aima.html
    • Author(s):
      • Name: Peter Norvig
      • URL: http://www.norvig.com/

      ---

      • Name: Stuart Russell
      • URL: http://www.cs.berkeley.edu/~russell/

  ---

  • Name: Membership Rule
  • Description in English:

    This proof step indicates that, in JTP's frame system, a specific Value Collection contains the value in question.

    A Value Collection can be thought of as the set of values of ?x that satisfy a triple of the form (property subject ?x), or of the form (property ?x value).

    Given a triple (property subject value) this proof step could represent the inference that ?x=value belongs to the Value Collection (property subject ?x), or the inference that ?x=subject belongs to the Value Collection (property ?x value).

  • Example in English:

    Given the triple (subClassOf SHELLFISH SEAFOOD) derive that ?x=SEAFOOD is a member of the Value Collection (subClassOf SHELLFISH ?x).

  ---

  • Name: Membership via Value Link
  • Description in English:

    This proof step is a special case of the Membership Rule, wherein membership in a Value Collection is inferred using a Value Link. For more information on Value Links, see the Value Link Creation rule description.

  • Example in English:

    Given that ?x=SEAFOOD is a member of the Value Collection (subClassOf SHELLFISH ?x), and given a Value Link represented by

       (<= (subClassOf CRAB ?y) 
           (subClassOf SHELLFISH ?y))
    

    derive that ?z=SEAFOOD is also a member of the Value Collection represented by (subClassOf CRAB ?z).

  • Source(s):
    • Name: Knowledge Systems Laboratory, Stanford University
    • URL: http://www.KSL.Stanford.EDU

  ---

  • Name: Reformulation
  • Source(s):
    • Name: KSL JTP Inference engine development team
    • Member(s):
      • Name: Gleb Frank
      • URL: http://xenon.stanford.edu/~gkfrank/
      • Name: Jessica Jenkins
      • URL: http://www-ksl.stanford.edu/people/jessicaj/
      • Name: Richard Fikes
      • URL: http://www.ksl.stanford.edu/people/bio/fikes.html
      • Affiliation(s):
        • Name: Knowledge Systems Laboratory, Stanford University
        • URL: http://www.KSL.Stanford.EDU

  ---

  • Name: Subsumption Rule
  • Source(s):
    • Name: Inference Web development team
    • URL: http://www.ksl.stanford.edu/software/IW/

  ---

  • Name: Time Point for Temporal Reasoning
  • Description in English: This temporal reasoning step represents a combination of one or more of the following facts about time points. We use the a shorthand notation where < means "before", <= means "before-or-equal-point", and = means "equal-point": If a < b, and b < c, then a < c. [Transitivity of "before"] If a <= b, and b <= c, then a <= c. [Transitivity of "before-or-equal-point"] If a < b, and b <= c, then a < c. [Composition of "before" and "before-or-equal-point"] If a < b, and b = c, then a < c. [Composition of "before" and "equal-point"] If a = b, and b <= c, then a <= c. [Composition of "equal-point" and "before-or-equal-point".]
  • Source(s):
    • Name: KSL JTP Inference engine development team
    • Member(s):
      • Name: Gleb Frank
      • URL: http://xenon.stanford.edu/~gkfrank/
      • Name: Jessica Jenkins
      • URL: http://www-ksl.stanford.edu/people/jessicaj/
      • Name: Richard Fikes
      • URL: http://www.ksl.stanford.edu/people/bio/fikes.html
      • Affiliation(s):
        • Name: Knowledge Systems Laboratory, Stanford University
        • URL: http://www.KSL.Stanford.EDU

  ---

  • Name: Time Point Mapping
  • Description in English: Maps the notational description of a time point into an instance of a TimePoint data structure. The data structure is what is actually reasoned with.
  • Example in English: The List of symbols (starting-point Jess-Life) is mapped into an instance of a TimePoint.
  • Source(s):
    • Name: KSL JTP Inference engine development team
    • Member(s):
      • Name: Gleb Frank
      • URL: http://xenon.stanford.edu/~gkfrank/
      • Name: Jessica Jenkins
      • URL: http://www-ksl.stanford.edu/people/jessicaj/
      • Name: Richard Fikes
      • URL: http://www.ksl.stanford.edu/people/bio/fikes.html
      • Affiliation(s):
        • Name: Knowledge Systems Laboratory, Stanford University
        • URL: http://www.KSL.Stanford.EDU

  ---

  • Name: TranslationReasoningStep
  • Source(s):
    • Name: Knowledge Systems Laboratory, Stanford University
    • URL: http://www.KSL.Stanford.EDU

  ---

  • Name: Value Collection Listener Creation
  • Description in English:

    This proof step is a forward-chaining resolution reasoning step implemented with Value Collections and listeners in JTP's frame system.

    Given a Horn clause with one positive literal and N>=3 negative literals, and given another positive triple P that unifies with one of the negative literals in the Horn clause, derive a shorter Horn clause with N-1 negative literals as would occur in a resolution step.

    Note: some implementation detail is useful here to motivate the name of the rule. Negative literals in the clause that are triples with one unbound variable correspond to Value Collections in JTP's frame system. Recall that a Value Collection can be viewed as the set of values of ?x that satisfy a triple of the form (property subject ?x), or of the form (property ?x value). A listener is created for one of those Value Collections to await new values, so that when one arrives (represented by triple P in the description above), this triggers the creation of new Value Collection listeners that correspond to triples with one unbound variable in the resultant shorter clause, thereby enabling future resolution involving the shorter clause.

    Note: regarding the restriction to N>=3 above, note that when N=2 the resulting clause would have only one antecedent and can be viewed as a Value Link between the Value Collections corresponding to its positive and negative triples, so the Value Link Creation proof step would instead be invoked to create such a Value Link. For more information refer to the Value Link Creation rule description.

  • Example in English:

    Example 1:

    Given the horn clause corresponding to a Value Collection Listener Creation step:

      (<= (holds ?prop ?w ?x) 
          (and (type ?prop TransitiveProperty) 
               (holds ?prop ?w ?y) 
               (holds ?prop ?y ?x)))
    

    wherein a listener has been set up awaiting new values for the Value Collection (type ?prop TransitiveProperty), and given the triple (type subClassOf TransitiveProperty), derive a new horn clause

      (<= (subClassOf ?w ?x) 
          (and (subClassOf ?w ?y) 
               (subClassOf ?y ?x)))
    

    with variable binding ?prop=subClassOf, and create a listener for Value Collection (:has-slot ?z subClassOf) to enable future resolution; this is what happens when the resultant clause has no literals corresponding to Value Collections.

    Example 2:

    Given the resultant clause above, and the triple (:has-slot CRAB subClassOf), derive a new clause:

      (<= (subClassOf CRAB ?x) 
          (and (subClassOf CRAB ?y) (subClassOf ?y ?x)))
    

    with variable binding ?w=CRAB, and create a listener for Value Collection (subClassOf CRAB ?y) to enable future resolution.

  • Source(s):
    • Name: Knowledge Systems Laboratory, Stanford University
    • URL: http://www.KSL.Stanford.EDU

  ---

  • Name: Value Link Creation
  • Description in English:

    This proof step is a forward-chaining resolution reasoning step implemented with Value Collections, listeners, and Value Links in JTP's frame system.

    Given a Horn clause with one positive literal and N=2 negative literals, and given another positive triple P that unifies with one of the negative literals in the Horn clause, derive a shorter Horn clause with one antecedent as would occur in a resolution step. (For the case of N>=3 negative literals refer to the Value Collection Listener Creation rule description.

    Note: some implementation detail is useful here to motivate the name of the rule. Negative literals in the clause that are triples with one unbound variable correspond to Value Collections in JTP's frame system. Recall that a Value Collection can be viewed as the set of values of ?x that satisfy a triple of the form (property subject ?x), or of the form (property ?x value). A listener is created for one of those Value Collections to await new values, so that when one arrives (represented by triple P in the description above), this triggers the creation of a Value Link.

    A ValueLink represents the inclusion of one Value Collection, the source, into another Value Collection, the target. A Value Link from source collection (p1 s1 ?x) to target collection (p2 s2 ?y) asserts that all values of ?x in the source are also values for ?y in the target. A Value Link can thus be viewed as implementing the implication:

       (<= (p2 s2 ?x)
           (p1 s1 ?x))
    

  • Example in English:

    Example 1:

    Consider the Value Collections (type Rover ?x) and (subClassOf Dog ?y), and suppose we know that (type Rover Dog). Then a Value Link from the source Value Collection (subClassOf Dog ?y) to the target Value Collection (type Rover ?x) asserts that all superclasses of Dog are also types for Rover. This ValueLink can be viewed as implementing the implication:

       (<= (type Rover ?x)
           (subClassOf Dog ?x))
    

    Example 2:

    Given the clause corresponding to a Value Collection Listener Creation step:

      (<= (subClassOf CRAB ?x) 
          (and (subClassOf CRAB ?y) (subClassOf ?y ?x)))
    

    wherein a listener has been set up awaiting new values for the Value Collection (subClassOf CRAB ?y), and given the triple (subClassOf CRAB SHELLFISH), a Value Link Creation proof step derives using variable binding ?y=SHELLFISH a new clause:

      (<= (subClassOf CRAB ?x) 
          (subClassOf SHELLFISH ?x))
    

    by setting up a Value Link from the Value Collection (subClassOf SHELLFISH ?x) to the Value Collection (subClassOf CRAB ?x).

  • Source(s):
    • Name: Knowledge Systems Laboratory, Stanford University
    • URL: http://www.KSL.Stanford.EDU

(Registration details...)

Copyright 2009 Inference Web group.
All Rights Reserved.