Gabbay's Separation Theorem
   HOME

TheInfoList



OR:

In
mathematical logic Mathematical logic is the study of logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of for ...
and
computer science Computer science is the study of computation, automation, and information. Computer science spans theoretical disciplines (such as algorithms, theory of computation, information theory, and automation) to Applied science, practical discipli ...
, Gabbay's separation theorem, named after
Dov Gabbay Dov M. Gabbay (; born October 23, 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 authore ...
, 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 Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the science of deductively valid inferences or of logical truths. It is a formal science investigating how conclusions follow from premises ...
"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