Note that I did restrict a grammar to consist only of a set of
definite clauses defining the predicate
*sign*/1. However, I
will also use definite clauses of
() to define meta-interpreters
for such grammars. For these meta-interpreters I will assume the
operational semantics sketched above. In such cases I treat the
definite clauses defining
*sign* as data; a clause:

is represented as
the clause

i.e. the body of the clause is represented as a list. A
meta-interpreter for
() thus may be defined as in
program 6, which follows the procedural semantics of
(),
i.e. it is a top-down proof procedure with a left-most computation
rule and a depth-first search rule.

For example, a rightmost computation rule can be implemented by
defining the predicate
*refutations* as follows:

1998-09-30