Propositional modal logic of programs
Michael J. Fischer, Richard E. Ladner · 1977
We introduce a fundamental propositional logical system for describing correctness, termination and equivalence of programs. We define a formal syntax and semantics for the propositional modal logic of programs and give several consequences of the definition. Principal conclusions are that deciding satisfiability requires time dn/log nfor some d > 1 and that satisfiability, even in an extended system, can be decided in nondeterministic time cnfor some c. We provide applications of the decision procedure to regular expressions, Ianov schemes, and classical systems of modal logic.