Gabbay's separation theorem

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

  1. ↑ Fisher, Michael David; Gabbay, Dov M.; Vila, Lluis (2005), Handbook of Temporal Reasoning in Artificial Intelligence, Foundations of Artificial Intelligence, 1, Elsevier, p. 150, ISBN 9780080533360.
  2. ↑ Kowalski, Robert A.; Sadri, Fariba (1996), "Towards a Unified Agent Architecture That Combines Rationality with Reactivity", Logic in Databases: International Workshop LID '96, San Miniato, Italy, July 1ÔÇô2, 1996, Proceedings, Lecture Notes in Computer Science, 1154, Springer-Verlag, pp. 137–149, doi:10.1007/BFb0031739, ISBN 3-540-61814-7.


This article is issued from Wikipedia - version of the 10/15/2016. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.