Check out the new USENIX Web site. next up previous
Next: Database Operations Up: THE SPECIFICATION LANGUAGE Previous: THE SPECIFICATION LANGUAGE

The Core Language

  Following the conventions of Prolog, variables begin in upper case. Constants, functors and predicates begin in lower case. Anonymous variables are denoted by underscores.

Definition 1578

A term is defined inductively as follows:
\begin{smallenum}
\item a variable is a term 
\item a constant is a term
\item i...
 ...For convenience, we use f/n to denote a functor 
 f with arity n.\end{smallenum}

Definition 1579

  A formula is defined inductively as follows:
\begin{smallenum}
\item if p is an n-ary predicate symbol and $T_{1}, T_{2}, ......
 ... 
 p with arity n.
\item if F is a formula, so is ({\bf not} F). \end{smallenum}

Definition 1580

A literal is an atom or the negation of an atom. A positive literal is an atom. A negative literal is the negation of an atom.

Definition 1587

If q is a positive literal, p1, p2, ..., pn are literals, \(n\geq0\), then

q :- p1, p2, ..., pn.

is a rule. Atom q is called the head, and p1, p2, ..., pn combined is called the body of this rule.



Du Li
8/25/1999