Ontologies

An ontology defines a domain-specific representation language shared by different KL-components. It is formally described through the definition of an order-sorted theory. In addition to its language (non-logical symbols), this theory provides axiomatic definitions of relations, functions and objects that constrain the interpretation and well formed use of its vocabulary [Gruber and Olsen 94].

import *
sorts sort tree
constants (constantsymbol +: sortsymbol) *
functions (functionsymbol +: sortsymb sortsymbol) *
predicates (predicatesymbol +: sortsymbol *) *
axioms (formula) *

Import is a modularizing operator that allows including a theory within another.

Throughout this section we shall illustrate the formal descriptions of KL-components with examples extracted from [van Harmelen and Balder 92]. The following is an example showing the formal description of an ontology.

sorts reading
constants low, zero: reading
functions gasDial, voltageDial: reading
predicates batteryLow, engineDoesntRun, noGas