Contributions to automated-theorem-proving and formal methods with applications to control systems

Part 1. We show that the standard notions of tautology and subsumption can be naturally generalized, (so that refutation completeness is preserved with respect to the associated deletion), within the context of (a specified set of) modified deduction rules for binary clausal resolution-refutation which build-in the reflexivity, symmetry, transitivity and predicate substitutivity axioms for equality. To this end, first a resolution system, PC<, in which equality has no special status, is introduced and its refutation completeness under subsumption and tautology deletion shown. The generalized notions of subsumption and tautology, Sigma0-subsumption and Sigma 0-tautology, respectively, are then formulated and analyzed. EPC <, a system which provides an adequate deductive context for refutation completeness under deletion with respect to these generalized notions, is then introduced. To prove this completeness, some technical notions (principally, to allow an induction) are introduced, and a number of technical results are obtained. Additionally, some clause "normalization" techniques including generalized forms of replacement factoring and a form of demodulation, are suitably formulated, and the preservation of refutation completeness with the further introduction of these normalization procedures is shown. Some refinements for the rules are offered, as well as a possible further generalization for subsumption, and a generalized form of a special case of replacement resolution, folding.Part 2. We present and analyze some primitives for the analysis and control specification of nondeterministic finite state machines (FSMs), analogous to the Reachability and Current State Estimate Set primitives, introduced as basic predicates, in COCOLOG [8, 9, 7, 38]. In terms of these predicates, an aggregation method for the hierarchical decomposition of a FSM is given, in terms of centered covers of the state space, whereby a hierarchical control may be synthesized and applied. A special class of covers is presented which possesses lattice theoretic properties generalizing the results of [13, 42, 41, 43, 40, 3]. A broader class of (so called) regular covers is introduced which, though lacking closure under any similar lattice operations, is sufficient to guarantee, in an obvious sense, the completeness of the abstraction, (which guarantees meta-level controllability under appropriate circumstances). Other cover classes, suitable for controllable FSMs are then introduced, and the lattice theoretic properties are therein recovered