Gabbay's separation theorem: Difference between revisions
Jump to navigation
Jump to search
Changing short description from "Any temporal logic formula can be rewritten in an equivalent "past → future" form" to "Theorem in temporal logic" |
m 1 revision imported |
(No difference)
| |
Latest revision as of 05:16, 23 March 2025
In mathematical logic and computer science, Gabbay's separation theorem, named after Dov Gabbay, states that any arbitrary temporal logic formula can be rewritten in a logically equivalent "past → future" form. I.e. the future becomes what must be satisfied.[1] This form can be used as execution rules; a MetateM program is a set of such rules.[2]
References
