Preprints of IIS SB RAS, 1998

The methodology of applying formula rewriting systems to automated program verification is suggested. The possibility of automated verification of a number of programs of text editing, array sorting and file sorting is demonstrated. The verification system SPECTRUM module combining simplification procedures based on formula rewriting systems with other decision and simplification procedures is described.

Formula rewriting system theory is represented. The unified approach to correctness definition of such systems is suggested. A relation between formula rewriting systems and type theories is considered. A survey of classes of terminating formula rewriting systems is given.

This paper presents a model of program properties. This model does not depend on programming languages and application areas. Also properties visualizer HyperCode is described in the paper. This tool is implemented for integration into different programming and software reengineering systems.

We present a semiautomatic theorem prover based on the notion of strategy. Main emphasis is made on description of the strategy definition language which is the key point in design of the system. Declarative and informal operational semantics of the language are described. Substantial number of examples illustrating features of the language is devoted to combining heterogeneous deductive procedures into a single proof-search strategy.

General methods for problem solving are objects of study in artificial intelligence. This work describes subdefinite models as a framework for solving constraint satisfaction problems. Such problems arise in many fields of science and engineering. The use of the method of constraint propagation in subdefinite models makes it possible to estimate the set of all solutions of such a problem. Foundations of subdefinite models are given in the paper. The notion of subdefinite extension of a many-sorted model is proposed, and the types of such extensions are discussed. Both denotational and operational semantics of constraint propagation in subdefined models are defined and their equivalence is proved.