This section describes an operational semantics for *DATR* theories. The
semantics is presented as a set of inference rules that axiomatises the
evaluation relationship for *DATR* expressions. The inference rules
provide a clear picture of the way in which *DATR* works, and should
lead to a better understanding of the mathematical and computational
properties of the language.

The original 1989 publications on *DATR* sought to provide the
language with a formal theory of inference (E&G 1989a) and a
model-theoretic semantics (E&G 1989b). Unfortunately, the
definitions set out in these papers are not general enough to cover
all of the constructs available in the *DATR* language. In
particular, they fail to provide a full and correct treatment of
*DATR*'s notion of global inheritance, or the widely-used evaluable
path construct. A denotational semantics for *DATR* that covers all
of the major constructs is presented in Section 4.
However, it still remains to provide a suitably general, formal
theory of inference for *DATR*, and it is this objective that is
addressed here. More precisely, an operational semantics for *DATR*\
is provided, comprising a formal system of rules that axiomatises the
essential details of how *DATR* expressions are *evaluated*.
Section 3.1.4 has already provided a concise
presentation of the syntax of
the *DATR* language. Section 5.1 compares the formal
theory of inference presented here to that given in 1989.
Section 5.2 introduces the inference rules for a
restricted version of *DATR* that is limited to local inheritance.
Section 5.3 extends the rules to allow global
inheritance. Section 5.4 then revises the theory to bring
in path extensions and defaults, thus covering the full *DATR*\
language. Finally, in Section 5.5, we make some
comments about the theory of inference presented here.

- Inference in
*DATR* - Local inheritance
- Global inheritance
- Path extensions and defaults
- Comments on the theory of inference

Wed Feb 26 12:00:02 GMT 1997