**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*