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

This is a condition, not a conclusion.  One can equivalently rewrite
this test case by adding the following rules to the ruleset:

ex:r :- q(ex:a)
ex:r :- external(pred:isNotInteger(ex:a))

and setting the conclusion to:

ex:r

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

it doesn't matter whether conditions allow disjunction or not, because
disjunction in conditions is syntactic sugar

> who cares about this test case?  Why is it important?

it shows that you need to reason by cases, which is not usual in
rule-based systems.

Best, Jos

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

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