BFO Release History: From BFO 1 to BFO-ISO

The history of BFO releases thus far (April 2023) is as follows:

2001: release of BFO 1

2007: release of BFO 1.1

changes consist primarily in the addition of the term generically dependent continuant in order to enable coverage of information artifacts, nucleotide sequences, and similar (copyable) entities. For early versions see also here.

2015: release of BFO 2

reflects primarily transition from OWL DL to OWL 2 formalization.

2020: release of BFO-2020

changes are as follows:

(i) changes to the content of BFO: addition of the terms: temporal instant and temporal interval; renaming of zero-, one- and two-dimensional continuant fiat boundary as, respectively, fiat point, line and surface boundary; and addition of two new relations: first instant of and last instant of.

(ii) changes to the treatment of definitions: All non-primitive terms have been provided with English language definitions (which means: statements of individually necessary and jointly sufficient conditions) together with specifications of examples of use. All primitive terms have been provided with elucidations, which means: statements of necessary conditions. All terms have been provided with examples of use. In addition, all relational expressions have been provided with specifications of domain and range constraints.

(iii) changes to the formalization of BFO: Along with an OWL version of BFO-ISO, the ISO standard provides also a CL axiomatization (BFO-ISO-CL) with versions in both CLIF (the Common Logic Interchange Format) and FOL (first-order logic). A proof of consistency of BFO-ISO-CL is provided, together with a proof that BFO-ISO-OWL is derivable thereform. English-language definitions and elucidations provided in the standard are formulated in such a way as to be as close as possible to BFO-ISO-CL while at the same time serving as an access route to the content of BFO-ISO for human users. Both elucidations and definitions are tied as closely as possible to the CLIF/FOL formalization, but there may be no direct mapping from the former to specific axioms in the latter. This is, for example, because the English language text may convey in a single definition what is communicated in the formalization through a combination of multiple axioms.