Putting Declarative Meta Control to Work

We present a logic programming system that accomplishes three important goals: equivalence of declarative and operational semantics, declarative specification of control information, and smoothness of interaction with nonlogic -based programs. The language of the system is that of Generalized Horn Clause Intuitionistic Logic with negation as inconsistency. Meta level predicates are used to specify control information declaratively, compensating for the absence of procedural constructs that usually facilitate formulation of e#- cient programs. Knowledge that has been derived in the course of the current inference process can at any time be passed to non-logic-based program modules. Traditional SLD inference engines maintain only the linear path to the current state in the SLD search tree: formulae that have been proved on this path are implicitly represented in a stack of recursive calls to the inference engine, and formulae that have been proved on previous, unsuccessful paths are lost..