Formal Ontology    (2AOZ)

A formal ontology is a software artifact that captures intuitions about the world in a formal language. The following definition is adapted from Guarino (1998).    (2AOL)

Definition:    (2AOM)

  An Ontology, Ok, is a set of logical formulae in some language L that aim
  to capture the intended models of a particular conceptualization, C. The
  language L consists of a set of logical symbols (i.e. and, not, exists etc.),
  and a set of non-logical symbols which we refer to as the vocabulary, V which
  consists of at least of variables and relations. A model for an ontology is
  constructed via an interpretation I, assigning to each element of the vocabulary
  V to the extensional structure of the conceptualization, S = {D,R} and thus to
  either elements of the domain D or the conceptual relations R.    (2AON)

Occasionally, the labels "theory" or "set of axioms" may refer equivalently to a formal ontology. Moreover, some languages support the notion of a "module" which is a set of axioms. Similarly, "module" may also refer to an ontology.    (2AOO)

Example:    (2AOY)

A very simple ontology written in the Common Logic Interchange Format might be one for partially ordered sets. It consists of three axioms collected as a single module, named poset.    (2AOX)

  (cl-module (poset)
    (forall (x)
      (leq x x)
     )
    (forall (x y)
      (if
        (and (leq x y) (leq y x))
        (x = y)
      )
    )
    (forall (x y z)
      (if
        (and (leq x y) (leq y z))
        (leq x z)
      )
    )
  )    (2AOQ)

In the example above, the module or ontology or theory for "poset" was written in L = Common Logic. The vocabulary consisted of three variables: x, y, and z and one relation, "leq" (less than or equal to). Moreover, the ontology comprised of three axioms specifying Reflexivity, Anti-Symmetry and Transitivity which constrain which models are admissible for the ontology.    (2AOR)

The following are some valid models which satisfy the poset ontology (set of axioms):    (2AOS)

Model 1:
 Domain D: { Natural Numbers } (i.e. 1, ... , infinity) 
 Relations R: { (1 leq 2), (2 leq 2) }

Model 2:
 Domain D: { 100 }
 Relations: { ( 100 leq 100 }

Model 3:
 Domain D: { -5, 1.1, 200, 18 }
 Relations: { (-5 leq 1.1), (-5 leq 18), (1.1 leq 200), (1.1 leq 1.1), .... }    (2AOT)

Note, the set of models that satisfy our ontology is infinite.    (2AOU)

The following are models that are ruled out:    (2AOV)

Not_Model 1:
 Domain D: {1, 2}
 Relations: { (2 leq 1), (1 leq 1), (1 leq 2)}

Not_Model 2:
 Domain D: { 1, ..., 2000000000} 
 Relations: { (1 leq 1), (1 leq 2), (3 leq 1)}    (2AOW)