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.