Algorithmic Structural Completeness and a Retrieval System for Proving Theorems in Algorithmic Theories

The book presents the proofs of algorithmic formulas that, as part of the language of algorithmic logic, enable expressing the properties of programs, e.g. correctness, the definitions of semantics of language of programming, and the data structure, e.g. the structures of trees, stacks, etc. Only the proof of formula expressing the correctness of the program in relation to the proper specification can assure the user of error-free application of the program. However, with some advanced tools and programming languages the correctness of programs is not always easy to verify. Therefore, the method of proving called 'abduction' has been used in this study. In consequence, this allowed to obtain the value of function by means of the proof (such technique was first mentioned by Herbrand in his definition of recursive function). The book consists of two parts: 1. research on algorithmic structural completness of algorithmic logic; 2a. description of the retrieval system RS providing comprehensive tools in automated theorem proving theorems of algorithmic theories, i.e. theories based on algorithmic logic, 2b. description of the RETRPROV system which enables proving theorems of algorithmic theories by using the decomposition rules.