20060105111006
Value Link Creation
20051128143825
<p>
This proof step is a forward-chaining resolution reasoning step implemented with Value Collections, listeners, and Value Links in JTP's frame system.
<p>
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.
<p>
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 <code>?x</code> that satisfy a triple of the form <code>(property subject ?x)</code>, or of the form <code>(property ?x value)</code>. 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.
<p>
A ValueLink represents the inclusion of one Value Collection, the source, into another Value Collection, the target. A Value Link from source collection <code>(p1 s1 ?x)</code> to target collection <code>(p2 s2 ?y)</code> asserts that all values of <code>?x</code> in the source are also values for <code>?y</code> in the target. A Value Link can thus be viewed as implementing the implication:
<pre>
(<= (p2 s2 ?x)
(p1 s1 ?x))
</pre>
<p>
Example 1:
<p>
Consider the Value Collections <code>(type Rover ?x)</code> and <code>(subClassOf Dog ?y)</code>, and suppose we know that <code>(type Rover Dog)</code>. Then a Value Link from the source Value Collection <code>(subClassOf Dog ?y)</code> to the target Value Collection <code>(type Rover ?x)</code> asserts that all superclasses of Dog are also types for Rover. This ValueLink can be viewed as implementing the implication:
<pre>
(<= (type Rover ?x)
(subClassOf Dog ?x))
</pre>
<p>
Example 2:
<p>
Given the clause corresponding to a Value Collection Listener Creation step:
<pre>
(<= (subClassOf CRAB ?x)
(and (subClassOf CRAB ?y) (subClassOf ?y ?x)))
</pre>
wherein a listener has been set up awaiting new values for the Value Collection <code>(subClassOf CRAB ?y)</code>, and given the triple <code>(subClassOf CRAB SHELLFISH)</code>, a Value Link Creation proof step derives using variable binding <code>?y=SHELLFISH</code> a new clause:
<pre>
(<= (subClassOf CRAB ?x)
(subClassOf SHELLFISH ?x))
</pre>
by setting up a Value Link from the Value Collection <code>(subClassOf SHELLFISH ?x)</code> to the Value Collection <code>(subClassOf CRAB ?x)</code>.
<p>