Automated reasoning with function evaluation for COCOLOG with examples

A function evaluation based automated (resolution) theorem proving (ATP) methodology is presented. It is called FE-resolution, for the sets of conditional observer and controller logics referred to by the acronym COCOLOG (conditional observer and controller logics). The unique model property of COCOLOG is presented, and the complete axiomatization and decidability properties of COCOLOG theories are given. The completeness of the FE-resolution method is proven, and complexity reduction via this technique is discussed. FE-resolution ATP is illustrated via a seven state machine example