Algorithmic structural completeness and a retrieval system for proving theorems in algorithmic theories (Q2757280)

The purpose of this book is to present a view on the notions of program substitution and admissibility of rules which are the tools for proving properties of programs in algorithmic logic and in the so-called extended algorithmic logic with quantifiers and with non-deterministic programs.NEWLINENEWLINENEWLINEThe paper presents the proofs of algorithmic formulas. These formulas make it possible to express the properties of programs, the definitions of semantics of programming languages, the data structures, etc.NEWLINENEWLINENEWLINEThe paper consists of two parts. The first one presents algorithmic structural completeness of algorithmic logic strengthened by the substitution rule, i.e. derivability of all structural, finitary and admissible rules, though this logic is not complete, so it is not true that each admissible rule is derivable. The second part is devoted to the construction of proving algorithims. The first of these algorithms, called RS-algorithm, uses Gentzen's method and some idea of decomposition of formulas containing programs. The retrieval system RS provides comprehensive tools in automated proving of theorems in algorithmic theories.