. Proof, We proceed by induction on ?. We sometimes expand the sets R and F as R = {v 1

?. .. Ca-w and . ??-ca, then some consequent of the ( k ) rule must occur in ? too j } such that [w] = [u i ], then by (repl), u i , {v 1 , . . . , v k }[w ? u i ], {u 1 , . . . , u j }[w ? u i ] Ca : k ? ?, and by (? F ) the branch would be closed The other case is that there is a v i such that, Therefore, to see M[+[v 1

. Assume-w,-{v-1, ?. Ca-w, ?. Ca, and . ??-ca, Let's analyze the situation of Looking at the consequents of the (¬¬ k ) rule, w¬¬ k cannot be in the branch, since by (? k ) the branch would be closed. So the only possibility is that w ? u i ? ? for some u i ? {u 1 , . . . , u j }. That means , [v k ]}, but that means that there is a v i ? {v 1 , . . . , v k } such that The last possibility is that, By (repl), v i , {v 1 , . . . , v k }[w ? v i ], {u 1 , . . . , u j }[w ? v i ] Ca :¬¬ k ? ? and by (? R ) the branch would be closed +[v k ], ?[u 1 ], . . . , ?[u j ]], [w] |= ¬¬ k

. Case-?:-=-r-?, R. Suppose-w, R. ?. Ca, F. ?. {w}, and . Ca, By rule ( r ), we know w

R. Ca-know-w,-r-?-{w} and F. ?. Ca, Observe that [w] is not in the current memory, we

. Proof, We proceed by induction on ?. The boolean cases (?) and (?) are dealt with in the standard way

P. [. Areces, M. Blackburn, and . Marx, Abstract, The Journal of Symbolic Logic, vol.XLI, issue.03, pp.977-1010, 2001.
DOI : 10.1093/jigpal/8.5.653

C. [. Alur, D. Courcoubetis, and . Dill, Model-checking in dense real-time. Information and Computation, pp.2-34, 1993.
DOI : 10.1006/inco.1993.1024

URL : https://doi.org/10.1006/inco.1993.1024

C. Areces, D. Figueira, S. Figueira, and S. Mera, Expressive Power and Decidability for Memory Logics, 15th Workshop on Logic, Language, Information and Computation, pp.56-68, 2008.
DOI : 10.1007/978-3-540-69937-8_7

URL : https://hal.archives-ouvertes.fr/inria-00323834

D. [. Areces, D. Figueira, S. Gorin, and . Mera, Tableaux and Model Checking for Memory Logics, Automated Reasoning with Analytic Tableaux and Related Methods Proceedings of Tableaux09, pp.47-61, 2009.
DOI : 10.1007/978-3-642-02716-1_5

URL : https://hal.archives-ouvertes.fr/inria-00423049

T. [. Alur, T. Feder, and . Henzinger, The benefits of relaxing punctuality, Journal of the ACM, vol.43, issue.1, pp.116-146, 1996.
DOI : 10.1145/227595.227602

S. [. Areces, S. Figueira, and . Mera, Completeness results for memory logics, LFCS 09: Symposium on Logical Foundations of Computer Science, pp.16-30, 2009.
DOI : 10.1007/978-3-540-92687-0_2

URL : https://hal.archives-ouvertes.fr/inria-00332399

]. R. Ah89a, T. Alur, and . Henzinger, A really temporal logic, Journal of the ACM, pp.164-169, 1989.

]. R. Ah89b, T. A. Alur, and . Henzinger, A really temporal logic, SFCS '89: Proceedings of the 30th Annual Symposium on Foundations of Bibliography Computer Science, pp.164-169, 1989.

]. J. All05 and . Allen, Towards a general theory of action and time. The language of time: a reader, p.251, 2005.

]. C. Atc06, B. Areces, and . Cate, Hybrid logics, Handbook of Modal Logics, pp.821-868, 2006.

G. [. Battigalli and . Bonanno, Recent results on belief, knowledge and the epistemic foundations of game theory, Research in Economics, vol.53, issue.2, pp.149-225, 1999.
DOI : 10.1006/reec.1999.0187

P. [. Bolander and . Blackburn, Termination for Hybrid Tableaus, Journal of Logic and Computation, vol.17, issue.3, pp.517-554, 2007.
DOI : 10.1093/logcom/exm014

URL : http://www.imm.dtu.dk/~tb/BB06_rev.pdf

D. [. Baader, D. L. Calvanese, D. Mcguinnessand, P. F. Nardiand, and . Patel-schneider, The description logic handbook, 2007.
DOI : 10.1017/CBO9780511711787

]. P. Bdrv01, M. Blackburn, Y. De-rijke, and . Venema, Modal Logic, 2001.

]. E. Bet65 and . Beth, The foundations of mathematics: a study in the philosophy of science, 1965.

S. [. Barwise, J. Feferman, and . Baldwin, Model-theoretic logics, 1985.
DOI : 10.1017/9781316717158

]. P. Bla90 and . Blackburn, Nominal tense logic and other sorted intensional frameworks, 1990.

]. P. Bla00 and . Blackburn, Representation, reasoning, and relational structures: a hybrid logic manifesto, Logic Journal of IGPL, vol.8, issue.3, pp.339-365, 2000.

K. [. Bull and . Segerberg, Basic modal logic, pp.1-88, 1984.

J. [. Blackburn and . Seligman, Hybrid languages, Journal of Logic, Language and Information, vol.57, issue.3, pp.251-272, 1995.
DOI : 10.1007/978-94-009-6259-0_4

M. [. Blackburn and . Tzakova, Hybrid completeness, Logic Journal of IGPL, vol.6, issue.4, pp.625-650, 1998.
DOI : 10.1093/jigpal/6.4.625

]. M. Cre67, A henkin completeness theorem for t, Notre Dame journal of formal logic, vol.8, pp.186-190, 1967.

D. [. Agostino, R. Gabbay, J. Hähnle, and . Posegga, Handbook of tableau methods, 1999.

]. K. Doe96 and . Doets, Basic model theory, 1996.

A. [. Demri and . Rabinovich, The Complexity of Temporal Logic with Until and Since over Ordinals, Lecture Notes in Computer Science, vol.4790, pp.531-545, 2007.
DOI : 10.1007/978-3-540-75560-9_38

]. E. Eme90 and . Emerson, Temporal and modal logic. Handbook of theoretical computer science, 1990.

]. L. Esa74 and . Esakia, Topological Kripke models, Soviet Mathematics Doklady, pp.147-151, 1974.

J. [. Fagin, Y. Halpern, M. Moses, and . Vardi, Reasoning about knowledge, 2003.

]. K. Fin74 and . Fine, An incomplete logic containing S4, Theoria, vol.40, issue.1, pp.23-29, 1974.

]. K. Fin75 and . Fine, Some connections between elementary and modal logic, Proceedings of the Third Scandinavian Logic Symposium, pp.15-31, 1975.

]. M. Fit72 and . Fitting, Tableau methods of proof for modal logics, Notre Dame Journal of Formal Logic, vol.13, issue.2, pp.237-247, 1972.

]. M. Fit83 and . Fitting, Proof methods for modal and intuitionistic logics, 1983.

R. [. Fischer and . Ladner, Propositional modal logic of programs, Proceedings of the ninth annual ACM symposium on Theory of computing , STOC '77, pp.286-294, 1977.
DOI : 10.1145/800105.803418

R. [. Fischer and . Ladner, Propositional dynamic logic of regular programs, Journal of Computer and System Sciences, vol.18, issue.2, pp.194-211, 1979.
DOI : 10.1016/0022-0000(79)90046-1

]. R. Flo67 and . Floyd, Assigning meanings to programs, Proceedings of the American Mathematical Society Symposia on Applied Mathematics, pp.19-31, 1967.

]. J. Ger99 and . Gerbrandy, Bisimulations on Planet Kripke, 1999.

M. [. Goranko and . Otto, 5 Model theory of modal logic, Handbook of modal logic, pp.249-329, 2005.
DOI : 10.1016/S1570-2464(07)80008-5

A. [. Gabbay, S. Pnueli, J. Shelah, and . Stavi, On the temporal analysis of fairness, Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '80, pp.163-173, 1980.
DOI : 10.1145/567446.567462

]. J. Gs91a, M. Groenendijk, and . Stokhof, Dynamic predicate logic, Linguistics and Philosophy, vol.14, pp.39-100, 1991.

]. J. Gs91b, M. Groenendijk, and . Stokhof, Two theories of dynamic semantics, Logics in AI ? European Workshop JELIA'90, pp.55-64

]. E. Hem96 and . Hemaspaandra, The price of universality, Notre Dame Journal of Formal Logic, vol.37, issue.2, pp.174-203, 1996.

]. T. Hen90 and . Henzinger, Half-order modal logic: How to prove real-time properties, Proceedings of the Ninth Annual Symposium on Principles of Distributed Computing, pp.281-296, 1990.

]. J. Hin62 and . Hintikka, Knowledge and belief, 1962.

