next up previous
Next: Models Up: KL-components Previous: KL-components


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 tex2html_wrap_inline971 *
sorts sort tree
constants (constantsymbol +: sortsymbol) *
functions (functionsymbol +: sortsymb tex2html_wrap_inline977 sortsymbol) *
predicates (predicatesymbol +: sortsymbol *) *
axioms (formula) *

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


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
functionsgif gasDial, voltageDial: tex2html_wrap_inline991 reading
predicates batteryLow, engineDoesntRun, noGas