Closing the world

[william-vw]

In my personal experience, the lack of this option (closure axioms exist in OWL but are rather limited) is a major bummer when using Semantic Web technology in general. I understand (/ assume) that the choice for only allowing an open-world-assumption relates directly to the "Web" part, i.e., one cannot reasonably assume that another Web data source does in fact have the missing statements.

But there are so many practical cases where a closed world would make much more sense, with its support for universal quantification and negation-as-failure. I'm not arguing pro or con an open-world-assumption—I'm sure it has its uses, such as inferring statements to explicate assumptions in the open world—but rather making constructs available that better allow one to close the world. Just to illustrate, in a recent work related to clinical decision support, I had to resort to writing a "NOWA" class that implemented a closed world to support universal quantification and complementary classes (I used OWL2 RL to realize a subset of OWL2 DL) .. In this particular setting, where all data was locally available, such a feature made a lot of sense.

For instance, one could set a scope in a formula to only consider all terms mentioned in an RDF graph or document.

[gkellogg]

Note that the contents of named graphs/formulae are inherently closed, as the graph name is effectively a blank node, with no way to be referenced from any other datasource. It's only the default graph which is inherently open.

Of course we could consider that the owl:sameAs/= properties can be used to name formulae, and could provide some open-world semantics to named graphs.

[doerthe]

Related to the previous remark: I think that scoped negation as failure is something we could support here. If you clearly name the graph(s) which did not contain any data leading to a certain conclusion in your negation like

(:graph1 graph2) :notEntail {:a :b :c}.

(in practice we might need a better way to represent it), you do not harm the open-word assumption. And I do not think that you have cases where you can't name the graphs you use for reasoning.

[william-vw]

The the latest case where I ran into this issue pertained to predicate logic-style universal quantification (I will post later about another case). As a simplified (and a bit contrived) example, I needed to classify all composite tasks that only comprise completed tasks (called AllTasksCompleted). You can use owl:allValuesFrom (see here) to represent this case, but a reasoner will not infer the particular type for a resource that, at least in the local graph, adheres to this constraint. For instance, the following

EquivalentClasses(:AllTasksCompleted ObjectAllValuesFrom(:contains :CompletedTask))

Will not yield infer the type AllTasksCompleted for a resource that is only linked (using contains) to instances of type CompletedTask. I added a test file to the repository.

In the context of an open world this makes sense - making this inference requires assuming that there's no other graph that links the resource to another resource, i.e., not of type CompletedTask. At the time I was using OWL2 RL (and Apache Jena) to implement a subset of OWL2 DL reasoning, but the same goes for a full OWL2 DL reasoner.

When N3 people talk about universal quantification it doesn't seem to comprise examples where every predicate must fulfill the constraint before an inference can be made - rather it means that an inference will simply be made for each value of the predicate (i.e., the same default behavior most rule languages produce for variables in general). See e.g., the TBL spec:

{ @forAll x, y, z. {x parent y. y sister z} log:implies {x aunt z} }

Whereas I would be hoping for the following logic (apologies for abuse of syntax):

{ @forSome ?composite . @forAll ?atomic . ?composite . :contains ?atomic :: ?atomic a :CompletedTask } => { ?composite a :AllTasksCompleted . }

I.e., if a composite exists, where all atomic that are linked to it using contains, the condition holds that atomic has type CompletedTask, we can infer the type AllTasksCompleted for composite. Before one starts focusing on the syntax or standard N3 specs, I know that this is not proper N3 syntax.

[william-vw]

This case seems like a classic case of negation-as-failure. I needed to annotate all tasks that were not discarded - i.e., not annotated with DiscardedTask type - as instances of a NotDiscardedTask class. One can create an OWL DL class that is the complement of the DiscardedTask class, but like before, a DL reasoner will not retrieve the instances for this complement class.

I.e., I can imagine that the following rule could be appropriate:

{ naf (?task a :DiscardedTask ) } => { ?task a :NotDiscardedTask }

