Intro -- Contents -- Preface -- About the Authors -- 1. Philosophical Roots of Temporal Logic -- 1.1. The Concept of Time -- 1.1.1. Aristotelean temporal logic -- 1.1.2. Linear and branching temporal logic -- 1.1.3. Temporal logic of modern physics -- 1.2. Toward Formal Systems of Temporal Logic -- 1.2.1. Modo recto and modo obliquo -- 1.2.2. Intuitionism and the relationship of modalities and temporality -- 1.2.3. Becker's modal-logical interpretation of intuitionism -- 1.2.4. Intuitionism and formal systems of temporal logic -- 1.2.5. Outlook on temporal logic in computer science 2. Computational Foundations of Temporal Logic -- 2.1. Basic Modal Logic -- 2.1.1. Syntax of BML -- 2.1.2. Semantics of BML -- 2.1.3. Axiomatic system AxSysBML for BML -- 2.2. Linear-Time Temporal Logic -- 2.2.1. Syntax of LTL -- 2.2.2. Semantics of LTL -- 2.2.3. Decidability problems of LTL -- 2.2.4. Axiomatic system AxSysLTL for LTL -- 2.3. Computation Tree Logic -- 2.3.1. Temporal logic of reachability -- 2.3.2. Computation tree logic -- 2.4. Full Computation Tree Logic -- 2.4.1. Syntax of CTL* -- 2.4.2. Semantics of CTL* -- 2.4.3. Axiomatic system AxSysCTL∗ for CTL∗ -- 2.4.4. Ockhamist CTL* 3. Proof-Theoretical Foundations of Temporal Logic -- 3.1. Gentzen Calculus and Temporal Logic -- 3.1.1. Gentzen's calculus for classical propositional logic in a nutshell -- 3.1.2. What is a (good) sequent-style calculus? -- 3.1.3. Sequent-style calculi for TL -- 3.1.4. Sequent-style calculi for LTL and CTL: A challenge -- 3.2. Tableaux-Based Calculus and Temporal Logic -- 3.2.1. What are tableaux? -- 3.2.2. Basics of tableau construction in basic modal logic -- 3.2.3. Basics of tableau construction in linear temporal logic -- 3.3. Automata-Based Calculus and Temporal Logic 3.3.1. What are Büchi automata? -- 3.3.2. Büchi automata for linear temporal logic -- 3.3.3. Büchi tree automata for branching-time logic CTL -- 3.4. Game-Based Calculus and Temporal Logic -- 3.4.1. Game-based calculus of basis modal logic -- 3.4.2. Game-based calculus and certification of computer programs -- 3.4.3. Game-based solution to the model-checking problem for CTL∗ -- 3.4.4. Game-based solution to the satisfiability problem for CTL∗ -- 3.5. Dialogue-Based Constructive Temporal Logic -- 3.5.1. Dialogue-based introduction of constructive logical operators 3.5.2. Constructive dialogue games -- 3.5.3. Constructive formal dialogue games -- 3.5.4. Constructive dialogue-based logic as Gentzen's intuitionistic calculus G3 -- 3.5.5. Dialogue-based modal logic -- 3.5.6. Dialogue-based temporal logic -- 4. Applications and Outlook of Temporal Logic -- 4.1. Temporal Logic in Artificial Intelligence and Machine Learning -- 4.1.1. Symbolic AI -- 4.1.2. Subsymbolic AI -- 4.1.2.1. Example: Neural networks -- 4.1.3. Statistical and causal learning -- 4.1.3.1. Example: Reinforcement learning -- 4.1.4. Hybrid AI -- 4.1.5. Reinforcement learning with temporal logic -- 4.1.6. Policy search in reinforcement learning | 
