A program logic with quantifiable propositional variables
A program logic with quantifiable propositional variables
In the paper an extension of propositional program logics is given, obtained by introducing quantifiers binding propositional variables. The complete axiomatization of the logic is provided. The problems are discussed of definability of sets of states of programs and distinguishability of states by means of the formulas of the logic. Some specific axioms are introduced which characterize a class of models such that for every model of the class there is a model in which all the states are distinguishable by formulas, and both models satisfy the same formulas.
definability of sets of states of programs, Specification and verification (program logics, model checking, etc.), extension of propositional program logics, propositional quantifiers, distinguishability of states, Other nonclassical logic, completeness, normalized models, compactness, Modal logic (including the logic of norms), extension of propositional dynamic logic, quantifiers binding propositional variables, Abstract data types; algebraic specification, complete axiomatization
definability of sets of states of programs, Specification and verification (program logics, model checking, etc.), extension of propositional program logics, propositional quantifiers, distinguishability of states, Other nonclassical logic, completeness, normalized models, compactness, Modal logic (including the logic of norms), extension of propositional dynamic logic, quantifiers binding propositional variables, Abstract data types; algebraic specification, complete axiomatization