for COCOLOG with Examples
Suning Wang, Peter E. Caines · 1992
In this paper, we present a function eval- uation based automated (resolution) theorem prov- ing (ATP) methodology, called FE-resolution, for the sets of conditional observer and controller logics re- ferred to by the acronym (COCOLOG) see (CWgO). The unique model property of COCOLOG is pre- sented first and then we give the complete axiomati- zation and decidability properties of COCOLOG the- ories. The completeness of the FE-resolution method is proven and complexity reduction via this technique is discussed. Finally FE-resolution ATP is illustrated via a seven state machine example.