- From: Doerthe Arndt <doerthe.arndt@ugent.be>
- Date: Fri, 14 Dec 2018 17:28:10 +0100
- To: public-n3-dev@w3.org
- Message-ID: <594bb686-1d8c-ad9c-c792-233ac37b418c@ugent.be>
Hi William,
> Proofs are there to explain derivations done not derivations which are
> not done.
>
> As a very simple example suppose you have the triple:
>
> :my :nice :triple.
>
> Now, you have a rule which you expect to be applicable on it, but that
> one has a typo:
>
> {?x :nic ?y}=>{?x :nicer ?y}.
>
> So, you would expect that the reasoner would come to the conclusion:
>
> :my :nicer :triple.
>
> but this derivation will not happen because you wrote :nic instead of
> :nice.
>
> In this case, it would be difficult to find this particular problem in
> a bigger setting. If you now ask your reasoner to give you proofs for
> all instances of ?x :nicer ?y (ie you give Cwm, EYE or whatever you
> use a goal like {?x :nicer ?y}=>{?x :nicer ?y}) the result above will
> simply not be derived and therefore there will be no proof.
>
> The reasoner will not give you a proof of everything it tried and then
> failed (and we do not know whether it even tried to apply this rule,
> this depends on the reasoning algorithm, simple forward-chaining would
> ignore this rule here, backward-chaining would try to apply it) since
> proofs reflect valid steps from a calculus which you applied on your
> data set.
>
> My remark relates to the fact that, technically, it would be possible
> to record why a particular rule is not firing (as you mention near the
> end). For instance, a particular premise was not matched, or there
> were no shared variables between particular premises. It would be
> quite trivial to do this in e.g., a forward-chaining reasoner (using
> RETE). But I make a moot point because it seems to be a bit out of
> scope of what we mean to do (?)
>
Mmm, maybe I really didn't get your point. In your example you would
need to explicitly mark the rule you are wondering about then (since I
expect you to have many rules which do not fire here) and then you
should also know on which triple you want it to fire since there will be
many triples it doesn't fire on. But if you are already that far that
you know which rule should fire on which triple, I doubt that you still
need a proof, you need some kind of debugging mechanism instead which
can show you what exactly happens on a rule. I would not see that as a
proof. As proof I really only see the mathematical proof of my result.
So, if there is not result, I also do not have this kind of proof.
Kind regards,
Doerthe
> William
>
> *From:*Doerthe Arndt <doerthe.arndt@ugent.be>
> *Sent:* December-13-18 5:30 AM
> *To:* William Van Woensel <william.vanwoensel@gmail.com>;
> public-n3-dev@w3.org
> *Subject:* Re: First meeting of our group
>
>
>
> Proofs will also certainly help for debugging but they rather
> help in cases where unexpected derivations happen.
>
> +1!
>
> When I expect a result which I then do not get, there is also no
> proof to check what happened (no proof for something which is not
> true).
>
> Why not? .. (aside from technical considerations)
>
> Proofs are there to explain derivations done not derivations which are
> not done.
>
> As a very simple example suppose you have the triple:
>
> :my :nice :triple.
>
> Now, you have a rule which you expect to be applicable on it, but that
> one has a typo:
>
> {?x :nic ?y}=>{?x :nicer ?y}.
>
> So, you would expect that the reasoner would come to the conclusion:
>
> :my :nicer :triple.
>
> but this derivation will not happen because you wrote :nic instead of
> :nice.
>
> In this case, it would be difficult to find this particular problem in
> a bigger setting. If you now ask your reasoner to give you proofs for
> all instances of ?x :nicer ?y (ie you give Cwm, EYE or whatever you
> use a goal like {?x :nicer ?y}=>{?x :nicer ?y}) the result above will
> simply not be derived and therefore there will be no proof.
>
> The reasoner will not give you a proof of everything it tried and then
> failed (and we do not know whether it even tried to apply this rule,
> this depends on the reasoning algorithm, simple forward-chaining would
> ignore this rule here, backward-chaining would try to apply it) since
> proofs reflect valid steps from a calculus which you applied on your
> data set.
>
> Kind regards,
> Doerthe
>
>
>
> W
>
> *From:*Doerthe Arndt <doerthe.arndt@ugent.be>
> <mailto:doerthe.arndt@ugent.be>
> *Sent:* December-12-18 11:09 AM
> *To:* public-n3-dev@w3.org <mailto:public-n3-dev@w3.org>
> *Subject:* Re: First meeting of our group
>
> Dear Sandro, all,
>
>
>
>
>
> My own interest is in making it practical (even fun and easy)
> to base real applications on open-world data (that is, RDF or
> other KR data), so that we end up with a full data-sharing
> ecosystem. It has long seemed like rules were a promising
> approach: rather than than having to code around all the
> possible forms the input data could take, we simply write the
> appropriate rules and let the system match them to the input
> data whenever/however possible. I've built a variety of
> systems like this, and in my experience, the promise has not
> worked out terribly well. Rules are very, very hard to debug.
> Hopefully things will improve some day.
>
> I am used to Prolog and wonder whether the simple debugging
> predicates and modes of for example SWI-Prolog could help here.
>
> The problem with debugging in Prolog (and I guess in any other
> rule language as well) is that it depends on the reasoning
> algorithm. In Prolog this is resolution with the left-most
> selection rule. Since we know that, we can also easily (ok,
> debatable, but I think it is easy) see where reasoning got stuck
> in case of problems. But I do not think that we should completely
> fix the reasoning mechanism we expect for N3 (for example we could
> be flexible with a selection rule and hope for different
> approaches) and concentrate on the logic instead.
>
> Proofs will also certainly help for debugging but they rather
> help in cases where unexpected derivations happen. When I expect a
> result which I then do not get, there is also no proof to check
> what happened (no proof for something which is not true).
>
>
> N3, as implemented in cwm, was an attempt to attack the
> problem by one person (with some advice from a few others -- I
> don't mean to minimized DanC's role, but I think he'd agree
> the vision was Tim's) who had no experience with existing
> rule-based system or familiarity with the literature, so the
> design ended up rather idiosyncratic. At the other end of the
> spectrum, RIF was an attempt to attack this problem by a
> committee which included experts in many different kinds of
> rule-based systems, so it ended up rather complicated and full
> of options. I joined Tim's group a few weeks after cwm
> started, in late 2000 and was staff contact for RIF from
> chartering <https://www.w3.org/2005/rules/wg/charter> through
> Recommendation <https://www.w3.org/TR/rif-overview/>. I might
> be the only person involved in both projects.
>
> I'd love to see something simple and elegant enough it
> actually catches on. I highly doubt that will be classic N3,
> in all its self-referential glory (the "implies" operator is
> just an RDF predicate!), or RIF, in all its complexity.
>
> I agree with both points and hope to find a practical solution
> here. I also think that we should consider the work already done
> in the past on N3 and RIF, so I am glad that you share your
> experience.
>
> If this group just wants to nail down N3, more or less as
> implemented in cwm (and perhaps EYE), then more power to it, I
> wish it well. I'll try to follow the progress from time to time.
>
> On the other hand, I rather hope it ends up evolving into a
> language which really fits the needs of application
> developers. That would be awesome.
>
> I also think that this should be the goal of the group should be
> to find a practical rule language which fits the needs of
> developers. Nevertheless, I also think that we should not be too
> ambitious either to be sure to not deviate from our goal of
> specifying a standard. So, maybe we start with N3 as it is and
> "fix" what according to the experience of the people in this group
> needs to be present in a rule language?
>
> I hope that you can help us here with all the lessons learned from
> the two other groups.
>
>
>
>
> * Together with the formalisation we should also discuss
> whether we provide a reference implementation together
>
>
> In general, in standards work, reference implementations are
> not a great idea. It's much better, if possible, to have
> multiple independent implementations and a shared test suite.
> Every substantive decision by the group -- that is, a decision
> that might affect whether some implementation conforms to the
> spec -- as well as every normative statement in the spec
> should be recorded as multiple tests added to the test suite,
> showing the correct way for reasoners to behave. For a rule
> language, positive-entailment and negative-entailment tests
> are most of what you probably want. Of course there are also
> positive-syntax and negative-syntax tests. See, for example,
> https://www.w3.org/TR/rif-test/
>
>
> Thank you for your advice. So, let's simply drop the point of a
> joint reference implementation then and write some test cases instead.
>
> Regards,
> Doerthe
>
> --
>
> Dörthe Arndt
>
> Researcher Semantic Web
>
> imec - Ghent University - IDLab | Faculty of Engineering and Architecture | Department of Electronics and Information Systems
>
> Technologiepark-Zwijnaarde 19, 9052 Ghent, Belgium
>
> t: +32 9 331 49 59 | e:doerthe.arndt@ugent.be <mailto:doerthe.arndt@ugent.be>
>
> --
> Dörthe Arndt
> Researcher Semantic Web
> imec - Ghent University - IDLab | Faculty of Engineering and Architecture | Department of Electronics and Information Systems
> Technologiepark-Zwijnaarde 19, 9052 Ghent, Belgium
> t: +32 9 331 49 59 | e:doerthe.arndt@ugent.be <mailto:doerthe.arndt@ugent.be>
--
Dörthe Arndt
Researcher Semantic Web
imec - Ghent University - IDLab | Faculty of Engineering and Architecture | Department of Electronics and Information Systems
Technologiepark-Zwijnaarde 19, 9052 Ghent, Belgium
t: +32 9 331 49 59 | e:doerthe.arndt@ugent.be
Received on Friday, 14 December 2018 16:28:38 UTC