Reasoning with modal relations

[nklsbckmnn]

Let's look at the following case.

Artifact Function Specification =def. A Directive Information Content Entity that prescribes some Artifact Function and which is part of some Artifact Model.

Asserted triples:

a instance of Directive Information Content Entity
a part of some Artifact Model
b instance of Artifact Function
a MRO:prescribes b

What I'd like to infer:

a instance of Artifact Function Specification

This obviously does not work because the class axiom uses http://www.ontologyrepository.com/CommonCoreOntologies/prescribes. Is there a recommended way to deal with this?

Is an application for example expected to convert MRO relations to non-MRO relations for reasoning, then convert possibly inferred triples (in this case there are none that correspond to relations) back to MRO?

[rorudn]

I won't say it's recommended but as a stopgap I would use a SPARQL construct query.

We can take a look at supplementing the Modal Relations Ontology with axioms that would derive the needed conclusions for the entities related via modal properties.

[nklsbckmnn]

@rorudn Thanks for the helpful reply.

Another example:

Artifact Function Specification =def. A Directive Information Content Entity that prescribes some Artifact Function and which is part of some Artifact Model. (Subclass of axiom: prescribes some Artifact Function)

I assume the following is asserted:

Directive ICE i mro:prescribes Artifact Function Specification m

If now m doesn't mro:prescribe any Artifact Function, I would expect the graph to be invalid.

Edit: The asserted triple mentioned didn't make sense.

[mark-jensen]

Agree it's a worthwhile to offer a slim of MRO axioms for users that want them. I think these should be maintained in a separate file from MRO.ttl and either imported into it or left as a standalone supplement.

[alanruttenberg]

Would you not want to infer a MRO:instance of Artifact Function Specification?
If an entailment is based on a modal relation shouldn't it be modal as well?

[nklsbckmnn]

@alanruttenberg I don't think so.

(1) If it is sufficient for an entity afs1 to mro:prescribe some Artifact Function to be an instance of Artifact Function Specification and afs1 mro:prescribes af1, then afs1 is an instance of Artifact Function Specification even if

(a) af1 does not really exist

or, if we assume that modal relations can have existing or non-existing objects (which makes sense to me),

(b) wether af1 exists or not.

I guess the relation under this interpretation is not really modal, just its object. There is no modality on the side of the subject. This interpretation enables us to "quote" modal relations in axioms.

