On the status of proving program properties in effective interpretations (Q689289)

The paper is based on the previous published results of the author. Considering dynamic theories, the author tries to give a generalisation of Lipton's theorem (R. Lipton: ``A necessary and sufficient condition for the existence of Hoare logics'', Proc. 18th IEEE Symp. FOCS (1977). The idea starts from the fact that every proof system for program correctness yields an enumeration procedure for correctness assertions. The effective interpretations are given by recursive subset of \(\omega\) and recursive functions and relations. The paper presents a sufficient condition for a uniform procedure enumerating dynamic theories of interpretations. If arithmetical notions are first-order-definable by universal or existential formulas within this interpretation, then there exists an appropriate uniform procedure.