Open RubenVerborgh opened 2 years ago
Related to #42. (underlying solution could solve both challenges)
@rubensworks Does that mean that you can a separate challenge that covers the "core" problem?
Yes, will look into that later.
@jeswr there is a very rough initial prototype at https://josd.github.io/eyebrow/cha58.html and it is using the data from https://github.com/josd/eye/tree/master/reasoning/cha58 reasoning and proof construction happens in the browser and the following shows why you could trust it ;-)
<#lemma5> a r:Inference;
r:gives {
:johnD a schema:Person.
};
r:evidence (
<#lemma6>
<#lemma7>
<#lemma8>
);
r:binding [ r:variable [ n3:uri "http://josd.github.io/var#x_0"]; r:boundTo [ n3:uri "http://example.org/ns#johnD"]];
r:binding [ r:variable [ n3:uri "http://josd.github.io/var#x_1"]; r:boundTo [ n3:uri "http://example.org/ns#Pod1"]];
r:rule <#lemma9>.
<#lemma6> a r:Extraction;
r:gives {
:johnD a foaf:Person.
};
r:because [ a r:Parsing; r:source <http://josd.github.io/eye/reasoning/cha58/cha58-data.n3>].
<#lemma7> a r:Extraction;
r:gives {
<<:johnD <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> foaf:Person>> :from :Pod1.
};
r:because [ a r:Parsing; r:source <http://josd.github.io/eye/reasoning/cha58/cha58-data.n3>].
<#lemma8> a r:Extraction;
r:gives {
:Pod1 :usingOnly foaf:Person.
};
r:because [ a r:Parsing; r:source <http://josd.github.io/eye/reasoning/cha58/cha58-data.n3>].
<#lemma9> a r:Extraction;
r:gives {
@forAll var:x_0, var:x_1. {var:x_0 a foaf:Person.
<<var:x_0 <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> foaf:Person>> :from var:x_1.
var:x_1 :usingOnly foaf:Person} => {var:x_0 a schema:Person}.
};
r:because [ a r:Parsing; r:source <http://josd.github.io/eye/reasoning/cha58/cha58-rules.n3>].
@josd this is a great start - on the proof side I think the next step is to work out how to include versioning in the solution.
Orthogonally I will continue to properly look into hooking this into Comunica this evening so we can have a working prototype with query (I've been a bit side-tracked with other tasks this morning).
Very cool; I'll just add my own notes below, as clarifications for myself and others who might stumble upon this thread.
The example has as data in https://josd.github.io/eye/reasoning/cha58/cha58-data.n3:
:johnD a foaf:Person {| :from :Pod1|}.
:lisaM a schema:Person {| :from :Pod5|}.
:Pod1 :usingOnly foaf:Person.
:Pod5 :usingOnly schema:Person.
The above is Turtle-star notation, such that {| … |}
is an annotation on the triple; so it asserts the triple (i.e., :johnD a foaf:Person
) and it also adds a note (in this case "I got this from Pod1").
Thought: this does put statements from Pods 1 and 5 in the same graph, such that cross-inferences between them are possible. This might or might not be desired.
The :usingOnly
annotation reflects the schema of the Pod; this is something we indeed can and should declaratively capture. Today, this piece of knowledge is not assumed to be there (to the extent that app developers assume it is not and cannot be there), but it's indeed a piece of knowledge we will need to rely on in the future. So makes a lot of sense. Of course, the descriptions will be more complex then this here (perhaps a SHACL shape), but the bottomline is the same: the reasoner has this info.
We're just looking for all schema:Person
instances:
{?X a schema:Person} => {?X a schema:Person}.
And then finally there is https://josd.github.io/eye/reasoning/cha58/cha58-rules.n3:
{?X a foaf:Person{| :from ?POD |}. ?POD :usingOnly foaf:Person} => {?X a schema:Person}.
which I assume would be autogenerated (how?).
In practice, this ontological knowledge will probably be separated; as in schema:Person owl:equivalentClass foaf:Person
and a separate OWL rule { ?x a ?c. ?c owl:equivalentClass ?d } => { ?x a ?d }.
but that doesn't matter here; the query rule is the consequence of this. (Side-note: can we generate EYE queries then based on such knowledge and a concrete case?)
To what extent is the ?POD
condition necessary, given that it is only an annotation? If we just had {?X a foaf:Person} => {?X a schema:Person}.
I'd also expect it to work?
(Side-note, I tried to confirm this with https://drive.verborgh.org/tmp/2022/cha-58-direct.n3, but I couldn't figure out how to wcache
it in the browser 🙂)
Similarly, do we want to track provenance, so have … => {?X a schema:Person {| :from ?POD |}}
? But I guess the proof serves the same purpose, so I am fine with that. (But that then begs the question, to what extent can the initial :johnD a foaf:Person {| :from :Pod1|}
annotation also not just be captured with a previous proof?)
Very promising, absolutely great to see this happening!!
To what extent is the
?POD
condition necessary, given that it is only an annotation? If we just had{?X a foaf:Person} => {?X a schema:Person}.
I'd also expect it to work?
Yes indeed, it is logically sufficient to have {?X a foaf:Person} => {?X a schema:Person}.
but we wanted to make it a pragmatic rule with more additional explicit assumptions that are the shown in the proof explanation.
(Side-note: can we generate EYE queries then based on such knowledge and a concrete case?)
Very much indeed, the rule generating the query would look like { ?c owl:equivalentClass ?d } => {{ ?x a ?c } => { ?x a ?d }}.
or more pragmatically as you indicated @RubenVerborgh only when we have an appropriate instance { ?i a ?c. ?c owl:equivalentClass ?d } => {{ ?x a ?c } => { ?x a ?d }}.
and of course also { ?i a ?d. ?c owl:equivalentClass ?d } => {{ ?x a ?d } => { ?x a ?c }}.
we wanted to make it a pragmatic rule with more additional explicit assumptions that are the shown in the proof explanation.
Hah, perfect, if only we had had RDF-star when we were doing RESTdesc!
Hah, perfect, if only we had had RDF-star when we were doing RESTdesc!
What can happen will happen, call it RESTdesc-star 🐶
@josd and I had a good discussion about this yesterday. From that I am going to forge ahead with plugging Eye in as a reasoning engine to Comunica (which I made a large amount of progress with today, and am close to completion).
After this point I would consider the challenge to be pretty well completed.
--
From there the steps are:
@jeswr:
Continue work on RDF-star support for Comunica so we can annotate the source of a triple, or the proof that was used to deduce the triple.
@josd
Will look into using RDF-star annotations of triple sources in the proof rather than document input into Eye.
The immediate reason for this is to enable proofs that can refer to non-document based sources such as aggregator APIs but that is just the tip-of-the iceberg.
From that I am going to forge ahead with plugging Eye in as a reasoning engine to Comunica (which I made a large amount of progress with today, and am close to completion).
I assume this will fit into the reasoning bus you've created before?
Continue work on RDF-star support for Comunica so we can annotate the source of a triple, or the proof that was used to deduce the triple.
Could probably do a very similar thing to: https://github.com/comunica/comunica-feature-link-traversal/tree/master/packages/actor-rdf-resolve-hypermedia-links-traverse-annotate-source-graph
If relevant, we may want to consider moving the graph and RDF* actors into base Comunica.
From there the steps are:
@jeswr:
- Continue work on RDF-star support for Comunica so we can annotate the source of a triple, or the proof that was used to deduce the triple.
@josd
- Will look into using RDF-star annotations of triple sources in the proof rather than document input into Eye.
The latest release of eye https://github.com/josd/eye/releases/tag/v22.0814.1056 should support all of that including the discussed use of Skolem IRIs. For an example see https://github.com/josd/eye/blob/master/reasoning/socrates/socrates-proof.n3 which is a proof generated using https://github.com/josd/eye/blob/master/reasoning/socrates/socrates.n3. The latter is containing N3-star annotations of triple/rule sources. The proof checker is also happy with the new proofs.
I assume this will fit into the reasoning bus you've created before?
Yes, just with a small addition of adding an N3Store to the context where proofs can be placed.
Done quite some improvements in eye reasoning in the browser and https://josd.github.io/eyebrow/cha58.html still does reasoning and proof construction in the browser as expected.
Please provide a status update about this challenge. Every ongoing challenge needs at least one status update every 2 weeks. Thanks!
There is an updated prototype using RDF+surfaces for the logic and RDF-star for the explanation at https://github.com/josd/eye/tree/master/reasoning/cha58 and it runs in the browser at https://josd.github.io/eyebrow/cha58.html
Seems like the reasoning part is working indeed! Can I see an end-to-end demo of this somewhere? Perhaps there should be as small separate repository where I enter the SPARQL query for schema:Person and then get foaf:Person back?
Right and if I remember well from our last review meeting, this is exactly what @jeswr mentioned and would take him a few hours?!
Please provide a status update about this challenge. Every ongoing challenge needs at least one status update every 2 weeks. Thanks!
Based on discussions today, we might be able to complete this challenge this week!
Please provide a status update about this challenge. Every ongoing challenge needs at least one status update every 2 weeks. Thanks!
Pitch
A group of friends store
foaf:Person
data in their pods. One of the friends issues a SPARQL query forschema:Person
and wants to find all people data in the network. They trust that the resulting list of people is correct and complete.Desired solution
schema:Person
tofoaf:Person
schema:Person
fromfoaf:Person
Acceptance criteria
schema:Person
and makes no mention to FOAFPointers
Scenarios
People of interest
@josd @rubensworks @jeswr