(2) If alternatively we want to say that it is necessary for an entity afs1 to prescribe some actually existing instance of Artifact Function to be an instance of Artifact Function Specification (which I think we don't), but only afs1 mro:prescribes af1 is assertable and not (also) afs prescribes af1, then I guess it could make sense to say that afs1 is only a possible instance of Artifact Function Specification. Although there is the problem that instance_of is not an explicitly defined relation.

[alanruttenberg]

I think the reasoning is incorrect. The semantics of modal logic involves possible worlds and an accessibility relation - which possible worlds are "accessible" from a give world. Usually (I'm told) the accessibility relation is assumed to be every world can access every other world, so we'll assume that. Then, two operators are defined, possibly (diamond) and necessarily (box). I'll write those as <> and []

<> assertion means that the assertion is true in some world that is accessible from the world in which it is asserted.
[] assertion means that the assertion is true in every accessible world, which implies the unqualified assertion is true as well.

When you write a "MRO:prescribes b" the interpretation would be <> "MRO:prescribes b" since otherwise why bother.

If the relationship is modal, that means it doesn't necessarily exist in this world, but does in some hypothetical world. Conclusions which include a modal assertion are modal themselves, i.e. they are also true in some possible world.

It is possible you are assuming that "b MRO:prescribes a" (= <> b prescribes a) implies "a prescribes some Thing". Paraphrased:

If a MRO:prescribes something specific then
a prescribes something (though not necessarily of same type that was asserted using the MRO relation).

From that you can conclude that a it is an Artifact Function Specification without knowing what it specifies. But there are other single triple assertions that would also work, like "b instance of Artifact Function Specification"

An alternative would be to add the above explicitly. That would be a GCI.

(MRO:prescribes some Thing) subClassOf (prescribes some Thing) .

If that's the intended semantics for all MRO relations, add an assertion like this for each relation.

There's still stuff to worry about. There aren't modal entities or modal instance-of relationship. That means that you have to be careful to not conclude actual world things from modal things unless it is justified.

For this example, I have the domain and range assertions asserted on prescribes, but not on MRO:prescribes. That's because if they were on MRO:prescribes, the translation for range would be if "a MRO:prescribes b" then "b MRO:instanceOf Directive Information Entity". Since there's now MRO:instanceOf there's nothing you can say in it's place.

Here's a sketch where the desired conclusion arises, and picture of the explanation.

Declaration(Class(:Artifact_Function))
Declaration(Class(:Artifact_Function_Specification))
Declaration(ObjectProperty(:possibly-prescribes))
Declaration(ObjectProperty(:prescribes))
Declaration(NamedIndividual(:a))
Declaration(NamedIndividual(:b))

ObjectPropertyDomain(:prescribes :Artifact_Function_Specification)
ObjectPropertyRange(:prescribes :Artifact_Function)

ObjectPropertyAssertion(:possibly-prescribes :a :b)
ClassAssertion(:Artifact_Function :b)

SubClassOf(ObjectSomeValuesFrom(:possibly-prescribes owl:Thing)
	   ObjectSomeValuesFrom(:prescribes owl:Thing))

[nklsbckmnn]

@alanruttenberg

Under interpretation (1), triples using MRO relations in OWL at first sight simply do not have the same semantic and syntax as triples in modal logic. Think of a whole new operator.

Under interpretation (2) they do. But, as you say, we do not have the modal instance of relation and also we might not want to always need it because we might want a "Artifact Function Specification" to be of that type independent of whether the referent exists or not.

Another question is if (1) can be made to conform to relations from modal logic somehow, e. g. by adding assumptions.

It is possible you are assuming that "b MRO:prescribes a" (= <> b prescribes a) implies "a prescribes some Thing".

I am not as far as I understand and I don't at first sight understand how it would help.

I would, if necessary, accept the assumption "a prescribes b -> a mro:prescribes b" if that solves anything.

[alanruttenberg]

It helps because it makes explicit what I think is the unspoken assumption. It shows that if we make that assumption then the conclusion you wanted to have happens. It does that in a way that i believe doesn't mix modal with actual, other than that sanctioned by the GCI.

The assumption you are offering is []p => <>p. It's a perfectly reasonable axiom. It doesn't help.

Maybe we should start earlier. Why did you think the "a instance of Artifact Function Specification" should be inferred from your assertions?

More generally, what do you propose the semantics of MRO:prescribes is? Or of MRO relations in general?

Alan

[nklsbckmnn]

I would need to think about this a little more... but I unfortunately don't have time until October.

Maybe we should start earlier. Why did you think the "a instance of Artifact Function Specification" should be inferred from your assertions?

I think we can agree on this:

If every Directive Information Content Entity that prescribes an Artifact Function is an Artifact Function Specification, then, if x instance of Directive Information Content Entity and x prescribes some Artifact Function, x is an instance of Artifact Function Specification.

And I think we can also say this:

If every Directive Information Content Entity that mro:prescribes an Artifact Function is an Artifact Function Specification, then, if x instance of Directive Information Content Entity and x mro:prescribes some Artifact Function, x is an instance of Artifact Function Specification.

More generally, what do you propose the semantics of MRO:prescribes is? Or of MRO relations in general?

Every ICE is about ONE possible world specific to this ICE. All of the asserted MRO relations belonging to that world are true in that world.

If we know the truth value in the actual world, then there is a corresponding non-MRO relation.

Knowing which MRO relation belongs to which ICE is a little complicated unless subgraphs are separated.

That's why I proposed to use a separate MRO subnamespace for every ICE. #97

I do not envision nested namespaces/possible worlds though.

ice1 is mro:ice1:about ice2
ice2 is mro:ice2:about e1

but not

ice1 is mro:ice1:about ice2
ice2 is mro:ice1:ice2:about e1

[alanruttenberg]

I would need to think about this a little more... but I unfortunately don't have time until October.

Maybe we should start earlier. Why did you think the "a instance of Artifact Function Specification" should be inferred from your assertions?

I think we can agree on this:

If every Directive Information Content Entity that prescribes an Artifact Function is an Artifact Function Specification, then, if x instance of Directive Information Content Entity and x prescribes some Artifact Function, x is an instance of Artifact Function Specification.

Yes.

And I think we can also say this:

If every Directive Information Content Entity that mro:prescribes an Artifact Function is an Artifact Function Specification, then, if x instance of Directive Information Content Entity and x mro:prescribes some Artifact Function, x is an instance of Artifact Function Specification.

No. Not in standard modal logic without something extra. Possibly in some other logic, which probably shouldn't be called modal. The CCO documentation says: "A query that filters out the Modal properties will return only the triples associated with the actual mission." This does not do that, because filtering out the modal properties would leave (what should be) a modal assertion that "x is an instance of Artifact Function Specification.". Consider: In some other possible world, x might not prescribe anything, might prescribe something that isn't an function, or just describe something.

Let's recast this with a different example. Suppose have a person and a class murderer and relations murders and MRO:murders. Have a definition that anyone that murders someone is a murderer. Have an assertion that Alan mro:murders John, perhaps a representation of an accusation. You don't want to conclude that Alan is a murderer in the actual world, right? But your proposed inference would sanction the incorrect conclusion about Alan being a murderer.

In fact, I would argue that there should not be any domain and range restrictions for the MRO terms, as any such restriction is a potential leak of something modal into something actual. Maybe there's some way to adjust things so you could have domains and ranges, but then the domain and range classes should be modal versions of the classes. And, in that case, the CCO doc would have to say: "A query that filters out the Modal properties and any assertion with either a subject or object with a modal type will return only the triples associated with the actual mission."

If you are going to have the inference you want, a assertion about the actual world, then you need an axiom of the sort: <> a MRO:prop b => [] a prop b . The GCI I offered is an approximation of that.

I'm not saying you can't have your inference, just that you have to understand and ideally represent what you are assuming in order to arrive at it.

More generally, what do you propose the semantics of MRO:prescribes is? Or of MRO relations in general?

Every ICE is about ONE possible world specific to this ICE. All of the asserted MRO relations belonging to that world are true in that world.

And you can conclude anything else you want about the actual world?? Because that's what you are doing.

If we know the truth value in the actual world, then there is a corresponding non-MRO relation.
Knowing which MRO relation belongs to which ICE is a little complicated unless subgraphs are separated.

I don't think I understand what you mean about a relation belonging to an ICE. I'm still not understanding the model.

That's why I proposed to use a separate MRO subnamespace for every ICE. #97

Didn't read it in detail but perhaps it aligns with what I suggested regarding modal classes. While I made the suggestion, I'm dubious it will be workable, for other reasons.

Here is the way I am advising people on another project to record and reason with possible world assertions. First, you reify any assertions you want to make in a possible world. A reification corresponds to something like someone saying that something is true, but without necessarily believing it. Then, when you want to reason with a subset of those statements you translate the reified statements into actual assertions, add them to the KB (i.e. temporarily "believe" them), and see the consequences. You can do that either with the OWLAPI or with SPARQL CONSTRUCT. Then you retract temporarily "believed" assertions so you are back in this world. I believe GraphDB has enough machinery to handle this sort of thing, meaning when you retract an assertion any entailments that depend on that assertion are also retracted. See their reasoning page

The benefit of this approach is that you can easily associate other information about the reified statement, such as confidence, provenance, etc. and then use that information to select candidate sets of statements to temporarily "believe". Also, you don't have to have these MRO shadow relations.

I do not envision nested namespaces/possible worlds though.

ice1 is mro:ice1:about ice2
ice2 is mro:ice2:about e1

but not

ice1 is mro:ice1:about ice2
ice2 is mro:ice1:ice2:about e1

[nklsbckmnn]

There is not much I disagree with.

While I made the suggestion, I'm dubious it will be workable, for other reasons.

Can you elaborate on your doubts? I don't see any other option to be honest.

Also, you don't have to have these MRO shadow relations.

How would you explicitly represent what an ICE in the actual world asserts about a possible world (and how that compares to the actual world) without such "virtual" relations?

[alanruttenberg]

I gave another option, which is to use reifications of statements in the main ontology and then assert as if true but eventually retract subsets of them to determine their implications. One may certainly do a calculation using an ontology - a "what if".

How can we have an ICE that's wrong? Statements are kinds of ICEs and they may or may not be true. "John said the earth is flat" is a perfectly good ICE. It's just that if it is a representation of a proposition, then that proposition is false.
Nonetheless this refers because the parts do "John", "earth", "flat".

Another way I've done it is to refer to types rather than instances. I don't get much OWL mileage out of relationships to punned classes, but I can still do a lot with them in SPARQL.

But at this point, to make further progress, perhaps you could bring a compelling story of how possible worlds would be used, ideally relevant to a project that currently exists one that has clear goals. Then we can look at what representations we need to help achieve one of those goals.

This conversation is so far about technique and if the question is: can we do modal reasoning in OWL, the answer is going to be no. Modal logic is a different logic, and OWL's expressivity is well known and not that.

The other way forward would be to propose a formal semantics for some well-defined subset of modal reasoning that might be able to be done in OWL. Consider it a semantic extension. The RDF specification has some discussion of semantic extensions.

That wouldn't be my first choice. I would rather be problem driven.

[nklsbckmnn]

@alanruttenberg

So here is a new suggestion... I would appreciate your thoughts. I think there is a lot of room for improvement.

Desiderata:
(A) Represent modal relations, instances, classes in a transparent manner (in the same graph) like CCO already tries to do now
(B) Allow representation of modal instance_of
(C) Allow representation of modality of instances that do not have any relations (Not sure if this is necessary)
(D) Allow mapping of modal states of affairs to individual ICEs
(E) Allow quoting of modal relations, classes and instances in definitions of types of ICEs so that e. g. an ICE can (optionally, but only if specified) be typed by what it aims to refer to without actually referring

Suggestion for representation:

• Modal namespace includes relations, instances, classes (A), (B), (C)
• Use an indexed modal namespace for each ICE (D) (MNS:X)
• Use a global, non-indexed modal namespace (MNS) for quotation of modal relations, classes and instances in definitions of non-modal entities (E)

Suggestion for reasoning:

• Reasoning would work as you suggested, by moving each graph from an indexed modal namespace to the prime (non-modal) namespace, reasoning and then moving back to the indexed modal namespace whatever relations (including instance_of relations) were inferred
• An ICE definition containing quoted modal relations (that are not logically treated as modal relations) from the global modal namespace would be validated by temporarily moving the graph from the indexed modal namespace corresponding to the ICE to the global modal namespace.

Example:

Class axioms:
EntityTypeA =def. has_part EntityTypeB
ICETypeA =def. is_about some EntityTypeA or MNS:is_about some MNS:EntityTypeA

Asserted triples:
ice1 MNS:1:is_about MNS:1:entityTypeA1
entityTypeA1 MNS:1:has_part MNS:1:entityTypeB1

Adding relations and instances from namespace MRO:1 to prime namespace:
ice1 is_about entityTypeA1
entityTypeA1 has_part entityTypeB1

Results of inference in prime namespace:
ice1 instance_of ICETypeA

Moving results back to namespace MRO:1:
ice1 instance_of MNS:1:ICETypeA

Adding relations and instances from namespace MRO:1 to global MRO namespace of quoted modal relations:
ice1 MNS:is_about entityTypeA1
entityTypeA1 MNS:has_part entityTypeB1

Results of inference:
ice1 instance_of ICETypeA

[nklsbckmnn]

@alanruttenberg Ignore what I wrote above for a moment.

"Predictive Information Content Entity" has this comment:

Since predictions are inherently about not-yet-existant things, the Modal Relation Ontology term 'describes' (i.e. mro:describes) should be used (instead of the standard cco:describes) to relate instances of Predictive Information Content Entity to the entities they are about.

So I think what we can do is change the logical definition of ICE from

subclassOf Generically Dependent Continuant
equivalentTo is about some Entity

to

subclassOf Generically Dependent Continuant
equivalentTo is about or mro:is_about some Entity

We only need to do this for ICE and all of its subclasses.

If we then add modal classes (and thereby modal instance of) and modal instances, it seems to me at first sight we should be able to reason in a way compatible with standard modal logic.

[alanruttenberg]

@eliasweatherfield Haven't got to this but haven't forgotten about it. Have to clear out some time to think through it properly. It might be easier to have a call to talk some of it through, if you are up for that.