O. [. Harel, A. Lichtenstein, and . Pnueli, Explicit clock temporal logic, [1990] Proceedings. Fifth Annual IEEE Symposium on Logic in Computer Science, pp.402-413, 1990.
DOI : 10.1109/LICS.1990.113765

]. C. Hoa69 and . Hoare, An axiomatic basis for computer programming, Communications of the ACM, vol.12, issue.10, pp.576-583, 1969.

]. E. Hoo01 and . Hoogland, Definability and interpolation: Model-theoretic investigations, 2001.

M. [. Hodkinson and . Reynolds, Temporal logic, Handbook of Modal Logics, pp.655-720, 2006.

A. [. Jónsson and . Tarski, Boolean Algebras with Operators. Part I, American Journal of Mathematics, vol.73, issue.4, pp.891-939, 1951.
DOI : 10.2307/2372123

A. [. Jónsson and . Tarski, Boolean Algebras with Operators, American Journal of Mathematics, vol.74, issue.1, pp.127-162, 1952.
DOI : 10.2307/2372074

. [. König, Theorie der endlichen und unendlichen Graphen, 2002.

]. J. Kam68 and . Kamp, Tense logic and the theory of linear order, 1968.

]. R. Koy90 and . Koymans, Specifying real-time properties with metric temporal logic. Real-Time Systems, pp.255-299, 1990.

]. S. Kri63a and . Kripke, Semantical Analysis of Modal Logic I. Normal Modal Propositional Calculi, Zeitschrift fur mathematische Logik und Grundlagen der Mathematik, 1963.

]. S. Kri63b and . Kripke, Semantical considerations on modal logic, Acta Philosophica Fennica, vol.16, pp.83-94, 1963.

]. R. Lad77 and . Ladner, The computational complexity of provability in systems of modal propositional logic, SIAM journal on computing, vol.6, p.467, 1977.

]. C. Lew18 and . Lewis, A Survey of Symbolic Logic, 1918.

