Abstract

Algorithmic and dynamic logics are powerful tools for programming analysis. Their investigation is one of the most actual trends of the modern mathematical logic. But each such logic is in some sense like a centaurus: its language consists of two parts and these two parts are of a very different nature. A logic of a completely new class is introduced and studied here: a constructive logic of program schemata Ω1. There is not in its language any explicite mention of programs, nevertheless its semantics is defined through realizability by program schemata. It is known that constructive logics also are powerful tools for the mentioned purposes. Furthermore, proof search strategies for constructive logics give us program synthesis algorithms and programming methodics. The main pecularities of our system by which many definitions are motivated are as follows; ruling out a possibility of infinite executions ab finitio and indeterminism