In fact, I believe this is referred to as Scoped Negation As Failure (SNAF) in the TBL spec, initially discussed in the W3C Workshop on Rule Languages for Interoperability. In case a scope is carefully indicated - similar to the universal quantification I talked about above - then I think this could be a very useful feature.

[doerthe]

Your example brought me back to another issue I forgot to raise (but I will do that): which built-in functions do we include?

Given that you could point me to a discussion where snaf was already mentioned in N3 , I had a look how we could solve your problem using only Cwm builtins. Scoped negation as failure can be expressed by using a combination of log:semantics and log:notIncludes, an example rule for your input could be:

{?t a :CompositeTask. ?t :contains ?st. <owa.n3> log:semantics ?x. ?x log:notIncludes {?st a :CompletedTask }}=>{ ?t a :NotAllTasksCompleted.}.

This rule works in EYE and by commenting out a :x a :CompletedTask. you get the expected output (ie :compositeTask1 a :NotAllTasksCompleted. ). I added the example to our git.

Unfortunately, this does not solve your first problem and I am currently trying to find a solution for that by only using Cwm built-ins.

Note, that your example requires a special kind of scope for the universal quantifier (sometihnig like: all contained tasks which are listed in the document). In EYE, the predicate e:findall does that job, an example rule would be:

{?t a :CompositeTask.  _:x e:findall (?st { ?t :contains ?st.} ?tasklist). }=>{?t :containsList ?tasklist }.

This rule here produced as list of all tasks mentioned in your document which are contained in your composite task. The scope in this rule here is somehow hidden since I only used a blank node. If you have a closer look at the proof, you will see that this blank node _:x gets replaced by a scope in the proof. To solve your problem, we can use a second rule (the example was solved ad-hoc, maybe it is also possible to have just one rule):

{?t a :CompositeTask. ?t :containsList ?tasklist.   _:x e:findall (?st { ?st list:in ?tasklist. ?st a :CompletedTask.} ?tasklist). }=>{?t a :AllTasksCompleted }.

This rule compare the list of the task contained in your composite task with the tasks of this list which are completed. It only fire for a composite task for which all tasks are completed.

I also added the example on git. You can test by commenting in or out the fact that one subtask is completed in the ontology file.

I do not say that this is the best solution to your problem and that we should define a built-in that solves it like that. But I am convinced that your problem can be solved by the choice of the right built-ins and what I uploaded are possible examples.

[doerthe]

When N3 people talk about universal quantification it doesn't seem to comprise examples where every predicate must fulfill the constraint before an inference can be made - rather it means that an inference will simply be made for each value of the predicate (i.e., the same default behavior most rule languages produce for variables in general). See e.g., the TBL spec:

{ @forAll x, y, z. {x parent y. y sister z} log:implies {x aunt z} }

Whereas I would be hoping for the following logic (apologies for abuse of syntax):

{ @forSome ?composite . @forAll ?atomic . ?composite . :contains ?atomic :: ?atomic a :CompletedTask } => { ?composite a :AllTasksCompleted . }

I.e., if a composite exists, where all atomic that are linked to it using contains, the condition holds that atomic has type CompletedTask, we can infer the type AllTasksCompleted for composite. Before one starts focusing on the syntax or standard N3 specs, I know that this is not proper N3 syntax.

Please note that from a strict logical point of view, we already have what you want by allowing nested quantifiers (I will come back to quantifiers in the other issues, but I already say how this can be logically represented)

{ ?t a :CompositeTask. @forAll :atomic . { ?t :contains :atomic} => {:atomic a :CompletedTask} } => { ?t a :AllTasksCompleted . }.

This rule can be translated to: if a task is a composite task andwe know that for all tasks that if they are contained in the task then the task is completed, then we can conclude that the task as a whole is completed.

