nextuppreviouscontents
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