AUTOMATED REASONING WITH FUNCTION EVALUATION FOR COCOLOG

The Conditional Observer and Controller Logic (COCOLOG) is a logical s ystem for the feedback control of finite input-state-output systems wh erein the individual first order logical theories have the properties of consistency, completeness and decidability. The efficiency of autom atic theorem proving (ATP) is a crucial issue in the implementation of COCOLOG control systems and in this paper we present a so-called func tion evaluation (FE) based resolution-refutation ATP methodology for C OCOLOG. FE-resolution ATP replaces the axioms specifying the dynamics of a finite input-state-output machine by a set of defined function re lations. The resulting procedure extends to predicates and hence permi ts the definition of constant and variable FE-resolution inference. It is shown that FE-resolution ATP is complete in the sense that a set o f clauses which is unsatisfiable in all models with the given interpre tation of the functions will yield the empty clause under resolution, paramodulation and FE-resolution.