bfo-ontology / bfo-2020 Goto Github PK

The text definition for Relational Quality reads:
"b is a relational quality =Def b is a quality and there exists c and d such that b and c are not identical, & b s-depends on c & b s-depends on d"

I think this should say that the two relata, c and d, are not identical, rather than the b, the relational quality, isn't identical to one of the relata. (If what's intended is that no relational quality relates itself to anything else, then the definition should include that b and d are not identical, as well. However, I don't think that was the idea.)

The at-all-times relations were predicated on the existence of the object instead of the subject.
e.g.

 (iff (has-material-basis-at-all-times p q)
  (and (exists (t) (and (has-material-basis p q t) (exists-at p t)))
   (forall (t) (if (exists-at q t) (has-material-basis p q t))))))

should be

 (iff (has-material-basis-at-all-times p q)
  (and (exists (t) (and (has-material-basis p q t) (exists-at p t)))
   (forall (t) (if (exists-at p t) (has-material-basis p q t))))))

Note the different in the argument to exists-at in the third line.

Is this axiom correct? If it is correct, explain why. If not, remove it.

    (forall (x y t)
     (if
      (exists (w)
       (and (continuant-part-of x w t) (continuant-part-of y w t)))
      (and (if (located-in x y t) (continuant-part-of x y t))
       (if (located-in y x t) (continuant-part-of y x t)))))

Question from Hedi Karray

The definition of concretizes at all times in bfo-2020.ttl states:

"an s-dependent continuant b concretizes a g-dependent continuant c at all times =Def for all times t, b exists at t implies (c is the pattern or content which b shares at t with actual or potential copies)"

From this definition, one would understand the domain to be SDC and the range GDC.

However, the domain in OWL is restricted to SDC or Process.

Hence, the definition needs to be expanded to allow 'b' to be a process and specify the conditions under which a process can concretize a GDC.

The same holds for concretizes at some times .

Werner Ceusters points one out

(cl:comment "quality, realizable-entity are mutually disjoint [ksk-1]"
  (and
   (not
    (exists (x t)
     (and (instance-of x quality t)
      (instance-of x realizable-entity t))))))

It's possible that there are axioms generated by a macro that might include multiple clauses but didn't go to the effort of not having the "and" in the case there was one. It's logically well-defined so it's a cosmetic fix rather than something that affects the logic.

Surfaced on BFO discuss topic: A single point with parts?

(forall (fp t p)
 (if (and (instance-of fp fiat-point t)
     (continuant-part-of p fp t))
    (= p fp)))

Looks like some covering axioms were excluded. Looks like they were marked "universal-covering" and I included "covering". Thanks to Dave Lutz.

It would be very helpful for users to have a picture of the classes in BFO 2020 on one page. If it could be made in a program CMaps and the cmaps file made available (in addition to jpg, pdf etc) that would be very useful. Thanks.

@alanruttenberg Following up on this COB issue.

The domain of the participates in relations are sdc, gdc, or ic but not spatial region. Together with the axioms that there must be a participant and that sdc and gdc participants imply a bearer participates, and bearers are material, one would conclude that it must be a material entity. When I'm next doing that sort of thing, I'll try to show it's provable.

These two CL axioms seem to prove this: SDC, GDC

Are you going to show how to run the theorem prover that uses the CL files?
Should object property chain be created in the OWL version that reflects this?

A comment reading:

if b has_participant c at t then b and c exists at t'

should be

At every time a process exists it has a participant'

Documented as Errata #1

Thanks to Werner Ceusters

Models with sites that have specific dependents aren't inconsistent currently, but the elucidation of disposition says

(Elucidation) b is a disposition means: b is a realizable entity & b's bearer is some material entity & b is such that if it ceases to exist, then its bearer is physically changed, & b's realization occurs when and because this bearer is in some special physical circumstances, & this realization occurs in virtue of the bearer's physical make-up

This would seem to rule out sites and boundaries with functions. A decision has to be made and then then either the elucidation of disposition needs to be modified to remove the material entity clause or axioms have to be added to rule out models where sites or boundaries have specific dependents.

FWIW I've always though that sites and boundaries can have dependents. They are independent continuants, and there are border lengths and surface areas (qualities) and that tapping wood creates a site one function of which is to put the screw into it, loosely speaking.

