BFOBasic Formal Ontology

First-Order Logic Based Implementation

As pointed out elsewhere, BFO has been applied successfully as a methodological tool in a wide range of areas. However BFO is still lacking a computational realization that can serve as the computational basis for the formal integration of the various ontologies that are to be included in the OBO-foundry as described elsewhere. The core of BFO (BFO core), a non-extensional temporal mereology with collections, sums, and universals [1] was recently implemented in Isabelle [2] a generic system for the implementation and rapid prototyping of logical formalisms. This computational representation of the BFO core including the definitions and axioms and the proofs of all theorems can be accessed from this webpage. Isabelle is distributed for free under the BSD license and can be downloaded for a wide range of operation systems from the Isabelle website.

The Isabelle-based computational representation of the BFO core will be used as follows:

  • As a basis to extend this core until it incorporates all of BFO (in particular [3-14]) together with theorems that verify the correctness of reasoning rules that are supported by BFO.
  • As a basis of derived domain ontologies that contains more domain-specific notions such as the Gene Ontology [15], the Foundational Model of Anatomy [16], etc.
In both cases the BFO core and its representation within the Isabelle system provide a computational environment that makes it easy to provide such extensions in a coherent, efficient, and logically rigorous way.

Attention: The theory is still under development and undergoes almost daily changes!


  1. Bittner, T., M. Donnelly, and B. Smith, A Spatio-Temporal Top-Level Ontology for Geographic Information Processing, in Technical report, Department of Philosophy, SUNY Buffalo. 2007.
  2. Bittner, T. and M. Donnelly, A formal theory of parthood, connectedness, and qualitative size and distance relations among anatomical entities, In C. Price, editor, Proc. of the 21st Annual Workshop on Qualitative Reasoning (QR07), 2007.
  3. Bittner, T. and M. Donnelly. A theory of granular parthood based on qualitative cardinality and size measures. in Proceedings of the fourth International Conference on Formal Ontology in Information Systems, FOIS06. 2006.
  4. Bittner, T. and M. Donnelly. A temporal mereology for distinguishing between integral objects and portions of stuff. In R. Holte and A. Howe (eds.), Proceedings of the Twenty-Second AAAI Conference on Artificial Intelligence (AAAI-07).
  5. Donnelly, M., Containment relations in anatomical ontologies, in AIMA Annual Symposium Proceedings. 2005. p. 206-210.
  6. Donnelly, M. and T. Bittner. Spatial relations between classes of individuals. in Spatial Information Theory. Cognitive and Computational Foundations of Geographic Information Science. International Conference (COSIT 2005). 2005: Springer Verlag.
  7. Bittner, T., M. Donnelly, and B. Smith, Endurants and Perdurants in Directly Depicting Ontologies. AI Communications, 2004. 14(4): p. 247-258.
  8. Donnelly, M. On Parts and Holes: The Spatial Structure of the Human Body. in Proceedings of the 11th World Congress on Medical Informatics (MedInfo-04). 2004.
  9. Smith, B., et al., Relations in Biomedical Ontologies. Genome Biology, 2005. 6(5): p. r46.
  10. Grenon, P., B. Smith, and L. Goldberg. Biodynamic Ontology: Applying BFO in the Biomedical Domain. in Ontologies in Medicine: Proceedings of the Workshop on Medical Ontologies. 2003: IOS Press, Amsterdam.
  11. Grenon, P. and B. Smith, SNAP and SPAN: Towards Dynamic Spatial Ontology. Spatial Cognition and Computation, 2004. 4(1): p. 69--103.
  12. Smith, B. and P. Grenon, The Cornucopia of Formal-Ontological Relations, in Dialectica 58: 3 (2004), 279–296.
  13. Rosse, C. and J.L.V. Mejino, A Reference Ontology for Bioinformatics: The Foundational Model of Anatomy. Journal of Biomedical Informatics, 2003. 36: p. 478-500.
  14. Rosse, C. and Mejino, J. The Foundational Model of Anatomy Ontology, in Burger, A and Davidson, D and Baldock, R, Eds. Anatomy Ontologies for Bioinformatics: Principles and Practice, pages pp. 59-117. Springer, 2007.
  15. Trentelman, K., Smith, B. An Axiomatisation of Basic Formal Ontology with Projection Functions”, Advances in Ontologies, Proceedings of the Sixth Australasian Ontology Workshop, Adelaide, 7 December 2010, Kerry Taylor, Thomas Meyer and Mehmet Orgun (eds.), 2010, Sydney: ACS, 71-80.

Further relevant papers can be found here.