Twierdzenie Gabbay'a o separacji

W logice matematycznej i informatyce twierdzenie Gabbay'a o separacji , nazwane na cześć Dova Gabbay'a , stwierdza , że ​​​​każdą dowolną formułę logiki czasowej można przepisać w logicznie równoważnej formie „przeszłość → przyszłość”. To znaczy przyszłość staje się tym, co musi być spełnione. Ten formularz może być używany jako reguły wykonania; program MetateM jest zbiorem takich reguł.