My parser choked on the following line: (exists (?tb ?tc)

The question marks should be removed.

Given extensional mereology for object aggregates, if organizations are object aggregates, then if two organizations (x and y) have member parts at all times the same set of members, then x=y.

Are there compelling counterexamples here?

These would need to be cases where:

• X and Y are instances of Organization.
• X and Y come to exist at the same time.
• X and Y cease to exist at the same time.
• X and Y share membership.
• X is not identical to Y.

Currently same as qga-1. Should be

A last instant is either part of an extended region or is preceded by it.

For example continuant part of is a ternary relation, thus it might be good to append some explanation what is meant by Domain/Range (e.g. that temporal parameter is neglected when presenting the Domain/Range).

Several relations have a domain or range of “independent continuant that is not a spatial region.“

Meaning “material entity or immaterial entity”?

”spatial region is an independent continuant” is not defined or elucidated.

Either the elucidation for spatial region is incomplete, or the domain and/or range is off for several relations.

bfo-2020-without-some-all-times.owl seems to be (basically) identical bfo-2020.owl without any difference re: the temporally qualified relations.

In all the OWL files, the prefix for namespace http://www.w3.org/2004/02/skos/core# is j.0. Can it be changed to skos?

Should read: If a material entity has a proper part, then at least one of its proper parts is not an immaterial entity

Thanks Werner Ceusters

In CommonCoreOntology/CommonCoreOntologies#112 (comment) I mention that I think that the following make sense. I don't remember if there's already an axiom to that effect or whether it is entailed, so this issue is a reminder to check, and to have a place for possible objections to this if it isn't.

if p1 is a temporal part of p that occupies temporal region t and p2 is a temporal part of p that occupies temporal region that also occupies t, then p1 = p2.

The CL axiomatisation uses the 'distinct' predicate:

Note that CL does not provide any semantics for this predicate, so if the intention was to convey the same constraint as in:

then you need to define the 'distinct' predicate. Otherwise, the intended meaning is not guaranteed. For example, currently, you can add to the CL axiomatisation statements like:
(= continuant material-entity)
and still get a consistent theory.

It should read: Every history is the history of something

Reported by Werner Ceusters.

The axiom "regions-precede-if-they-meet", [suk-1], says, in prover9 syntax:

all i1 all i2 all l1 all f2 ((((-(bfoiof(i1,tinstbcat,i1))) & (-(bfoiof(i2,tinstbcat,i2))) & (lastInstantOf(l1,i1)) & (firstInstantOf(f2,i2)) & ((l1) = (f2)))) -> (precedes(i1,i2)))

But all other axioms about the preceding relation seems to entail that a time region precedes another only if they are disjoint. For example, this axiom:

% if one occurrent precedes another then they do not overlap temporally
all p all q ((((precedes(p,q)) | (precedes(q,p)))) -> (-(exists overlap (((bfotpart(overlap,p)) & (bfotpart(overlap,q))))))) # label("precedes-doesnt-overlap")

makes so that the axiom suk-1 can never hold true (unless the antecedent of the axiom is void).

Therefore, is the axiom suk-1 actually an intended part of the BFO axiomatisation?

1. Some of the definitions are marked as elucidations rather than definitions. Should these use an elucidation property rather than skos definition?
2. It appears the prefix declaration for skos is j.0. Suggest using 'skos' instead.

Need to review - should be easy fix.

I had, at some point, a worry about whether it would be a problem in OWL. Articulate a problem or add it as a relation.

Thanks to Hedi Karray for raising this.

Reported by Stefan Schulz.
It's declared transitive in the FOL, but in an oversight it wasn't on the list of transitive properties for which the OWL transitivity axiom was added.

Two tasks that may aid in generating documentation from the OWL file:

1. Ensure all definition properties are set in sentence case and terminate with a period.
2. Set separate examples as their own value of a property rather than set a list as the object of a skos:example.

There are probably others too...

In bfo-2020-terms.xlsx (BTW, pity not to see it in some non-proprietary format like CSV), on line 5 (exists_at):

While Elucidation speaks about "relation between a particular and ..", the Domain is entity.

This is confusing.

Generation of this artifact worked earlier on, but must have got broken along the line. Replace it with a fixed version.

... what is an Elucidation there looks more like a Definition and vice versa, or alternatively (to keep it better aligned with their A.1.2.5 and A.1.2.6 counterparts) the Elucidation should be rephrased into a Definition and vice versa.

The relations in that column are not the inverse of the relations in the "at all times" column. That's because each are predicated on when the first argument exists - they might more verbosely labeled at-all-times-subject-exists. The inverse of an at-all-times relation would have to be something like at-all-times-object-exists and so predicated on the existence of the same entity.
The proposed fix is to change the column header to "reverse at all times".

Note: If one wants to use the inverse of an at-all-times relation, then one needs to use the object property expression ObjectInverseOf(...-at-all-times).

I don't think so as I think 2 and 1d things belong on the information side. However we probably need to have Barry weigh in on this. If so then maybe we don't have to do anything - have to check, since st regions project and the range is spatial region. If not (one can hope) we should change these to project to 3d spatial regions, Same issue with occurs in.

See https://github.com/BFO-ontology/BFO-2020/tree/master/21838-2/owl

It looks like there's:

• bfo-2020-without-some-all-times.owl
• bfo-without-some-all-times.owl
• bfo-without-some-all-times.ttl.

The first is called out in the ReadMe, but the second two are not. Is this an error?

I'm not sure what to do about this. The example given is a hole in a piece of wood that has a disposition to break 'because' of the hole. The question is what would the basis of a disposition that inheres in an immaterial entity be.

Raised by Werner Ceusters.

Axiom [eom-1] is ill-formed:

To see this try to run this axiom or the whole of occurrent-mereology.cl through http://rest.hets.eu.

I think that the correct form of its content should look like below:

(cl:comment "b temporal part c (both spatiotemporal regions) iff b temporal projection is part of c's temporal projection, and for all parts of b's existence, if it spatially-projects-onto s at that time, then so does c [eom-1]"
    (forall (b c)
     (if
      (and (exists (t) (instance-of b spatiotemporal-region t))
       (exists (t) (instance-of c spatiotemporal-region t)))
      (iff (temporal-part-of b c)
       (and (exists (tb tc)
        (and
            (temporally-projects-onto b tb)
            (temporally-projects-onto c tc)
            (occurrent-part-of tb tc)))
         (forall (tp)
          (if
           (and (occurrent-part-of tp tb)
            (exists (s) (spatially-projects-onto b s tp)))
           (exists (s)
            (and (spatially-projects-onto b s tp)
             (spatially-projects-onto c s tp))))))))))

We have

(forall (p q)
 (if (has-temporal-part p q)
  (if (exists (t) (instance-of p one-dimensional-temporal-region t))
   (exists (t)
    (or (instance-of q one-dimensional-temporal-region t)
     (instance-of q zero-dimensional-temporal-region t))))))

We don't have a similar axiom for temporal-part-of. In my testing this was provable, but depends on there being a covering axiom for temporal region.

However, in most cases there are not covering axioms, even though I define them for purposes of working on the model proving consistency. My build process removes all the covering axioms, but shouldn't remove the one for temporal region. With the covering axiom the other direction is provable.

Thank to Hedi Karray for surfacing this.

Spec says:

b occurs in c =Def. b is a process or a process boundary and c is a material entity or immaterial entity & there exists a spatiotemporal region r and b occupies spatiotemporal region r & for all t, if b exists at t then c exists at t & there exist spatial regions s and s' where b spatially projects onto s at t & c occupies spatial region s' at t & s is a continuant part of s' at t

Can't find an axiom corresponding to this. Verify and then add one if necessary.

Thank to Hedi Karray for surfacing this.

Documented as Errata #2

• In the PDF axiom 6
• In the common logic 4
• Not numbered in the prover9 source

Since this is a logic error, the model will be rechecked once fixed.

Thanks to Werner Ceusters

[201-BFO]
has continuant part at
Definition:
& b is a continuant part of c at t
and c is a continuant part of b at t

This is the case in BFO-2020-text.pdf and bfo-2020-terms.xlsx. I didn’t check anywhere else.

The ISO has a convention that all such relations are suffixed with "at", e.g. 'continuant part of at'
However, in the FOL the terms don't have that suffix. FWIW I think the "at" suffix doesn't read well.

This does not affect the OWL, which has no ternary relationships.

Proposed resolution is to just document this.

As Ludger Jansen convincingly argues in his "Gruppen und Institutionen“, social institutions like corporations can be immaterial independent continuants (pp. 160 f.). In my opinion, we need to allow those entities to participate in processes by themselves.

OBOFoundry/COB#40 (comment)

They are currently both material entity. It should be that member part of should have domain object and range object aggregate.

Thanks to [email protected] for the questions that surfaced this.

To make referring to them in a stable way possible. Currently they are ordered in ascending order in each file, and that order is not necessarily maintained. The stable identifier probably needs a version number so that it's possible to maintain continuity in the event an axiom needs to be corrected.

A copy-paste error, it duplicates the description of axiom 20. It should read: "every temporal region has a first and last instant"

Thanks to @neilotte for reporting this.

Suggests (at least) going through known theorems and check if any are such, and then manually add those to the OWL. See discussion that prompted this realization. In that discussion it is noted that it's reasonable to add a covering axiom for independent continuant.

Note: Known theorems are not included in this distribution.

Should say "A realizable entity exists at least at the beginning of the realization process"
Thanks Werner Ceusters

... saying that Domain/Range is continuant.

Could you share the details of how you checked the consistency of 8792dde?

I tried to use a number of reasoners, including the ones accessible from https://www.tptp.org, but all of them timed out after reasonable time limits.

has participant at some times
"p has participant c at some time =Def for some time t (b is a process, c is a continuant, and c participates in p some way at t"

has participant at all times
"p has participant c at all times =Def for all times t, b exists at t implies (b is a process, c is a continuant, and c participates in p some way at t)"

in both cases "b is a process" should read "p is a process"

in the all-times rel, "b exists at t" should read 'p exists at t"