Significant modifications of the first-order rules have been developed so that they can be applied directly to algebraic expressions. The importance and implication of normalization of formulas in any theorem prover are discussed. It is shown how the properties of the domain of discourse have been taken care of either by the normalizer or by the inference rules proposed. Using a nontrivial example, the following capabilities of the verifier that would use these inference rules are highlighted: (1) closeness of the proof construction process to the human thought process; and (2) efficient handling of user provided axioms. Such capabilities make interfacing with humans easy.>

Because of the undecidability problem of program verification, it becomes necessary for an automated verifier to seek human assistance for proving theorems which fall beyond its capability. In order that the user be able to interact smoothly with the machine, it is desired that the theorems be maintained and processed by the prover in a form as close as possible to the popular algebraic notation. Motivated by the need of such an automated verifier, which works in an environment congenial to human participation and at the same time uses the methodologies of resolution provers of first-order logic, some inference rules have previously been proposed by the authors (ibid., vol.15, no.1, p.1-9, Jan. 1989) for integer arithmetic, and their completeness issues have been discussed. In the present work, the authors examine how these rules can be applied to quantified formulas vis-a-vis verification of programs involving arrays. An interesting situation, referred to as bound-extension, has been found to occur frequently in proving the quantified verification conditions of the paths in a program. A novel rule, called bound-extension rule, has been devised to consolidate and depict the various issues involved in a bound-extension process. It has been proved that the rule set proposed previously by the authors is adequate for handling a more general phenomenon, called bound-modification, which covers bound-extension in all its entirety.>

An implementation of a rule-based theorem prover for verifying iterative programs over integers is presented. The authors emphasize the overall proof construction strategy of the prover which has been able to construct the correctness proofs of all iterative programs taken from the literature. Two performance measures for the prover are proposed, and its proof construction for an array-sorting program is evaluated using these measures.>

In this paper the problems associated with the minimal realization of synchronous sequential machines by unate cellular cascades have been studied. Given the sequential machine in the form of a flow table, a systematic procedure is followed to generate all the selectable sets. Compatible sets consisting of these selectable sets are next determined and the different secondary variables are assigned. The nested functional forms of the next-state expressions for these variables are finally established. The proposed method is very systematic and perfectly suited for machine processing.

The irredundant prime closed sets play an important role in the simplification of an incompletely specified flow table. In this note, an algebraic method for deriving the irredundant prime closed sets corresponding to any given flow table has been presented. It has been shown that the complete set of irredundant prime closed sets is obtained following the procedure suggested.

In this short note, an attempt has been made to arrive at a general algorithm for minimizing the number of internal states in an incompletely specified flow table. The closure property of the compatibility classes which cover a given flow table leads us to the derivation of a particular class of closed sets defined as irredundant prime closed sets. It has been shown that these prime closed sets in sequential circuit synthesis play an analogous role to that of the prime implicants in combinational circuit synthesis. A method has been described for determining all the irredundant prime closed sets and finding the minimal row flow table by suitably choosing one or a collection of those sets.