Transcript BFO: Now with More Logic!

BFO 2.0: Axiomatization,
Modularization, and
Semantic Verification
John Beverley
1
Big Picture for Today
• The Basic Formal Ontology, and Axiomatization in First Order Logic
• Modularization of the Axioms
• Semantic Verification of the Axioms
• Summary and Future Work
2
The Basic Formal Ontology (BFO)
Everything you think you know
about BFO is….
3
The Basic Formal Ontology
Everything you think you know
about BFO is….
Probably about right, but
here’s a refresher.
4
The BFO 2.0 Taxonomy
5
Some Important Distinctions
• Continuant Entities vs. Occurrent Entities
• Dependency vs. Independency
• Types vs. Instances
6
Continuant vs. Occurrent
• Continuants are enduring entities, wholly present whenever they are,
and which lack temporal parts
Continuant
thing, quality …
7
Continuant vs. Occurrent
• Occurrents are perduring entities, not wholly present (usually) at a
single instants, and which have temporal parts
Continuant
Occurrent
thing, quality …
process, event
8
Dependence vs. Independence
Continuant
Independent
Continuant
Dependent
Continuant
thing
quality
Occurrent
process, event
e.g. temperature depends
on a bearer
9
Dependence vs. Independence
Continuant
Independent
Continuant
Dependent
Continuant
thing
quality, …
Occurrent
process, event
e.g. an event depends on
some participant
10
Types vs. Instances
Continuant
Independent
Continuant
Dependent
Continuant
thing
quality
.... .....
Occurrent
process, event
.......
11
Types vs. Instances
types
Continuant
Independent
Continuant
Dependent
Continuant
thing
quality
.... .....
Occurrent
process, event
.......
12
Types vs. Instances
types
Continuant
Independent
Continuant
Dependent
Continuant
thing
quality
.... .....
instances
Occurrent
process, event
.......
13
Dependence vs. Independence Again
Continuant
Occurrent
process
Independent
Continuant
Dependent
Continuant
thing
quality
.... .....
temperature depends
on bearer
.......
14
Instance of Independent Continuant
Continuant
Occurrent
process
Independent
Continuant
Dependent
Continuant
thing
quality
.... .....
John
temperature depends
on bearer
.......
15
Instance of Quality Dependent on…
Occurrent
Continuant
process
Independent
Continuant
Dependent
Continuant
thing
quality
.... .....
John
temperature depends
on bearer
John’s 101 Degree Temperature
.......
16
Instance of Process Dependent on…
Occurrent
Continuant
process
Independent
Continuant
Dependent
Continuant
thing
quality
.... .....
John
temperature depends
on bearer
John’s 101 Degree Temperature
.......
John’s running process
17
Example Binary Relations
• Type-Type Relations
• human is_a mammal
• human heart part_of human
• Instance-Type Relations
• John instance_of the type human
• Sally allergic_to the type codeine
• Instance-Instance Relations
• John’s heart part_of John
• John’s aorta connected_to John’s heart
18
More Basic Formal Ontology Details
• Basic Formal Ontology History
• Developed by Smith/Grenon
• Based, in part, on Theory of Granular Partitions of Smith/Bittner/Donnelly
• Designed as upper level, domain neutral, ontology
• Computationally tractable fundamental ontology
• Upper level ontologies are response to data silo problems
• Also allow easy computational inferencing due to class/subclass structure
19
BFO Versioning
• Developing BFO is a community effort, see here:
https://raw.githubusercontent.com/BFOontology/BFO/master/releases/2.0/bfo.owl
• BFO has undergone significant changes since introduced
• Recent version, 2.0, codified in a reference document, and MIT Press
published “Building Ontologies with the Basic Formal Ontology”
20
BFO Implementations
• A BFO implementation is the realization of a codified BFO technical
specification (e.g. reference manual) as a program or as a software
component
• Implementations:
• OWL – Used in web development/Protégé
• FOL – Commonly used; theorem prover friendly
• CLIF – Common logical language (FOL with abstract semantic language)
21
BFO 2.0 Implementation
• New versions require either new implementations, or updating old
implementations
• Given BFO 2.0 changes, implementations are:
• OWL – Description Logic Base
• FOL – First Order Logic
• CLIF – Common Logic
22
BFO 2.0 Implementation
• New versions require either new implementations, or updating old
implementations
• Given BFO 2.0 changes, implementations are:
• OWL – Description Logic Base (up-to-date!)
• FOL – First Order Logic
• CLIF – Common Logic
23
BFO 2.0 Implementation
• New versions require either new implementations, or updating old
implementations
• Given BFO 2.0 changes, implementations are:
• OWL – Description Logic Base (up-to-date!)
• FOL – First Order Logic (up-to-date!)
• CLIF – Common Logic
24
BFO 2.0 Implementation
• New versions require either new implementations, or updating old
implementations
• Given BFO 2.0 changes, implementations are:
• OWL – Description Logic Base (up-to-date!)
• FOL – First Order Logic (up-to-date!)
• CLIF – Common Logic (given FOL implementation, easily generated)
25
BFO 2.0 Implementation
• New versions require either new implementations, or updating old
implementations
• Given BFO 2.0 changes, implementations are:
• OWL – Description Logic Base (up-to-date!)
• FOL – First Order Logic (up-to-date!)
• CLIF – Common Logic (given FOL implementation, easily generated)
• The work I’ll discuss today concerns the FOL implementation…
26
Axiom Alignment
• The FOL implementation is generated by perusing BFO source
material, and representing philosophical claims in first order logic
• To my knowledge, all claims in the literature concerning BFO have
been axiomatized, i.e. represented as axioms in FOL
• But let’s look at an example of what I mean…
27
Example: Continuant Axiom
• Perusing the reference manual, you’ll find claims like the following:
• “Every continuant is an entity.”
• Which can be represented in FOL as:
28
Theorem Alignment
• Additionally, theorems are often stated (in the source material) to
follow from given philosophical claims, and these must be proven
• To my knowledge, all claimed theorems have been proven…by me
and some relatively new, and very powerful, software:
29
Theorem Alignment
• Additionally, theorems are often stated (in the source material) to
follow from given philosophical claims, and these must be proven
• To my knowledge, all claimed theorems have been proven…by me
and some relatively new, and very powerful, software:
30
Theorem Alignment
• Additionally, theorems are often stated (in the source material) to
follow from given philosophical claims, and these must be proven
• To my knowledge, all claimed theorems have been proven…by me
and some relatively new, and very powerful, software
• Prover9 is useful in automating theorem proofs, and it comes bundled
with Mace4 which is useful for finding models of subsets of axioms
31
Prover9: What?
• FOL axioms can be used to prove theorems about BFO
2.0 within Prover9
• Prover9’s
user
interface
32
Toy Example: Sentential Logic
• Sentential logic input illustrated with MP:
Set Goal(s):
33
Toy Example: Sentential Logic
Sentential logic MP ‘resolution’ proof:
34
Resolution Proof?
• Common automated prover technique.
• Claims ‘clausified’ in conjunctive normal form
• Goal is negated (for reductio ad absurdam)
• Contradictions sought and resolved
35
Toy Example: FOL
• First Order Logic input illustrating DS:
• Set Goal(s):
36
Toy Example: FOL
• Disjunctive Syllogism resolution proof:
37
Time to Put Away the Toys: BFO 2.0
• BFO 2.0 modularized txt files can be uploaded to prover9:
38
Time to Put Away the Toys: BFO 2.0
• Generating axioms (and associated Reference Manual citations +
comments)
39
Time to Put Away the Toys: BFO 2.0
• Look! Here’s our example from earlier, all continuants are entities…
40
BFO 2.0-FOL Theorem: S-DependsOnAt
• But let’s not waste time with nostalgia; let’s get provin’
• ‘Specifically Depends On At’ is a BFO 2.0 relation
• Holds between a,b,t such that b and a share no parts; if b exists c
must exist; and b is neither a boundary nor Site of c
• Similar to “existential dependence”, e.g. pain on organism; gait on
walking, etc.
41
BFO 2.0-FOL Theorem: S-DependsOnAt
• Intuitively, this relation is irreflexive, i.e. it is not the case for any x, x
s-depends-on x
• This is because BFO accepts parthood is reflexive; everything is a
(maximal) part of itself
• Hence, every continuant shares a part with itself; but s-depends-on
requires relata share no parts; we should be able to prove irreflexivity
then for this relation (in the presence of parthood axioms)
42
BFO 2.0-FOL Theorem: S-DependsOnAt
• S-depends-on-at irreflexive proof:
43
BFO 2.0-FOL Theorem: Material Entity
• If an Entity has a continuant part that is a material entity, then the
Entity in question is a Continuant
• Entities are…everything…but not everything is a continuant…(e.g.
there are occurrents)
• Import the source file Material Entity Axioms and Continuant
Axioms…
44
BFO 2.0-FOL Theorem: Material Entity
45
BFO 2.0-FOL Theorem: Material Entity
• Voila, the theorem is proved:
46
Limitations of Theorem Proving
• Proving theorems is useful for uncovering relationships among axioms
and axiom commitments
• But capturing the philosophical underpinning of BFO requires a large
number of axioms; proving theorems here and there just isn’t going
to help us understand BFO very well…
• We need to prove meta-theoretic results about BFO; we accomplish
this by working with the logical structure of BFO directly, i.e. the
relations each class bears to other classes
47
BFO 2.0 Logical Structure
48
Displaying Logical Dependencies
• BFO-FOL axioms have been organized to display logical dependencies
49
Displaying Logical Dependencies
• BFO-FOL axioms have been organized to display logical dependencies
• Example: Object class logically depends on Continuant class
50
Displaying Logical Dependencies
• BFO-FOL axioms have been organized to display logical dependencies
• Example: Object class logically depends on Continuant class
51
The BFO 2.0 Hierarchy
52
The BFO 2.0 Hierarchy
53
Displaying Logical Dependencies
• BFO-FOL axioms have been organized to display logical dependencies
• Example: Object class logically depends on Continuant class
54
Displaying Logical Dependencies
• BFO-FOL axioms have been organized to display logical dependencies
• Example: Object class logically depends on Continuant class
55
The BFO 2.0 Hierarchy
56
The BFO 2.0 Hierarchy
57
Displaying Logical Dependencies
• BFO-FOL axioms have been organized to display logical dependencies
• Example: Object class logically depends on Continuant class
58
Displaying Logical Dependencies
• BFO-FOL axioms have been organized to display logical dependencies
• Example: Object class logically depends on Continuant class
59
The BFO 2.0 Hierarchy
60
The BFO 2.0 Hierarchy
61
Why Logical Dependencies?
• Focusing on logical dependencies helps with:
62
Why Logical Dependencies?
• Focusing on logical dependencies helps with:
• Spotting axioms used by all/most classes/relations in BFO 2.0
63
Why Logical Dependencies?
• Focusing on logical dependencies helps with:
• Spotting axioms used by all/most classes/relations in BFO 2.0
• Spotting redundant axioms
64
Why Logical Dependencies?
• Focusing on logical dependencies helps with:
• Spotting axioms used by all/most classes/relations in BFO 2.0
• Spotting redundant axioms
• Spotting useful modularizations of the BFO 2.0 axioms
65
Why Logical Dependencies?
• Focusing on logical dependencies helps with:
• Spotting axioms used by all/most classes/relations in BFO 2.0
• Spotting redundant axioms
• Spotting useful modularizations of the BFO 2.0 axioms
• What is, and why should I care about, modularization, I hear you cry…
66
Modularization: What?
• Modules are extracted subsets of axioms from BFO-FOL 2.0
• Example: Proper subset of BFO-FOL 2.0 axioms compose the “Taxonomy
Module”, i.e. structural axioms governing all entities (the examples I just
gave!)
67
Taxonomy Module
• Subset of axioms governing taxonomy for BFO; sample axioms:
68
Modularization: What?
• Modules: Extracted subsets of axioms from BFO-FOL 2.0
• Example: Proper subset of BFO-FOL 2.0 axioms compose the “Taxonomy
Module”, i.e. structural axioms governing all entities
69
Modularization: What?
• Modules: Extracted subsets of axioms from BFO-FOL 2.0
• Example: Proper subset of BFO-FOL 2.0 axioms compose the “Taxonomy
Module”, i.e. structural axioms governing all entities
• Example: Proper subset of BFO 2.0 axioms compose the “Temporal Region
Mereology Module”, i.e. axioms governing temporal region mereology (a
parthood relation governing regions of time)
70
Temporal Region Mereology Module
• Subset of axioms applying to temporal regions; sample axioms:
71
Modularization: What?
• Modules: Extracted subsets of axioms from BFO-FOL 2.0
• Example: Proper subset of BFO-FOL 2.0 axioms compose the “Taxonomy
Module”, i.e. structural axioms governing all entities
• Example: Proper subset of BFO 2.0 axioms compose the “Temporal Region
Mereology Module”, i.e. axioms governing temporal region mereology
72
Modularization: What?
• Modules: Extracted subsets of axioms from BFO-FOL 2.0
• Example: Proper subset of BFO-FOL 2.0 axioms compose the “Taxonomy
Module”, i.e. structural axioms governing all entities
• Example: Proper subset of BFO 2.0 axioms compose the “Temporal Region
Mereology Module”, i.e. axioms governing temporal region mereology
• Example: Proper subset of BFO-FOL 2.0 axioms compose the “Exists At
Module”, i.e. axioms governing the Exists At relation (an existence at a time
relation ranging over all entities in BFO)
73
Exists At Module
• Subset of axioms governing the exists at relation; sample axioms:
74
Modularization: How?
• Start with the most general subset of axioms; proceed to next most
general, and so on…
• Generality is a heuristic characterized in terms of logical dependence;
the proper subset of axioms on which all other subsets of axioms are
logically dependent is the most general
• The proper subset(s) of axioms on which no others depend, are the
least general
75
Modularization: How?
• Hypothesis: The BFO Taxonomy Module is the most general, followed
in order of (loosely) decreasing generality:
• Taxonomy Module
• Exists At Module
• Temporal Region Mereology Module…
• As mentioned, modularization is a “divide and conquer” approach to
proving meta-theoretic properties about BFO
76
Modularization: Why?
• Proving meta-theoretic properties concerning the BFO axioms is easier if
we use a ‘divide-and-conquer’ approach when dealing with the axioms;
ultimately we are trying to answer:
• What are BFO’s ontological and relational commitments?
• This is too tough to answer directly, since BFO is so big, but if we divide the
axioms up, we can approach this question in steps…
• Still, a natural follow-up: Why do I want to find such commitments?
77
Modularization: Why?
• Given two theories, if they have different commitments which satisfy them,
then they cannot be computationally integrated
• Because one theory might say “X” is true under one interpretation, while
the second says “~X” is true under the same interpretation; if we attempt
to integrate these theories together in a computing environment, disaster
will result
• We want to be able to predict disaster, so we can avoid it…finding
commitments allows us to make predictions; we find them by a method of
semantic verification, which uses the modules we construct…
78
Semantic Verification: What?
• Logical theories are satisfied or not; if they are, the axioms representing
the theory has a true interpretation, we say the interpretation is a model
• Theories have intended models, or standard interpretations
• E.g. The intended models of Peano Arithmetic include just the natural
numbers as the domain and arithmetic operations as relations
• Semantically verification consists in (1) finding, for a given theory, all the
models which satisfy that theory, and (2) making sure the intended models
of the theory line up with the models that satisfy it
79
Semantic Verification: What?
• But we accomplish this in pieces, by using proper modules of BFO…
• Claim: Intended models of BFO 2.0 are captured with the BFO-FOL 2.0
implementation
• To verify this claim for BFO-FOL 2.0, we must characterize the models
of the axioms (i.e. find the ontological and relational commitments)
• Then check to see if they line up with BFO 2.0 (i.e. the reference
manual, Barry’s intuitions, etc.)
80
Semantic Verification: How?
• This is no easy task…
• It requires tedious sorting through well-understood mathematical
theories to uncover axiom sets that constrain specific models
81
Semantic Verification: How?
• This is no easy task…
• It requires tedious sorting through well-understood mathematical
theories to uncover axiom sets that constrain specific models
• There are…so many well-understood mathematical theories…and
trust me, staring at, and thinking hard about, how axioms relate to
one another is not as productive as you might first think.
82
Semantic Verification: How?
• This is no easy task…
• It requires tedious sorting through well-understood mathematical
theories to uncover axiom sets that constrain specific models
• There are…so many well-understood mathematical theories…and
trust me, staring at, and thinking hard about, how axioms relate to
one another is not as productive as you might first think.
• So, I turned to a recent development in Toronto, an axiom repository
83
COLO(REpository) and Hierarchies
• COLORE is an open repository of ontologies represented as sets of
axioms in Common Logic
• COLORE consists of hierarches, or partially ordered finite set of
theories (modules closed under entailment) in same language:
84
COLO(REpository) and Hierarchies
• COLORE is an open repository of ontologies represented as sets of
axioms in Common Logic
• COLORE consists of hierarches, or partially ordered finite set of
theories (modules closed under entailment) in same language:
• Distinct theories in the same language, may be compared based on
conservative/non-conservative extension properties
85
COLO(REpository) and Hierarchies
• COLORE is an open repository of ontologies represented as sets of
axioms in Common Logic
• COLORE consists of hierarches, or partially ordered finite set of
theories (modules closed under entailment) in same language:
• Distinct theories in the same language, may be compared based on
conservative/non-conservative extension properties
• Distinct theories in distinct languages, may be compared by definable
equivalence for specific theories, and reducibility for sets of theories
86
Definitions
• A Conservative extension to an axiom set, is an extension that
‘doesn’t get you anything new’, but makes stuff easier to prove
• E.g. defining the binary relation ‘is a member of’ in naïve set theory
results in a conservative extension
• A non-conservative extension ‘gets you new stuff’
• E.g. adding a new non-equivalent axiom to an existing axiom set,
trivially gets you something new, and is a non-conservative extension
87
Hierarchy Properties (same Language)
• Ordering Hierarchy houses theories concerning orderings of points.
88
Ordering Hierarchy
89
Hierarchy Properties (same Language)
• Ordering Hierarchy houses theories concerning orderings of points.
90
Hierarchy Properties (same Language)
• Ordering Hierarchy houses theories concerning orderings of points;
includes (among others):
• Theory of Linear Ordering (theory of linear order over points)
91
Ordering Hierarchy
92
Ordering Hierarchy
93
Hierarchy Properties (same Language)
• Ordering Hierarchy houses theories concerning orderings of points;
includes (among others):
• Theory of Linear Ordering (theory of linear order over points)
94
Hierarchy Properties (same Language)
• Ordering Hierarchy houses theories concerning orderings of points;
includes (among others):
• Theory of Linear Ordering (theory of linear order over points)
• Theory of Dense Linear Ordering (theory of dense linear order over
points)
95
Ordering Hierarchy
96
Hierarchy Properties (same Language)
• Ordering Hierarchy houses theories concerning orderings of points;
includes (among others):
• Theory of Linear Ordering (theory of linear order over points)
• Theory of Dense Linear Ordering (theory of dense linear order over
points)
97
Hierarchy Properties (same Language)
• Ordering Hierarchy houses theories concerning orderings of points;
includes (among others):
• Theory of Linear Ordering (theory of linear order over points)
• Theory of Dense Linear Ordering (theory of dense linear order over
points)
• Dense Linear Point is a non-conservative extension of Linear Point
(Linear Point is ‘agnostic’ about density; Dense Linear requires it)
98
Hierarchy Properties (different Languages)
• Relationships can be examined between theories in distinct
hierarchies, via definable equivalence:
• We start with one theory in one language, make a ‘translation
manual’ that allows this theory to speak the language of other
theories, then see how much of what the theories ‘say’ is the same
• Toy example: When I use the word ‘parthood’ how much of what you
mean by ‘parthood’ matches up with what I mean?
99
Semantic Verification: How?
• I’ve used the COLORE repository’s extensive catalogue of wellunderstood mathematical theories (such as Dense Linear Point), to
semantically verify BFO
• Mathematical theories in the repository are linked together based on
language, conservativity, definable equivalence, etc.
• My task: Construct a BFO hierarchy in COLORE, built out of modules,
and determine how each module relates to other theories in COLORE
100
BFO/COLORE Observations
• BFO-FOL modules based on generality, when compared to existing
COLORE theories, motivate the following hypotheses (among others):
101
BFO/COLORE Observations
• BFO-FOL modules based on generality, when compared to existing
COLORE theories, motivate the following hypotheses (among others):
• The BFO Taxonomy constrains the same models as a COLORE “Theory
of Lines”
102
BFO:Taxonomy and COLORE:Theory of Lines
103
BFO/COLORE Observations
• BFO-FOL modules based on generality, when compared to existing
COLORE theories, motivate the following hypotheses (among others):
• The BFO Taxonomy constrains the same models as a COLORE “Theory
of Lines”
104
BFO/COLORE Observations
• BFO-FOL modules based on generality, when compared to existing
COLORE theories, motivate the following hypotheses (among others):
• The BFO Taxonomy constrains the same models as a COLORE “Theory
of Lines”
• The Temporal Region Mereology constrains the same models as the
COLORE “Minimal Extensional Mereology”
105
Minimal Extensional Mereology (MEM)
• Concerns parthood relation, minimal in that the theory only requires:
• Reflexive (every x is part of itself)
• Antisymmetric (if x part of y & y part of x then x=y)
• Transitive (if x part of y & y part of z then x part of z)…
• Applied here, the result is every temporal region is part of itself,
putatively symmetrical parts of temporal regions are identical, and, of
course, transitivity…
106
COLORE: Mereology Hierarchy
107
COLORE: Mereology Hierarchy
108
Minimal Extensional Mereology (MEM)
• Concerns parthood relation, minimal in that the theory only requires:
• Reflexive (every x is part of itself)
• Antisymmetric (if x part of y & y part of x then x=y)
• Transitive (if x part of y & y part of z then x part of z)…
• Applied here, the result is every temporal region is part of itself,
putatively symmetrical parts of temporal regions are identical, and, of
course, transitivity…
109
Minimal Extensional Mereology (MEM)
• Concerns parthood relation, minimal in that the theory only requires:
• Reflexive (every x is part of itself)
• Antisymmetric (if x part of y & y part of x then x=y)
• Transitive (if x part of y & y part of z then x part of z)…
• Applied here, the result is every temporal region is part of itself,
putatively symmetrical parts of temporal regions are identical, and, of
course, transitivity…
• MEM contrasts with stronger mereologies, which may require the
existence of unrestricted composite objects (BFO doesn’t!)
110
COLORE: Mereology Hierarchy
111
COLORE: Mereology Hierarchy
112
BFO/COLORE Observations
• BFO-FOL modules based on generality, when compared to existing
COLORE theories, motivate the following hypotheses (among others):
• The BFO Taxonomy constrains the same models as a COLORE “Theory
of Lines”
• The Temporal Region Mereology constrains the same models as the
COLORE “Minimal Extensional Mereology”
113
BFO/COLORE Observations
• BFO-FOL modules based on generality, when compared to existing COLORE
theories, motivate the following hypotheses (among others):
• The BFO Taxonomy constrains the same models as a COLORE “Theory of
Lines”
• The Temporal Region Mereology constrains the same models as the
COLORE “Minimal Extensional Mereology”
• Exists At constrains the same models of “Lower MEM Weak Mereology”
114
BFO/COLORE Observations
• BFO-FOL modules based on generality, when compared to existing COLORE
theories, motivate the following hypotheses (among others):
• The BFO Taxonomy constrains the same models as a COLORE “Theory of
Lines”
• The Temporal Region Mereology constrains the same models as the
COLORE “Minimal Extensional Mereology”
• Exists At constrains the same models of “Lower MEM Weak Mereology”
115
Taxonomy Models: Setup
• We show the BFO Taxonomy semantically equivalent to the COLORE:
Theory of Lines
• We introduce translation defs between Taxonomy and Lines and vice
versa (sample):
• Entity(x) <-> (x=x)
• Continuant(x) <-> L1…
• Restricts the domain to entities, and translates ‘Continuant’ in BFO
2.0 to ‘Line 1’ in the COLORE Theory of Lines, and so on…
116
Taxonomy Models: Characterized
• Given the appropriate two-way translation definitions, derivation of
target axioms can be conducted:
• In one direction, with the translation definitions from Taxonomy to Lines, we
prove each axiom of the COLORE Theory of Lines
• In the other direction, with the translation definitions that from Lines to
Taxonomy, we prove each axiom of the BFO Taxonomy
• Prover9 semi-automates both tasks, showing definable equivalence
between the theories
117
Temporal Region Models: Setup
• We next show the Temporal Region Mereology (TRM) semantically
equivalent to the COLORE: Minimal Extensional Mereology (MEM)
• We introduce translation defs between TRM and MEM and vice versa
(sample):
• TemporalRegion(x) <-> (x=x)
• TemporalRegionPartOf(x,y) <-> part(x,y)…
• Restricts the domain to Temporal Region, and translates
‘TemporalRegionPartOf’ in BFO 2.0 to ‘part’ in the COLORE mereology
hierarchy
118
Temporal Region Models: Characterized
• Given the appropriate two-way translation definitions, derivation of
target axioms can be conducted:
• In one direction, with the translation definitions from TRM to MEM, we prove
each axiom of COLORE: MEM
• In the other direction, with the translation definitions that from MEM to TRM,
we prove each axiom of the BFO Temporal Region Mereology
• Again, we use Prover9 to show definable equivalence between TRM
and the COLORE theory MEM
119
Exists At Models: Setup
• A more complicated example, we want to show Exists At semantically
equivalent to a formal theory in COLORE…but which?
• Following Gruninger & Chui work on DOLCE’s ‘present’ relation, what
might be called the Lower MEM Weak Mereological Geometry seems
a good place to start (but let me explain…)
• Motivating Intuition: Entity existing at a time can be represented by a
point incident to a line
120
Exists At Models: Setup
• Lower MEM Weak Mereological Geometry is composed of theories
from various hierarchies in COLORE (continued):
• Mereological Geometry combines theories from the ordering, mereology, and
incidence geometry hierarchies
• Incidence relation concerns lines/points and is reflexive and symmetric
• MEM is the underlying mereology (partial order, unique product, etc.)
• ‘Lower’ indicates parthood preserves incidence (e.g. if Entity x Exists At at
Temporal Region t’, and Temporal Region t’’ is part of t’, then x Exists At t’’)
121
Exists At Models: Characterized
• We show Exists At semantically equivalent to Lower MEM Weak
Mereological Geometry (LWMG)
• We introduce translation defs from LWMG to Exists at, and vice versa
(sample):
• Point(x) <-> (Continuant(x) v Occurrent(x))
• Line(x) <-> Temporal Region(x)…
• Definable equivalence shown as before with Prover9 and Mace4
122
Verification So Far…
• The following definable equivalencies have been carried out (BFO
modules on left side; COLORE on right):
•
•
•
•
•
BFO Taxonomy – Theory of Lines
Temporal Region – Minimal Extensional Mereology (MEM)
Exists At – Lower MEM Weak Mereology*
Occurrent Mereology – MEM
Continuant Mereology – Lower MEM Foliation*
*Indicates proposed theory extensions to be introduced to COLORE
123
Future Work
• The remainder of BFO-FOL 2.0 needs to be modularized and verified…in
works are Theory of Time and Theory of Specific Dependence
• BFO theories should also be reduced, if possible, to existing theories in
COLORE
• Modularization and Verification of BFO-FOL 2.0 will allow for direct
comparisons of semantic properties with other ontologies in COLORE (such
as DOLCE and SUMO, which have been partially modularized and verified)
124
Future Work
• COLORE + Hierarchies approach fleshes out the logical space of
axioms, and allows information gleaned from well-known subsets of
axioms to clarify other subsets of axioms
• Hence, Modularization and Verification will also, likely, lead to
clarification of classes of models for various subsets of axioms in
general
• And in particular, full verification will likely lead to a better
understanding of BFO-FOL 2.0’s overall models
125