D. [. Lemmon and . Scott, An Introduction to Modal Logic: The " Lemmon Notes, 1977.

]. C. Lut03 and . Lutz, Description logics with concrete domains?a survey, Advances in Modal Logics, 2003.

]. D. Mak66 and . Makinson, On some completeness theorems in modal logic, Zeitschrift fur mathematische Logik und Grundlagen der Mathematik, pp.379-384, 1966.

]. M. Mar01 and . Marx, Tolerance logic, Journal of Logic, Language and Information, vol.10, issue.3, pp.353-374, 2001.

]. J. Mck45 and . Mckinsey, On the syntactical construction of systems of modal logic, Journal Symbolic Logic, vol.10, issue.3, pp.83-94, 1945.

A. [. Mckinsey and . Tarski, The Algebra of Topology, The Annals of Mathematics, vol.45, issue.1, pp.141-191, 1944.
DOI : 10.2307/1969080

A. [. Mckinsey and . Tarski, Some theorems about the sentential calculi of Lewis and Heyting, The Journal of Symbolic Logic, vol.4, issue.01, pp.1-15, 1948.
DOI : 10.1090/S0002-9904-1934-05881-6

Y. [. Marx and . Venema, Multi-dimensional modal logic, 1997.
DOI : 10.1007/978-94-011-5694-3

J. [. Ouaknine and . Worrell, On the Decidability of Metric Temporal Logic, 20th Annual IEEE Symposium on Logic in Computer Science (LICS' 05), pp.188-197, 2005.
DOI : 10.1109/LICS.2005.33

]. J. Pla07 and . Plaza, Logics of public communications, Synthese, vol.158, issue.2, pp.165-179, 2007.

]. A. Pnu77 and . Pnueli, The temporal logic of programs, 18th Annual Symposium on Foundations of Computer Science, pp.46-57, 1977.

]. V. Pra76 and . Pratt, Semantical consideration on Floyd-Hoare logic, Foundations of Computer Science 17th Annual Symposium on, pp.109-121, 1976.

]. V. Pra79 and . Pratt, Models of program logics, 20th Annual Symposium on Foundations of Computer Science, pp.115-122, 1979.

]. A. Pri57 and . Prior, Time and modality, 1957.

]. A. Pri67 and . Prior, Past, present and future, 1967.

]. A. Pri77 and . Prior, Papers on time and tense, 1977.

]. M. Rey03 and . Reynolds, The complexity of the temporal logic with " until " over general linear time, Journal of Computer and System Sciences, vol.66, issue.2, pp.393-426, 2003.

]. H. Sah73 and . Sahlqvist, Completeness and correspondence in the first and second order semantics for modal logics, Proceedings of the 3rd Scandinavian Logic Symposium, 1973.

]. V. She83 and . Shehtman, Modal logics of domains on the real plane, Studia Logica, vol.42, issue.1, pp.63-80, 1983.

]. R. Smu95 and . Smullyan, First-order logic, 1995.

]. A. Tar38 and . Tarski, Der aussagenkalkul und die topologie [tC05] B. ten Cate. Model theory for extended modal languages, Fundamenta Mathematicae, vol.31, pp.103-134, 1938.

]. S. Tho72 and . Thomason, Semantic analysis of tense logics, Journal of Symbolic Logic, pp.150-158, 1972.

]. S. Tho74 and . Thomason, An incompleteness theorem in modal logic, Theoria, vol.40, issue.1, pp.30-34, 1974.

]. M. Var97 and . Vardi, Why is modal logic so robustly decidable, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol.31, pp.149-184, 1997.

]. J. Van-benthemvb91, ]. J. Van-benthem, and J. Van-benthem, Modal logic and classical logic The logic of time [vB01] J. van Benthem. Logics for information update An essay on sabotage and obstruction One is a lonely number: on the logic of communication, Modal correspondence theory. Handbook of Philosophical Logic TARK'01: Proceedings of the 8th Conference on Theoretical Aspects of Rationality and Knowledge. [vB05] J. van Benthem Mechanizing Mathematical Reasoning Logic Colloquium, pp.167-247, 1984.

]. J. Van-benthem, J. Van-eijck, and B. Kooi, Logics of communication and change. Information and Computation, pp.1620-1662, 2006.

]. H. Van-ditmarsch, W. Van-der-hoek, and B. Kooi, Dynamic Epistemic Logic Kluwer academic publishers [vEB97] P. van Emde Boas. The convenience of tilings, Complexity, Logic and Recursion Theory, vol.187, pp.331-363, 1997.

]. G. Wright, An essay in modal logic, 1951.