Re: [test] disjunctive entailment without equality

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

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

Received on Friday, 12 December 2008 19:13:22 UTC