Logic Control via Automatic Theorem Proving: COCOLOG Fragments Implemented in Blitzensturm 5.0

The COCOLOG sstem is a partially ordered family of first order logical theories that describe the controlled evolution of the state of a given partially observered finite machine M. Following the review of the general theory of COCOLOG, the notion of Markovian fragments MThk,k ¿ 1, of full COCOLOG theories Thk, is presented. These fragments enjoy the property of having axiom set of fixed size over time. MThk and Thk, have the virtually same state estimation and control power. Next, a newly developed automatic theorem proving software called Blitzenstrum is described and some applications Blitzenstrnm 5.0 to the logic control of a stylized elevator problem are presented.