Re: [test] disjunctive entailment without equality

Sandro Hawke wrote:
>>>   Document(
>>>      Prefix(ex http://example.com/example#)
>>>      Prefix(pred http://www.w3.org/2007/rif-builtin-predicate#)
>>>      Group(
>>>         Forall ?x (ex:q(?x) :-
>>>                     Or (
>>>                       External(pred:isNotInteger(?x))
>>>                       External(pred:isInteger(?x))
>>>                        )
>>>                    )
>>>       )
>>>
>>> entails:
>>>     ex:q(ex:a)
>> Yes, this is also a good one.
>> I think it nicely complements the test case 
>> Disjunctive_Information_from_Negative_Guards_3.
>>
>> Your test case shows how you need to do reasoning by case using the 
>> rule bodies, whereas Disjunctive_Information_from_Negative_Guards_3 
>> show how you need to reason by case with the rule heads.
> ...
>>> It's logically entailed, but neither a production rule system nor a
>>> prolog-style system is going to figure that out.   (The prolog one
>>> might, by mistake, if it took ex:a as a prolog atom.)
> 
> I think the problem/question here is about whether DTB/PRD/Core
> reasoners are expected to know about the internals of externals.  I
> suggest they are not.  I expect a BLD consumer to have a BLD reasoner
> which treats all Externals as opaque, and then a library implementing
> the required Externals.  The library should be usable by other dialects,
> including PRD, Core, and someday full FOL and LP dialects.  I think we
> have example systems out there (production rule systems, logic
> programming systems, and FOL theorem provers) which have opaque external
> elements.
> 
> I believe the API for predicates should allow "True", "False", and
> "Unknown" responses.  For both isInteger and isNotInteger on a constant
> symbol it would return Unknown (since it doesn't know if that constant
> is equal to some integer).  (If it turns out to be equal to something
> like an integer or a non-integer (eg string), then then the rule engine
> can do the substitution and try again.)

This sounds like a completely reasonable way to implement the
predicates.  And "unknown" could simply be interpreted as "false" if we
would not have negation, and the system would work fine.
However, we do have this negation.

We could introduce a general datatype, i.e., rdfs:Literal, which is a
super type of all other datatypes, and either recommend or require every
term (that is not a typed literal) used in a negative guard to also be
used in pred:isLiteral.

So, the second rule would become

ex:q(?x) :- And(External(pred:isNotInteger(?x))
External(pred:isLiteral(?x)))

And it is not known whether ex:a is a data value (and there is no way to
assert that this is the case), so implementing the externals in the way
you suggested works under this restriction, as far as I can tell at the
moment.
That is, ex:q(ex:a) is not entailed.


Best, Jos

> 
> That is:
> 
>      ex:q(?x) :- External(pred:isInteger(?x))
>   does not entail
>      ex:q(ex:a)
> 
> and 
> 
>      ex:q(?x) :- External(pred:isNotInteger(?x))
>   does not entail
>      ex:q(ex:a)
> 
> Hmmm....   Thoughts?
> 
>     -- Sandro
> 
> 
> 

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