Abstract

The purpose of the present paper is to show that modal propositional logics can be interpreted in a logic based on relational calculus. We consider languages with necessity operators [R], where R is an accessibility relation expression representing an element of the algebra of binary relations with operations −,∪,∩, −1 , ◦. The relational logic is based on relational calculus enriched by operations of weakest prespecification and weakest postspecification introduced in Hoare and He Jifeng and investigated in He Jifeng et al . The logic is an extension of the system introduced in Or lowska and investigated in Buszkowski and Or lowska