Re: [test] disjunctive entailment without equality

Michael Kifer wrote:
> 
> On Sat, 29 Nov 2008 22:39:24 -0500
> Chris Welty <cawelty@gmail.com> 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).

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

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

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

-Chris


-- 
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 Monday, 1 December 2008 03:24:39 UTC