In
mathematical logic
Mathematical logic is the study of Logic#Formal logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory (also known as computability theory). Research in mathematical logic com ...
and
computer science
Computer science is the study of computation, information, and automation. Computer science spans Theoretical computer science, theoretical disciplines (such as algorithms, theory of computation, and information theory) to Applied science, ...
, Gabbay's separation theorem, named after
Dov Gabbay
Dov M. Gabbay (, ; born October 26, 1945) is an Israeli logician. He is Augustus De Morgan Professor Emeritus of Logic at the Group of Logic, Language and Computation, Department of Computer Science, King's College London.
Work
Gabbay has autho ...
, states that any arbitrary
temporal logic
In logic, temporal logic is any system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of time (for example, "I am ''always'' hungry", "I will ''eventually'' be hungry", or "I will be hungry ''until'' I ...
formula can be rewritten in a
logically equivalent
In logic and mathematics, statements p and q are said to be logically equivalent if they have the same truth value in every model. The logical equivalence of p and q is sometimes expressed as p \equiv q, p :: q, \textsfpq, or p \iff q, depending on ...
"past → future" form. I.e. the future becomes what must be satisfied. This form can be used as execution rules; a
MetateM program is a set of such rules.
[.]
References
Artificial intelligence
Theorems
Temporal logic
{{Comp-sci-stub