nextuppreviouscontents
Next:Nonlinear Control Up:Logic Control Previous:Macro-COCOLOG

Automated Theorem Proving and Formal Methods in System Theory

It is shown that the standard notions of tautology and subsumption can be naturally generalized within the context of modified deduction rules for binary clausal resolution-refutation algorithms. Furthermore, this may be carried out in such a way that refutation completeness is preserved. The modified deduction rules build-in the reflexivity, symmetry, transitivity and predicate substitutivity axioms for equality. Primitives for the analysis and control specification of non-deterministic finite state machines analogous to reachability and current state estimation are introduced in COCOLOG. A hierarchical control theory has been developed in this framework which generalizes the results of Caines and Wei in the deterministic setting.

T. Mackling, P. E. Caines
 


Annual Report

Mon Jun 26 21:22:20 GMT 2000