[ToC]

 

Anil Nerode and Wolf Kohn, "Multiple Agent Hybrid Control Architecture," in Robert L. Grossman, Anil Nerode, Anders P. Ravn, Hans Rischel, eds., Hybrid Systems, Springer-Verlag, 1993

CONCEPTUAL STRUCTURE OF THE PROOF AUTOMATON

We now provide an overview of the mechanism by which the inferencer carries out the procedure described above. The inferencer builds a procedure for variable goal instantiation: a locally finite automaton. We refer to this automaton as the Proof Automaton. This important feature is unique to our approach. The proof procedure is customized to the particular theorem statement and knowledge base instance it is currently handling.