Logics for Computer and Data Sciences, and Artificial Intelligence

Foreword
Preface
Contents
List of Figures
List of Tables
1 Propositional Logic
1.1 Introduction
1.2 Syntax and Semantics of Propositional Logic
1.3 Truth Tables
1.4 Normal Forms
1.5 Provability in PL
1.6 Natural Deduction: Decomposition Diagrams
1.7 Analytic Tableaux
1.8 Metatheory of Propositional Logic
1.8.1 Provability from Sets of Formulae
1.8.2 Consistency
1.8.3 Completeness of Propositional Logic
1.9 Resolution
1.10 Entailment
1.11 Horn Clauses. Forward and Backward Chaining
1.12 Satisfiability, Validity and Complexity in Propositional Logic
1.13 Resolution Based SAT Solvers
1.14 Logic Circuits, Threshold Logic
1.15 Problems
References
2 First-Order Logic
2.1 Introduction to Syntax of First-Order Logic (FO)
2.2 Introduction to Semantics of Predicate Logic
2.3 Natural Deduction: Sequents
2.4 Natural Deduction: Diagrams of Formulae
2.5 Natural Deduction: Tableaux
2.6 Metatheory of Predicate Logic
2.6.1 Tableau-Completeness of Predicate Logic
2.6.2 Countable Interpretation Property: The Löwenheim–Skolem Theorem; Compactness Property
2.6.3 Consistency: Existence of Interpretations
2.7 Normal Forms
2.8 Towards Applications: Resolution
2.8.1 Horn Clauses and SLD-Resolution
2.9 Decision Problems in Predicate Logic. Complexity of Satisfiability Problem
2.10 Monadic Predicate Logic Is Decidable
2.11 Herbrand Interpretations and Expansions
2.12 Formal Syntax of First-Order Logic
2.13 Problems
References
3 Propositional Modal Logic
3.1 Syntax of the Modal System K
3.2 Semantics of the Modal System K
3.3 Metatheory of Modal Logics
3.3.1 Canonical Structures and Strong Completeness
3.4 Natural Deduction in Modal Logics: Tableaux
3.4.1 Tableau Provability, Satisfiability, Soundness, Completeness
3.5 Small Structure (Small Model) Property, Decidability
3.6 Satisfiability, Complexity
3.7 Problems
References
4 Epistemic, Default and Dynamic Logics
4.1 Epistemic Logics for a Single Agent
4.2 Epistemic-Doxastic Logics
4.3 Epistemic Logics for n Agents
4.3.1 Completeness of EKn
4.3.2 Logics ETn, ES4n, ES5n, EKD45n
4.3.3 Group Knowledge and Common Knowledge
4.4 Satisfiability, Validity, Decidability of Epistemic Logics
4.5 Non-monotonic Reasoning: Default Logics
4.6 Propositional Dynamic Logic (PDL)
4.7 Basic Laws of PDL. An Axiom System for PDL
4.8 Completeness of PDL
4.9 Filtration. Small Model Property for PDL
4.10 Decidability, Validity, Complexity of PDL
4.11 Examples of Validity Proofs in PDL
4.12 Problems
References
5 Temporal Logics
5.1 Temporal Logic of Prior
5.2 Propositional Linear Temporal Logic (LTL)
5.3 Computational Tree Logic (CTL)
5.4 Full Computational Tree Logic CTL*
5.5 Metatheory of Temporal Logics
5.6 LTL + PAST
5.7 Properties of Systems, Model Checking by Means of Automata
5.8 Natural Deduction: Tableaux
5.8.1 Tableaux for Linear Temporal Logic
5.8.2 Tableaux for Linear Temporal Logic: Construction
5.8.3 Tableaux for Computational Tree Logic CTL
5.9 Problems
References
6 Many-Valued Logics
6.1 The Three-Valued Logic of Łukasiewicz
6.2 Completeness of the Three-Valued Logic 3L
6.3 The N-Valued Logic nL
6.4 Infinite-Valued Logics
6.5 Complexity of Satisfiability Decision Problem for Infinite-Valued Logics
6.6 Problems
References
7 Approximate Reasoning: Rough Logics
7.1 Rough Set Theory: Indiscernibility, Concept Approximations
7.2 The Rauszer Functional Dependence Logic (FD-logic)
7.3 The Vakarelov Information Logic (IL)
7.4 An Interlude: Decision Systems and Rules
7.5 Algorithmic Problems of Data Analysis. Boolean Reasoning
7.6 Algebraic Structures Induced by Rough Sets
7.7 Problems
References
8 Beyond First-Order Logics
8.1 Introduction to Finite Structures and First-Order Definability
8.2 Ehrenfeucht Games
8.3 Second-Order Logic (SO)
8.4 Ehrenfeucht Games for MSO
8.5 Connectivity of Graphs in MSO
8.6 FO and MSO on Strings
8.7 Some Remarks on Decidability and Complexity Issues for Second Order Logics
8.8 Mereological Approximate Logic of Concepts
8.8.1 Classical Mereology
8.9 Approximate (rough) Mereology and Logic of Approximate Containment
8.9.1 Provable Consequences of (M1)–(M3)
8.9.2 Provable Consequences of (M1)–(M3) Involving Rough Inclusions
8.10 Problems
References
Appendix A Set Theory
A.1 Algebra of Sets
A.2 Axiomatic Set Theory
A.3 Cartesian Products
A.4 Relations
A.5 Ordering Relations
A.6 Well-Ordered Sets I
A.7 The Set of Natural Numbers
A.8 Finite Sets
A.9 Functions
A.10 Equipollence
A.11 Countable Sets
A.12 Tolerance Relations
A.13 Equivalence Relations
A.14 Infinite Operations
A.15 Well-Ordered Sets II
A.16 Ordinal Numbers
A.17 The Arithmetic of Ordinal Numbers
A.18 Cardinal Numbers
A.19 Graphs
A.20 Trees
Appendix B Algebraic Structures
B.1 Lattices
B.2 Distributive Lattices
B.3 Relatively Pseudo-complemented Lattices
B.4 Boolean Algebras
Appendix C Computability
C.1 Turing Machines
C.2 Computable Functions
C.3 Recursive Functions
C.4 Primitive Recursive Functions
C.5 Recursive Sets and Predicates
C.6 Arithmetization of Turing Machines
C.7 Computability Versus Recursiveness
C.8 Some Unsolvable Decision Problems
C.9 Recursively Enumerable Sets
C.10 Computability Aspects of First-Order Logic: Arithmetization of Logic FO
Appendix D Complexity
D.1 Introduction
D.2 Classes DTIME, P
D.3 Classes L, NL
D.4 Class NP
D.5 Space Complexity
D.6 Relations Among Complexity Classes
D.7 Classes co-X, EXP, NEXP
D.8 Polynomial Hierarchy
Appendix E MV-Algebras
E.1 Wajsberg Algebras
E.2 MV-Algebras
E.3 Ideals in MV-Algebras
E.4 The Chang Representation Theorem
E.5 Relations Among Wajsberg Algebras, MV-Algebras and the Łukasiewicz Infinite-Valued Propositional Logic
E.6 Completeness Theorem for Infinite-Valued Propositional Logic
Appendix F Transition Systems, Automata, Formal Languages
F.1 Finite Transition Systems
F.2 Finite Automata
F.3 Regular Grammars and Languages
F.4 Regular operations. Regular Expressions
F.5 Regular Expressions
F.6 ω-Expressions. Büchi Automata
F.7 Variants of Büchi Automata: Tree Automata
Index