penetrates meetsSpatially contradiction

[fcbr]

First, we have this formula about inheritable relations.

(=>
   (and
      (subrelation ?PRED1 ?PRED2)
      (instance ?PRED2 ?CLASS)
      (subclass ?CLASS InheritableRelation))
   (instance ?PRED1 ?CLASS))

Looking at the axioms about penetrates and meetsSpatially, we find:

(subrelation penetrates meetsSpatially)
(instance meetsSpatially SymmetricRelation)

SymmetricRelation is a subclass of InheritableRelation since:

(subclass SymmetricRelation BinaryRelation)
(subclass BinaryRelation InheritableRelation)

and subclass is a TransitiveRelation (since it is a PartialOrderingRelation).

so the conclusion is that:

(instance penetrates SymmetricRelation)

but penetrates is defined explicitly as:

(instance penetrates AsymmetricRelation)

and we have the following regarding AsymmetricRelations:

(<=>
   (instance ?REL AsymmetricRelation)
   (and
       (instance ?REL AntisymmetricRelation)
       (instance ?REL IrreflexiveRelation)))

so, the conclusion is that:

(instance penetrates AntisymmetricRelation)

but we also have that:

(disjoint SymmetricRelation AntisymmetricRelation)

and that:

(=>
   (disjoint ?CLASS1 ?CLASS2)
   (forall (?INST)
     (not
       (and
         (instance ?INST ?CLASS1)
         (instance ?INST ?CLASS2)))))

but, recall that, from above, we have:

(and
   (instance penetrates SymmetricRelation)
   (instance penetrates AntisymmetricRelation))

Thus a contradiction is found.

[arademaker]

This is an old problem, with the command below and searching for 'penetrates', I found that this inconsistency was introduced in Feb 2004 in SUMO!

git blame -- Merge.kif

[apease]

I propose that we delete

(subrelation penetrates meetsSpatially)

and add

(=> (penetrates ?X ?Y) (meetsSpatially ?X ?Y))

[TeamSPoon]

First off, I want to say I completely agree with Adam's changes below.

But would think the following GAF is going to create future similar troubles:

(subclass BinaryRelation InheritableRelation)

[apease]

I agree and I'm surprised that one hasn't shown up in previous contradictions. But we do want the properties of relations to be inheritable, so until it does appear in a contradiction, it should be only a source of suspicion, but not action, I'd say.

[fcbr]

Doing what Adam proposes uncovers a similar problem between member and part. I'll open a new issue for that.

[TeamSPoon]

we do want the properties of relations to be inheritable, so until it does appear in a contradiction, it should be only a source of suspicion, but not action, I'd say

I still agree. I don't think action should be taken about it.

Side note:

Another factor that sometimes I forget when analyzing KIF, CycL or Common Logic. And it may not be applicable in this specific case since I can't discount the importance of
(disjoint SymmetricRelation AntisymmetricRelation) ...

But there can be cases that an inheritance (i am thinking along a domain or range here) eventualy creates a contradiction. But in many cases still legal.. the result is that "at that level" of inheritance (I am assuming two inheritance chains overlap into disjointedness ) there are no longer any valid instances. (The point being, a contradiction only "happens" whenever an instance became existent)

But if we take what I just said as valid we might believe this would be OK

(range mother Female)
(=>  
  (parents ?Child ?Parent)
  (mother ?Child ?Parent))

Which I secretly think might be valid because the range of 'mother' prevents errant fathers sneaking in.

This type of thing appears in Cyc sometimes, just not as obvious as my example above.

What is the opinion in SUMO?

Is there a forum we all pay attention to best answer this question?

[arademaker]

@logicmoo , I am not sure if I understood are you talking about in your notes. Note that your example doesn't make sense for me. If you take the range of mother as Female, than mother is a function, a term constructor. It is not a predicate and you should not use it as you used in the rule. But if you take

(domain mother 1 Female)
(domain mother 2 Person)
(domain parents 1 Person)
(domain parents 1 Person)

(=> (parents ?Child ?Parent)
    (mother ?Child ?Parent))

Any SUMO->TPTP transformation should take care of adding the proper restrictions for the variables, that is

