Formal Ontology

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).

Definition:

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.

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.

Example:

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.

(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) ) ) )

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.

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

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), .... }

Note, the set of models that satisfy our ontology is infinite.

The following are models that are ruled out:

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)}