Reverse-vs-inverse: Difference between revisions
mNo edit summary |
mNo edit summary |
||
| Line 12: | Line 12: | ||
of the iff | of the iff | ||
(forall (p q) | :(forall (p q) | ||
:: (iff (has-participant-at-all-times p q) | |||
::: (forall (t) (participates-in q p t)))) | |||
Then rewrite participates-in to has-participant, swapping the arguments since | Then rewrite participates-in to has-participant, swapping the arguments since | ||
(has-participant p q t) =def (participates-in q p t) | (has-participant p q t) =def (participates-in q p t) | ||
(forall (p q) | :(forall (p q) | ||
:: (iff (has-participant-at-all-times p q) | |||
::: (forall (t) (has-participant p q t)))) | |||
To see the difference between reverse and inverse, we'll | To see the difference between reverse and inverse, we'll create the inverse as we did above | ||
create the inverse as we did above | |||
Initially: | Initially: | ||
(forall (p q) | (forall (p q) | ||
:: (iff (participates-in-at-all-times p q) | |||
:: (and (exists (t) (and (participates-in p q t) (exists-at p t))) | |||
::: (forall (t) (if (exists-at p t) (participates-in p q t))))))) | |||
Swap p and q on the rhs | Swap p and q on the rhs | ||
(forall (p q) | :(forall (p q) | ||
:: (iff (has-participant-at-all-times(inverse) p q) | |||
::: (and (exists (t) (and (participates-in q p t) (exists-at q t))) | |||
:::: (forall (t) (if (exists-at q t) (participates-in q p t))))))) | |||
Now do the participates-in = has-participant swap | Now do the participates-in = has-participant swap | ||
(forall (p q) | :(forall (p q) | ||
:: (iff (has-participant-at-all-times(inverse) p q) | |||
::: (and (exists (t) (and (has-participant p q t) (exists-at q t))) | |||
:::: (forall (t) (if (exists-at q t) (has-participant p q t))))))) | |||
If you compare has-participant-at-all-times to has-participant-at-all-times(inverse) | If you compare has-participant-at-all-times to has-participant-at-all-times(inverse) | ||
where the arrow points, it's p in the former and q in the latter. | where the arrow points, it's p in the former and q in the latter. | ||
We *could* defined the inverses as well but then we would land up with | We *could* have defined the inverses as well, but then we would land up with | ||
two more relations. | two more relations. | ||
1. subject-quantified participates-in-at-all-times | :1. subject-quantified participates-in-at-all-times | ||
2. object-quantified has-participant-at-all-times (inverse of 1) * | :2. object-quantified has-participant-at-all-times (inverse of 1) * | ||
3. subject-quantified has-participant-at-all-times (reverse of 1) | :3. subject-quantified has-participant-at-all-times (reverse of 1) | ||
4. object-quantified participates-in-at-all-times (inverse of 3) * | :4. object-quantified participates-in-at-all-times (inverse of 3) * | ||
It was decided this would be even more confusing. So, in OWL, if you | It was decided this would be even more confusing. So, in OWL, if you | ||
| Line 65: | Line 62: | ||
Note that the same asymmetry existed in the original class-based | Note that the same asymmetry existed in the original class-based | ||
definitions the relations as described in the paper "Relations in | definitions of the relations as described in the paper "[https://genomebiology.biomedcentral.com/articles/10.1186/gb-2005-6-5-r46 Relations in | ||
Biomedical Ontologies" | Biomedical Ontologies]". | ||
Revision as of 14:53, 5 December 2021
The temporal scope of an at-all-times relation is the existence of the subject. If we wanted an inverse, the subject becomes the object and and to match the temporal scope it is the existence of subject=now object that qualifies the relation.
Example:
First imagine that we don't have the temporal qualification, as in
- (forall (p q)
- (iff (participates-in-at-all-times p q)
- (forall (t) (participates-in p q t))))
- (iff (participates-in-at-all-times p q)
We would form the inverse by swapping p and q on the right-hand side of the iff
- (forall (p q)
- (iff (has-participant-at-all-times p q)
- (forall (t) (participates-in q p t))))
- (iff (has-participant-at-all-times p q)
Then rewrite participates-in to has-participant, swapping the arguments since (has-participant p q t) =def (participates-in q p t)
- (forall (p q)
- (iff (has-participant-at-all-times p q)
- (forall (t) (has-participant p q t))))
- (iff (has-participant-at-all-times p q)
To see the difference between reverse and inverse, we'll create the inverse as we did above
Initially:
(forall (p q)
- (iff (participates-in-at-all-times p q)
- (and (exists (t) (and (participates-in p q t) (exists-at p t)))
- (forall (t) (if (exists-at p t) (participates-in p q t)))))))
Swap p and q on the rhs
- (forall (p q)
- (iff (has-participant-at-all-times(inverse) p q)
- (and (exists (t) (and (participates-in q p t) (exists-at q t)))
- (forall (t) (if (exists-at q t) (participates-in q p t)))))))
- (and (exists (t) (and (participates-in q p t) (exists-at q t)))
- (iff (has-participant-at-all-times(inverse) p q)
Now do the participates-in = has-participant swap
- (forall (p q)
- (iff (has-participant-at-all-times(inverse) p q)
- (and (exists (t) (and (has-participant p q t) (exists-at q t)))
- (forall (t) (if (exists-at q t) (has-participant p q t)))))))
- (and (exists (t) (and (has-participant p q t) (exists-at q t)))
- (iff (has-participant-at-all-times(inverse) p q)
If you compare has-participant-at-all-times to has-participant-at-all-times(inverse) where the arrow points, it's p in the former and q in the latter.
We *could* have defined the inverses as well, but then we would land up with two more relations.
- 1. subject-quantified participates-in-at-all-times
- 2. object-quantified has-participant-at-all-times (inverse of 1) *
- 3. subject-quantified has-participant-at-all-times (reverse of 1)
- 4. object-quantified participates-in-at-all-times (inverse of 3) *
It was decided this would be even more confusing. So, in OWL, if you want the inverse of participates-in-at-all-times, which is unnamed, use the expression InverseOf(participates-in-at-all-times).
Note that the same asymmetry existed in the original class-based definitions of the relations as described in the paper "[https://genomebiology.biomedcentral.com/articles/10.1186/gb-2005-6-5-r46 Relations in Biomedical Ontologies]".
