Value Collection Listener Creation 20060105102912 20051128143726 <p> This proof step is a forward-chaining resolution reasoning step implemented with Value Collections and listeners in JTP's frame system. <p> 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. <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 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. <p> 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. <p> Example 1: <p> Given the horn clause corresponding to a Value Collection Listener Creation step: <pre> (<= (holds ?prop ?w ?x) (and (type ?prop TransitiveProperty) (holds ?prop ?w ?y) (holds ?prop ?y ?x))) </pre> wherein a listener has been set up awaiting new values for the Value Collection <code>(type ?prop TransitiveProperty)</code>, and given the triple <code>(type subClassOf TransitiveProperty)</code>, derive a new horn clause <pre> (<= (subClassOf ?w ?x) (and (subClassOf ?w ?y) (subClassOf ?y ?x))) </pre> with variable binding <code>?prop=subClassOf</code>, and create a listener for Value Collection <code>(:has-slot ?z subClassOf)</code> to enable future resolution; this is what happens when the resultant clause has no literals corresponding to Value Collections. <p> Example 2: <p> Given the resultant clause above, and the triple <code>(:has-slot CRAB subClassOf)</code>, derive a new clause: <pre> (<= (subClassOf CRAB ?x) (and (subClassOf CRAB ?y) (subClassOf ?y ?x))) </pre> with variable binding <code>?w=CRAB</code>, and create a listener for Value Collection <code>(subClassOf CRAB ?y)</code> to enable future resolution. <p>