Unfortunately, even if reasoners could deal with that rule (which is difficult on its own), that rule would not solve your problem. Even with your kind of scope, we still have an open world and we simply do not know whether or not there is a hidden task somewhere out there in the web which is not completed but contained in your composite task. So, what we really need is some reference to the data sources you want to search in. If these are explicitly mentioned as in the example of the cwm built-ins (with the eye solution we already have the problem that the scope is not defined while writing down the rule, that is a problem, but I know that that has practical reasons) we are fine here.

So, what we can do is something like the following:

{ ?t a :CompositeTask. 
@forAll :atomic .
   { <owa.n3> log:semantics ?x. ?x log:includes { ?t :contains :atomic}}
    =>
   {<owa.n3> log:semantics ?x. ?x log:includes {:atomic a :CompletedTask} } 
=> { ?t a :AllTasksCompleted . }.

Since this rule requires much more reasoning then simple resolution, I guess that no reasoner will actually derive the desired result. I just added this example to show that with the built-ins of cwm we can already express the scope as you want it here. But I believe that here we need to make a practical compromise and define a built-in.

[william-vw]

@doerthe Thanks for your answer (which is quite elaborate, as usual! In a good way, lol.). I think that we're in agreement that, ideally, we should define proper constructs in N3 to support those cases in an expressive way, i.e., without having to chain existing reasoner built-ins in ways that are rather unclear (nevertheless, I appreciate your efforts in that regard!).

In fact, I'm a bit unsure what you mean with "built-in" - afaik a built-in is the implementation of particular construct (e.g., to support lists, ..) that is specific to a reasoner, i.e., typically not supported by any other reasoner (Apache Jena has a bunch of those). I could of course be wrong - but if we're on the same page then perhaps we could use "construct" instead of "built-in" to avoid confusion (?)

[doerthe]

By built-in I mean any N3 uri with a pre-defined meaning which directly effects the reasoning (without making a rule for this uri). By this definition, rdfs:range for example would be a built-in for rdfs while it has no special meaning for rdf.

In the discussion above, I specifically meant built-ins as they are defined for cwm and for EYE.

These can either be specific for a reasoner (ideally under the reasoner's namespace) or they could be part of the logic. We only need to discuss what we want to consider as part of the logic. Good candidates for that are all concepts in the swap context (if you go to the above built-in lists, they have "swap" in their uri).

Maybe we call them N3-predicates (if they are predicates) to avoid the confusion you mention above?

[gkellogg]

Of these, I think the list, some of the log, math, string, and time built-ins are generally useful, although any normative requirements to support them may be in separate documents, so it's not an all or none case.

For the log built-ins, obviously implies is necessary. equalTo (although sameTerm might be clearer), includes, notEqualTo, notIncludes, rawType, and uri seem useful. Things that load documents, such as semantics and content we should consider, but they have quite a bit of implications outside of N3 itself.

[william-vw]

@doerthe said:

Maybe we call them N3-predicates (if they are predicates) to avoid the confusion you mention above?

Yes, I'd rather call them predicates/constructs in case the N3 (or any other) spec formally defines then. To me a "built-in" is specific to a particular implementation (hence the term).

[dbooth-boston]

FWIW, in computer science and software development I have always understood the term "built-in" to mean that the function is already implemented in the software that is being discussed, as opposed to requiring the user to supply a definition of it. Being a built-in function does not imply that it is specific to an implementation. Many built-in functions are standardized across all conforming implementations, such as basic arithmetic operations in a programming language.

[doerthe]

Related to that issue but not the same. What do we do with the expression:

{:a :b :c}=>false.

This is valid N3 and the use of false here is different then for example in a triple:

:Socrates :isAlive false.

I will not yet tell my opinion here or explain problems since I would like to know how someone who hasn't thought a lot about it understands it when he or she sees it for the first time.

[wwaites]

This is valid N3 and the use of `false` here is different then for example in a triple: `:Socrates :isAlive false.'

In particular, is the meaning different from: { :Socratese :isAlive true } => false and if so, what is the difference, precisely? Does the problem arise because we only have binary predicates and not unary predicates and so the object in your triple is more of an artefact than a meaningful token?

[william-vw]

@wwaites

This is valid N3 and the use of false here is different then for example in
a triple:

`:Socrates :isAlive false.'
In particular, is the meaning different from:

{ :Socratese :isAlive true } => false

Just my two cents: looking at the truth table I'd guess that when Socrates is alive then the implication (i.e., whole expression) would be false, and when he's not alive then the implication would be true (?) Unsure what the practical use of it would be - imo it's not the same as saying that Socrates is not alive.

[doerthe]

I raised the question because I wanted to know whether or not you understand a construct like
{ :a :b :c } => false.
as a negation or not.

false stems from RDF and is there a boolean literal which can occur in a triple. In N3 we now somehow mix up formulas and triples (which has many advantages) and we now understand the literal also as the truth constant false which stands for a formula (just like the "normal" false or bottom from first order logic).

We cannot have the "normal" truth constant because the syntax forces us into a triple structure.
math:False.
is not a valid formula.

We can understand the example I gave above as explicit negation.

Alternatively, we could also say that it is not that different from something like
{ :a :b :c } => :z.
which I would understand as some random triple without special meaning.

From a practical point of view rules as the example can help to detect problems. I could for example say that I want to immediately stop reasoning if I find out that a person is dead and alive at the same time:

{?x :isAlive true. ?x :isAlive false} => false.

But such things as explicit negation also make the logic more complex. the case above could also be solved by some kinds of warning:

{?x :isAlive true. ?x :isAlive false} => { :warning :message "Schroedinger alarm"}.

So, what do we do with false?

[william-vw]

Indeed, I suppose there's multiple ways to look at it:

• having this implication with a true antecedent and false consequent means that the KB would contain an assertion (i.e., implication) that is false in its entirety - i.e., you're not saying that "a b c." is false (negation) but rather that, when the antecedent holds, the implication "{ :a :b :c } => false" is false. When this occurs, this could then be considered an inconsistency in your KB (cfr. your dead & alive example)

• to ensure the truth of the assertion (i.e., implication) in light of the false consequent, and hence avoid a KB inconsistency, the reasoner needs to infer that the antecedent is false as well (cfr. negation).

It's an interesting problem - if one considers the OWL semantics one can easily find examples that do not involve an explicit false as consequent but one that would be inconsistent with the knowledge already present.

For instance:
:wineryLocation a owl:FunctionalProperty . :BordeauxWine rdfs:subClassOf :Wine .
:Bordeaux a :FrenchLocation . :RhineValley a :GermanLocation .
:StrangeWine :wineryLocation :RhineValley . :StrangeWine a BordeauxWine .
(?w a :BordeauxWine) -> (?w :wineryLocation :BordeauxLocation)

Since :wineryLocation is a functional property and :StrangeWine now has two winery locations, a reasoner would try inferring an equivalency between both locations - but since German and French locations are disjoint this would trigger an inconsistency. Perhaps one could also see this as the consequent being false since it is in (DL-)contradiction with the current KB?

[dbooth-boston]

having this implication with a true antecedent and false consequent means that the KB would contain an assertion (i.e., implication) that is false in its entirety - i.e., you're not saying that "a b c." is false (negation) but rather that, when the antecedent holds, the implication "{ :a :b :c } => false" is false. When this occurs, this could then be considered an inconsistency in your KB (cfr. your dead & alive example)

That is definitely the way I look at it, because I tend to think operationally in terms of forward chaining, rather than backward chaining. I would probably use a rule of that form only for error checking, to flag an inconsistency in my data.

My own desire for negation is mainly -- only? -- for writing rules under the CWA, such as to find all tasks that have not been completed.

[william-vw]

In favor of closing this issue, since I think the WG landed on interpreting { :a :b :c } => false. as an integrity constraint, instead of explicit negation (see meeting 26th June, 2019 .. quite a while ago). Also, we have a separate issue on built-ins for CWA #18