Declarative multiplexed rational controllers

The author discusses an architecture for the design and implementation of a class of feedback knowledge-based autonomous control systems in which the central operational element, the inferencer, is all online mechanical theorem prover whose function is to determine whether an existentially qualified theorem, representing the desired system behavior, logically follows from the theory stored in the knowledge base, and if so to generate command actions. The knowledge base is a set of declarations given by equational Horn clauses organized in a nested hierarchy. The knowledge base is dynamically modified by sensory and goal data. The main elements of the architecture are discussed, and some its operational characteristics, adaptability, stability, and goal reachability are considered. The architecture is illustrated by all autonomous guidance controller for a transport aircraft in the vicinity of an airport. >