Re: [test] disjunctive entailment without equality

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

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
> 

-- 
Jos de Bruijn            debruijn@inf.unibz.it
+390471016224         http://www.debruijn.net/
----------------------------------------------
No one who cannot rejoice in the discovery of
his own mistakes deserves to be called a
scholar.
  - Donald Foster