procedure execute(prog :tree);
   type mode = (PrintAll, Silent);    {search mode}
   var index :integer; { used for renaming }

#include "unify.P"     { unify two predicates }
#include "rename.P"    { rename variables in a rule }
#include "prove.P"     { proof strategy }

begin {execute}
   index := 0;
   if not Prove(PrintAll, prog^.query, prog^.facts, nil) then
      writeln(' no')
end  {execute};

{\fB Interpreter. \fP}