Re: [test] disjunctive entailment without equality

Jos de Bruijn wrote:
>>>>> Thanks, Jos.
>>>>>
>>>>> This gets me wondering.  Clearly the converse of Jos' test case also holds,
>>>>> e.g. that:
>>>>>
>>>>> Document(
>>>>>   Prefix(ex http://example.com/example#)
>>>>>   Prefix(pred http://www.w3.org/2007/rif-builtin-predicate#)
>>>>>   Group(
>>>>>     ex:p(ex:a)
>>>>>     Forall ?x (q(?x) :- And (ex:p(?x) External(pred:isInteger(ex:a))))))
>>>>>
>>>>> |= (or q(ex:a) External(pred:isNotInteger(ex:a)))
>>>> Why is this outside the language?
>>> By outside the language I mean that you cannot say (or q(ex:a) 
>>> External(pred:isNotInteger(ex:a))) in BLD, it is syntactically invalid.  The 
>>> whole point of Jos' test cases was being able to entail something that can't be 
>>> expressed in the language (in this case disjunction in the conclusion).
>> This is not outside of the language. It is a condition formula and a completely
>> kosher goal. Such goals are normal not only in 1-order logic, but also in
>> logic programming.
> 
> Indeed.  Even if one would not allow disjunction in condition formulas,
> one could simply write two rules with the same head, with the disjuncts
> as the individual rule bodies.
> See also my response [1] to similar e-mail by Dave.

Err....now I'm completely confused.  The

(or q(ex:a) external(pred:isNotInteger(ex:a))))

is not a condition, its a conclusion.  I do not know how to rewrite a rule so 
that disjunction in the conclusion is possible, except for the test cases here. 
   What are you talking about?

I searched for "kosher goal" (and also "goal") in the BLD spec and it speaks 
nothing of such things.  What are you talking about?

I interpreted this test case as showing that you could "sneak" disjunction into 
the conclusion of a rule using negative guards.  Now you are talking about 
conditions, which already allow disjunction.  So who cares about this test case? 
  Why is it important?

-Chris

> 
> Best, Jos
> 
> [1] http://lists.w3.org/Archives/Public/public-rif-wg/2008Nov/0191.html
> 
>>>> The problem here is that without
>>>> any kind of closed-world assumption or a unique name assumption the above leads
>>>> to a disjunction, which cannot be taken apart, unlike in logic programming.
>>> The problem I'm talking about is that the language has entailments that fall 
>>> outside its expressivity.
>> It is outside of the expressivity only if we add negation as we did (through
>> the  back door).
>>
>>>> So, with negative guards we are introducing negation through the back door, but
>>>> do not inject the standard antidotes to keep disjunction away.
>>> I'm suggesting negative guards don't create a new problem here.  We already know 
>>> implication is negation + disjunction, so even without negative guards you can 
>>> write rules whose entailments are outside the language, including disjunction in 
>>> the conclusion.
>> No you cannot! If you have pure Horn clauses then disjunctive goals are NOT
>> outside of the expressivity of the language.
>>
>>
>>> So, why not just take the usual route in such cases and say that anything 
>>> outside the expressiveness of the language is not entailed (or not
>>> necessarily entailed, I guess).
>> See above.
>>
>> michael
>>
> 

-- 
Dr. Christopher A. Welty                    IBM Watson Research Center
+1.914.784.7055                             19 Skyline Dr.
cawelty@gmail.com                           Hawthorne, NY 10532
http://www.research.ibm.com/people/w/welty

Received on Tuesday, 2 December 2008 04:21:51 UTC