Overview

Here we give an abstract view of the term data-structure  . Details follow in Section .

Let variables  be some infinite class of atomic individuals. The class of terms as the least set of expressions such that:

• if v is a variable, then v is a term,

• if for we have that are variables, is a term, and we define

  

  then

  

  is a term.

We name the parts of a term as follows:

• is the operator  .

  The parts of the operator are:

  • opid is the operator identifier.
  • is the jth parameter  . is its value, and is its type.

• The tuple where is the arity  of the term.

• is the ith bound-term of the term. This bound-term binds free occurrences of the variables in .

When writing terms, we sometimes omit the brackets around the parameter list if it is empty.