**Next:**Maximum
Likelihood Parameter Estimation
**Up:**Logic
Control
**Previous:**Macro-COCOLOG
###
Automated Theorem Proving and
Formal Methods in System Theory

*T. Mackling*
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.

*Annual Report*

*Fri Nov 26 23:00:32 GMT 1999*