(=> (and (instance ?Child Person)
         (instance ?Child Female)
         (instance ?Parent Person))
    (=> (parents ?Child ?Parent)
        (mother ?Child ?Parent)))

This doesn't add contradiction!

[TeamSPoon]

If you take the range of mother as Female, than mother is a function

Ahah, thank you for clarifying that 'range' is for functions only. The domain/range notation I used was from RDF where the predicates are restricted to the max arity of 2 . And 'domain' is also is restricted to arity 2. So in RDF so 'domain' may only refer to the first argument (heaven help them).. So they (RDFers) use 'range' to mean the arg2's domain :) Sorry for that confusion.

Anyways yes we agree.. Though I meant:

(domain mother 1 Person)
(domain mother 2 Female)
(domain parents 1 Person)
(domain parents 2 Person)

(=> (parents ?Child ?Parent)
    (mother ?Child ?Parent))

thus:

(=> (and (instance ?Child Person)
         (instance ?Parent Female)
         (instance ?Parent Person))
    (=> (parents ?Child ?Parent)
        (mother ?Child ?Parent)))

In which is yes why we agree that this is not a contradiction and thus valid even if it looked controversial.

The note is that despite people feeling compelled to write such a rule this way instead:

(=> (mother ?Child ?Parent)
      (parents ?Child ?Parent))

And definitely not this way:

(<=> (mother ?Child ?Parent)
      (parents ?Child ?Parent))

All these ways are fine due to the domain/3 restrictions keeping them working (no contradiction).

[TeamSPoon]

I'll take this example one step further

(domain mother 1 Person)
(domain mother 2 Female)
(domain father 1 Person)
(domain father 2 Male)

(=> 
    (mother ?Child ?Parent)
    (father ?Child ?Parent))

becomes:

(=> (and (instance ?Child Person)
         (instance ?Parent Female)
         (instance ?Parent Male))
    (=> (mother ?Child ?Parent)
        (father ?Child ?Parent)))

In my opinion the above still is not a contradiction. What I think happens in this case is the rule ends up having "No effect" on the system. So taking this even further lets look at

(domain female 1 Female)
(domain male 1 Male)
(=>
 (female ?Person)
 (male ?Person))

I believe the above to still be non contradictory. Even with the addition of the next two rules:

(<=>
 (female ?Person)
 (instance ?Person Female))

(<=>
 (male ?Person)
 (instance ?Person Male))

I wont claim my examples are good knowledge engineering :) But I want to hear if we agree or not that it should be considered legal.

[apease]

Hi Doug A simple answer is that if it's valid KIF and there's no contradiction then its legal and that's the case with your examples. But also as you point out they're not a consistent style with sumo which doesn't have unary predicates

[arademaker]

Hi Adam, this issue was closed with 7b7ce3a6fbc123a428b457d469c630919482b9d4 ?

[vcvpaiva]

Alexandre, I don't think one should close any issues hastily. The fix above in 7b7ce3a is a bit of a hack, it stops the contradiction, but then it destroys the modelling of "penetrates" too, hence a proverbial case of the baby with the bathwater, if "penetrates" is a useful relation. (I don't know if it is or not)

I don't think I understand the general problem here, yet. and would welcome a clearer, higher level discussion. what's clear to me, from Fabricio's examples so far, is that we have two classes of problems.

1. problems where clear mathematical relations are being understood by modellers differently (meetsSpatially does look a symmetric relation in abstract, while "penetrates" does not look symmetric) (mother does not look symmetric, while "relative" does). Here what's required is to decide which intuition is most useful and then change as little as possible.
2. problems like the holdsDuring one that invokes a serious modelling problem in that case if time is to be considered instants or intervals. I think separating the problems into these two buckets and making sure that we can run a collection of tests on the mathematical relations would be a better bet.

[arademaker]

Just a short note on the @vcvpaiva comment above. We are not destroying penetrates since we added the axiom suggested by @apease to enforce that, in all interpretations I, all tuples part I(penetrates) to be part of I(meetsSpatially). We have only avoided the use of subrelation which propagates the InheritableRelation class.