Using a metatheory as a functional representation

One approach to enabling an expert system to reason in a sophisticated fashion is to provide the system with multiple representations of its knowledge base. A useful type of representation is the functional representation, which describes how objects in the task environment can be used. In this article we construct a metatheory of problem‐solving in rule‐based systems in which object‐level rules, which specify how to interact with the external task environment, are controlled by meta‐level rules. an object‐level rule is viewed as a transformation of the task environment, and an execution trace is a sequence of transformations leading from the initial state to the goal state. Thus, an execution trace is a proof that the goal state is reachable from the initial state via the object‐level rule set, or alternatively, that the initial state is a sufficient precondition to guarantee the truth of the goal condition after executing a specific sequence of rules. This observation permits us to construct a metatheory for solving problems at the meta‐level by examining object‐level proofs. We describe this metatheory, discuss its usefulness as a functional representation of the task domain, and describe some experiments in reasoning within the metatheory.