DATA-STORAGE INTERPRETATION OF LABELED MODAL LOGIC

We introduce reference structures - a basic mathematical model of a da ta organization capable of storing and utilizing information about its addresses. A propositional labeled modal language is used as a specif ication and programming language for reference structures; the satisfi ability algorithm for modal language gives a method of building and op timizing reference structures satisfying a given formula, Correspondin g labeled modal logics are presented, supplied with cut free axiomatiz ations, completeness and decidability theorems are proved. Initializat ion of typed variables in some programming languages is presented as a n example of a reference structure building.