Dynamic logic with program specifications and its relational proof system
Ewa S. Orłowska · Journal of Applied Non-Classical Logics · 1993
Propositional dynamic logic with converse and test, is enriched with complement, intersection and relational operations of weakest prespecification and weakest postspecification. Relational deduction system for the logic is given based on its interpretation in the relational calculus. Relational interpretation of the operators “repeat” and “loop” is given.