defRelation

  The defRelation form is used to introduce new relation constants and provide some constraints on their meaning and use in domain theories.

  
Figure: Logical relations are defined with the defRelation form.

 (defRelation R name (x ...x)

		  [ :=> implication asentence ]

		  [ :<=> iff asentence ]

		  [ :function function? ]

		  [ :time-dependent time-dependent? ] )

After the translations required to make time dependence explicit (See section , page ) have been performed, we can define the semantics of defRelation.

The symbol R name is a relation constant naming a relation of arity n; the x are logical variables, one for each argument of R name.

defRelation is a ``global'' definition of the relation; all uses of R name in the domain theory should be consistent with the specified constraints.

:=>

The implication asentence is a logical sentence that mentions the variables x. When R name is a unary relation, then defRelation defines a class; As a consequence, any literal of the form (super x) in the implication asentence means that super is a superclass of R name. If the :=> keyword is present, the following axiom is defined:

:<=>

The iff asentence is a logical sentence that mentions the variables x. If the :<=> keyword is present, the following axiom is defined:

:function

If the boolean function? is true, then R name is a function (the first n-1 arguments to R name uniquely determines the nth). Furthermore, R name(x ...x) may be used as a term denoting x.

:time-dependent

If the boolean time-dependent? is true, then R name is a time-dependent relation. This means that appearance of R name in a CML form must be handled as specified in section , page .