[Fwd: Ontologies Containing FOL Axioms]

From: Richard Fikes (fikes@ksl.stanford.edu)
Date: 03/05/02


-------- Original Message --------
Subject: Ontologies Containing FOL Axioms
Date: Fri, 31 Aug 2001 11:35:58 -0700
From: Richard Fikes <fikes@KSL.Stanford.EDU>
Organization: Knowledge Systems Laboratory
To: Joint Committee <joint-committee@daml.org>

During a recent joint committee telecon, I offered in support of the
work on a rules language to provide pointers to ontologies that contain
FOL axioms that would be difficult (or perhaps impossible) to express in
DAML+OIL.  Such examples are not difficult to find.  It occurred to me
that there are some (I think) easy to understand examples in the lecture
slides for my KR course.  So, I am attaching to this message Powerpoint
files containing slides describing three such ontologies.

All comments welcome.

Richard



Units and Measures

The first file describes a portion of a "Units and Measures" ontology
containing classes Physical-Dimension, Physical-Quantity,
Unit-Of-Measure, Magnitude, Length-Unit-Of-Measure, etc.  The notation
used on the slides for class definitions is a simple monotonic frame
language (OKBC) in which slot names are indented and template slots
(i.e., slots that are inherited to instances) are denoted by an "*"
preceding the name.  So, for example, slide 3 says that
Physical-Dimension is a class each of whose instances has exactly one
Standard-Unit that is an instance of Unit-Of-Measure.  (The frame
language is described in the OKBC spec at
http://www.ai.sri.com/~okbc/spec.html, but you shouldn't need to read
any of the spec in order to understand the slides.)

The ontology contains definitions of multiple logical functions that
consist of complex axioms, including Unit* (an associative commutative
mapping of all pairs of units to units), Unit^ (a mapping of reals to
units that has the algebraic properties of exponentiation),
Quantity-Magnitude (i.e., the magnitude of a physical quantity in a
given unit of measure), The-Quantity (i.e., the physical quantity with a
given magnitude in a given unit of measure), and an if-and-only-if
definition for physical quantities being equal.

The functions and classes are used to define objects, such as
Length-Dimension, Meter, Kilometer, and Meter/Second.  The definitions
involve axioms such as:

(= Meter/Second (Unit* Meter (Unit^ Second 1)))

(=> (and (Instance-Of ?q1 Physical-Quantity)
         (Quantity-Dimension ?q1 Length-Dimension))
    (= (Quantity-Magnitude ?q1 Kilometer)
       (/ (Quantity-Magnitude ?q1 Meter) 1000)))

[Where slots (aka properties) are considered to be binary relations.]


Time

The second file describes a time ontology based on the paper at
http://www.ksl.stanford.edu/KSL_Abstracts/KSL-00-01.html.  There are
many complex axioms in that ontology.  For example there are axioms for
computing the value of slot Year-Of, Hour-Of, Minute-Of, etc. of a time
point based on its location on the time line (see slide 7), relations
Before, After, and Equal for time points are defined in terms of
Location-Of and for time points described at different granularities,
constraints are expressed on the start and end time for intervals, the
start and end time of an interval are defined as greatest lower bounds
and least upper bounds on the points in an interval, axioms state that
the time line is dense and that "infinite-past" and "infinite-future"
are time points, etc.


Electronic Circuits

The third file describes a toy ontology that is the first example I
present in the class.  In that ontology, axioms are used to specify the
relationship between the inputs and the output of an AndGate, OrGate,
XorGate, and NotGate.





This archive was generated by hypermail 2.1.4 : 04/02/02 EST