We proceed by induction on ?. We sometimes expand the sets R and F as R = {v 1 ,
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 ,
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 ,
By rule ( r ), we know w ,
Observe that [w] is not in the current memory, we ,
We proceed by induction on ?. The boolean cases (?) and (?) are dealt with in the standard way ,
Abstract, The Journal of Symbolic Logic, vol.XLI, issue.03, pp.977-1010, 2001. ,
DOI : 10.1093/jigpal/8.5.653
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
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
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
The benefits of relaxing punctuality, Journal of the ACM, vol.43, issue.1, pp.116-146, 1996. ,
DOI : 10.1145/227595.227602
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
A really temporal logic, Journal of the ACM, pp.164-169, 1989. ,
A really temporal logic, SFCS '89: Proceedings of the 30th Annual Symposium on Foundations of Bibliography Computer Science, pp.164-169, 1989. ,
Towards a general theory of action and time. The language of time: a reader, p.251, 2005. ,
Hybrid logics, Handbook of Modal Logics, pp.821-868, 2006. ,
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
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
The description logic handbook, 2007. ,
DOI : 10.1017/CBO9780511711787
Modal Logic, 2001. ,
The foundations of mathematics: a study in the philosophy of science, 1965. ,
Model-theoretic logics, 1985. ,
DOI : 10.1017/9781316717158
Nominal tense logic and other sorted intensional frameworks, 1990. ,
Representation, reasoning, and relational structures: a hybrid logic manifesto, Logic Journal of IGPL, vol.8, issue.3, pp.339-365, 2000. ,
Basic modal logic, pp.1-88, 1984. ,
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
Hybrid completeness, Logic Journal of IGPL, vol.6, issue.4, pp.625-650, 1998. ,
DOI : 10.1093/jigpal/6.4.625
A henkin completeness theorem for t, Notre Dame journal of formal logic, vol.8, pp.186-190, 1967. ,
Handbook of tableau methods, 1999. ,
Basic model theory, 1996. ,
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
Temporal and modal logic. Handbook of theoretical computer science, 1990. ,
Topological Kripke models, Soviet Mathematics Doklady, pp.147-151, 1974. ,
Reasoning about knowledge, 2003. ,
An incomplete logic containing S4, Theoria, vol.40, issue.1, pp.23-29, 1974. ,
Some connections between elementary and modal logic, Proceedings of the Third Scandinavian Logic Symposium, pp.15-31, 1975. ,
Tableau methods of proof for modal logics, Notre Dame Journal of Formal Logic, vol.13, issue.2, pp.237-247, 1972. ,
Proof methods for modal and intuitionistic logics, 1983. ,
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
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
Assigning meanings to programs, Proceedings of the American Mathematical Society Symposia on Applied Mathematics, pp.19-31, 1967. ,
Bisimulations on Planet Kripke, 1999. ,
5 Model theory of modal logic, Handbook of modal logic, pp.249-329, 2005. ,
DOI : 10.1016/S1570-2464(07)80008-5
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
Dynamic predicate logic, Linguistics and Philosophy, vol.14, pp.39-100, 1991. ,
Two theories of dynamic semantics, Logics in AI ? European Workshop JELIA'90, pp.55-64 ,
The price of universality, Notre Dame Journal of Formal Logic, vol.37, issue.2, pp.174-203, 1996. ,
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. ,
Knowledge and belief, 1962. ,
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
An axiomatic basis for computer programming, Communications of the ACM, vol.12, issue.10, pp.576-583, 1969. ,
Definability and interpolation: Model-theoretic investigations, 2001. ,
Temporal logic, Handbook of Modal Logics, pp.655-720, 2006. ,
Boolean Algebras with Operators. Part I, American Journal of Mathematics, vol.73, issue.4, pp.891-939, 1951. ,
DOI : 10.2307/2372123
Boolean Algebras with Operators, American Journal of Mathematics, vol.74, issue.1, pp.127-162, 1952. ,
DOI : 10.2307/2372074
Theorie der endlichen und unendlichen Graphen, 2002. ,
Tense logic and the theory of linear order, 1968. ,
Specifying real-time properties with metric temporal logic. Real-Time Systems, pp.255-299, 1990. ,
Semantical Analysis of Modal Logic I. Normal Modal Propositional Calculi, Zeitschrift fur mathematische Logik und Grundlagen der Mathematik, 1963. ,
Semantical considerations on modal logic, Acta Philosophica Fennica, vol.16, pp.83-94, 1963. ,
The computational complexity of provability in systems of modal propositional logic, SIAM journal on computing, vol.6, p.467, 1977. ,
A Survey of Symbolic Logic, 1918. ,
An Introduction to Modal Logic: The " Lemmon Notes, 1977. ,
Description logics with concrete domains?a survey, Advances in Modal Logics, 2003. ,
On some completeness theorems in modal logic, Zeitschrift fur mathematische Logik und Grundlagen der Mathematik, pp.379-384, 1966. ,
Tolerance logic, Journal of Logic, Language and Information, vol.10, issue.3, pp.353-374, 2001. ,
On the syntactical construction of systems of modal logic, Journal Symbolic Logic, vol.10, issue.3, pp.83-94, 1945. ,
The Algebra of Topology, The Annals of Mathematics, vol.45, issue.1, pp.141-191, 1944. ,
DOI : 10.2307/1969080
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
Multi-dimensional modal logic, 1997. ,
DOI : 10.1007/978-94-011-5694-3
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
Logics of public communications, Synthese, vol.158, issue.2, pp.165-179, 2007. ,
The temporal logic of programs, 18th Annual Symposium on Foundations of Computer Science, pp.46-57, 1977. ,
Semantical consideration on Floyd-Hoare logic, Foundations of Computer Science 17th Annual Symposium on, pp.109-121, 1976. ,
Models of program logics, 20th Annual Symposium on Foundations of Computer Science, pp.115-122, 1979. ,
Time and modality, 1957. ,
Past, present and future, 1967. ,
Papers on time and tense, 1977. ,
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. ,
Completeness and correspondence in the first and second order semantics for modal logics, Proceedings of the 3rd Scandinavian Logic Symposium, 1973. ,
Modal logics of domains on the real plane, Studia Logica, vol.42, issue.1, pp.63-80, 1983. ,
First-order logic, 1995. ,
Der aussagenkalkul und die topologie [tC05] B. ten Cate. Model theory for extended modal languages, Fundamenta Mathematicae, vol.31, pp.103-134, 1938. ,
Semantic analysis of tense logics, Journal of Symbolic Logic, pp.150-158, 1972. ,
An incompleteness theorem in modal logic, Theoria, vol.40, issue.1, pp.30-34, 1974. ,
Why is modal logic so robustly decidable, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol.31, pp.149-184, 1997. ,
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. ,
Logics of communication and change. Information and Computation, pp.1620-1662, 2006. ,
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. ,
An essay in modal logic, 1951. ,