A predicate logic of well-founded actions

Abstract

Recently a new constructive logic of program schemes, have been developed by N.N. Nepejvoda (see [1], [2]). In the logic a programs are treated as state transformers, as actions, which decrease a well-founded resource. So the logic provide easy loop construction and allow to obtain totally correct program schemes. In Nepejvoda calculi Ω actions are ivestigated inside propositional logic framework. In this paper we elaborate a notion of well-founded action and prove useful results allowing investigate actions inside framework of any logic with compactness property. As example, we describe a predicate calculi of well-founded actions PΩ and prove its soundness and completeness.