Logic in Computer Science

Mathematical logic is an important basis for mathematics, computer science and artificial intelligence alike. This book provides a comprehensive introduction to various logics, including classical propositional logic and first-order predicate logic, as well as equational logic, temporal logic, and Hoare logic. In addition, it presents proof procedures for classical logics and decision procedures for checking the satisfiability of logical formulas. Preface Contents About the Authors 1 Introduction to Logic 1.1 Logic Is Everywhere 1.1.1 Statement or Proposition 1.1.2 A Brief History of Logic 1.1.3 Thinking or Writing Logically 1.2 Logical Fallacies 1.2.1 Formal Fallacies 1.2.2 Informal Fallacies 1.3 A Glance of Mathematical Logic 1.3.1 Set Theory Basic Concepts and Notations Relations Functions Countable Sets Uncountable Sets 1.3.2 Computability Theory Recursion Backus–Naur Form (BNF) Computable Functions 1.3.3 Model Theory Syntax and Semantics Boolean Algebra 1.3.4 Proof Theory Axioms and Theorems Proof Procedures Inference Rules Exercises References Part I Propositional Logic 2 Propositional Logic 2.1 Syntax 2.1.1 Logical Operators 2.1.2 Formulas 2.2 Semantics 2.2.1 Interpretations 2.2.2 Models, Satisfiability, and Validity 2.2.3 Equivalence 2.2.4 Entailment 2.2.5 Theorem Proving and the SAT Problem 2.3 Normal Forms 2.3.1 Negation Normal Form (NNF) Equivalence Rules for Obtaining NNF 2.3.2 Conjunctive Normal Form (CNF) Equivalence Rules for Obtaining CNF Equivalence Rules for Obtaining Full CNF 2.3.3 Disjunctive Normal Form (DNF) Equivalence Rules for Obtaining DNF Equivalence Rules for Obtaining Full DNF 2.3.4 Full DNF and Full CNF from Truth Table 2.3.5 Binary Decision Diagram (BDD) 2.4 Optimization Problems 2.4.1 Minimum Set of Operators 2.4.2 Logic Minimization Karnaugh Maps for Minimizing DNF and CNF 2.4.3 Maximum Satisfiability 2.5 Using Propositional Logic 2.5.1 Bitwise Operators 2.5.2 Decision Problems in Propositional Logic Exercises References 3 Reasoning in Propositional Logic 3.1 Proof Procedures 3.1.1 Types and Styles of Proof Procedures 3.1.2 Semantic Tableau 3.1.3 α-Rules and β-Rules 3.2 Deductive Systems 3.2.1 Inference Rules and Proofs 3.2.2 Hilbert System 3.2.3 Natural Deduction 3.2.4 Inference Graphs 3.3 Resolution 3.3.1 Resolution Rule 3.3.2 Resolution Strategies 3.3.3 Preserving Satisfiability 3.3.4 Completeness of Resolution 3.3.5 A Resolution-Based Decision Procedure 3.3.6 Simplification Strategies 3.4 Boolean Constraint Propagation (BCP) 3.4.1 BCP: A Simplification Procedure 3.4.2 A Decision Procedure for Horn Clauses 3.4.3 Unit Resolution Versus Input Resolution 3.4.4 Head/Tail Literals for BCP Exercises References 4 Propositional Satisfiability 4.1 The DPLL Algorithm 4.1.1 Recursive Version of DPLL 4.1.2 All-SAT and Incremental SAT Solvers 4.1.3 BCPw: Use of Watch Literals in DPLL 4.1.4 Iterative Implementation of DPLL 4.2 Conflict-Driven Clause Learning (CDCL) 4.2.1 Generating Clauses from Conflicting Clauses 4.2.2 DPLL with CDCL 4.2.3 Unsatisfiable Cores 4.2.4 Random Restart 4.2.5 Branching Heuristics for DPLL 4.3 Use of SAT Solvers 4.3.1 Specify SAT Instances in DIMACS Format 4.3.2 Sudoku Puzzle 4.3.3 Latin Square Problems 4.3.4 Graph Problems 4.4 Maximum Satisfiability 4.4.1 2SAT Versus Max2SAT 4.4.2 Weighted and Hybrid MaxSAT 4.4.3 Local Search Methods 4.4.4 The Branch-and-Bound Algorithm Simplification Rules and Lower Bounds 4.4.5 Use of Hybrid MaxSAT Solvers Exercises References Part II First-Order Logic 5 First-Order Logic 5.1 Syntax of First-Order Languages 5.1.1 Terms and Formulas 5.1.2 Quantifiers 5.1.3 Unsorted and Many-Sorted Logic 5.2 Semantics 5.2.1 Interpretation 5.2.2 Models, Satisfiability, and Validity 5.2.3 Equivalence and Entailment 5.2.4 Set Constructions and Many-Sorted Logic Extensional and Intentional Definitions Many-Sorted Logic and Strong Typing 5.2.5 First-Order Logic Versus Higher-Order Logic Higher-Order Logic ``Privileged'' Status of First-Order Logic Type Theory Versus Higher-Order Logic 5.3 Proof Methods 5.3.1 Semantic Tableau 5.3.2 Natural Deduction 5.4 Conjunctive Normal Form (CNF) 5.4.1 Prenex Normal Form Equivalence Rules for PNF 5.4.2 Skolemization Skolemizing Non-prenex Formulas 5.4.3 Clausal Form Herbrand Models for CNF Exercises References 6 Unification and Resolution 6.1 Unification 6.1.1 Substitutions and Unifiers 6.1.2 Combining Substitutions 6.1.3 Rule-Based Unification 6.1.4 Practically Linear Time Unification Algorithm 6.2 Resolution 6.2.1 Formal Definition 6.2.2 Factoring 6.2.3 A Refutational Proof Procedure 6.3 Simplification Orders and Ordered Resolution 6.3.1 Well-Founded Partial Orders Multiset Extension Lexicographic Extension Precedence 6.3.2 Simplification Orders LPO: Lexicographic Path Order RPO: Recursive Path Order KBO: Knuth–Bendix Order 6.3.3 Completeness of Ordered Resolution 6.4 Prover9: A Resolution Theorem Prover 6.4.1 Input Formulas to Prover9 6.4.2 Inference Rules and Options 6.4.3 Simplification Orders in Prover9 6.4.4 The TPTP Library Exercises References 7 First-Order Logic with Equality 7.1 Equality of Terms 7.1.1 Axioms of Equality 7.1.2 Semantics of ``='' 7.1.3 Theory of Equations 7.2 Rewrite Systems 7.2.1 Rewrite Rules 7.2.2 Termination of Rewriting 7.2.3 Confluence of Rewriting 7.2.4 The Knuth-Bendix Completion Procedure 7.2.5 Special Rewrite Systems Rewrite Systems for Ground Equations String Rewrite Systems Rewriting with Polynomial Equations 7.3 Inductive Theorem Proving 7.3.1 Inductive Theorems 7.3.2 Structural Induction Structural Induction Rule for C={0, s} Equality Crossing 7.3.3 Induction on Two Variables Induction Rule on Two Variables for C={0,s} 7.3.4 Many-Sorted Algebraic Specification Structural Induction Rule for C={nil, cons} 7.3.5 Recursion, Induction, and Self-Reference 7.4 Resolution with Equality 7.4.1 Paramodulation 7.4.2 Simplification Rules 7.4.3 Equality in Prover9 7.5 Finite Model Finding in First-Order Logic 7.5.1 Mace4: A Finite Model Finding Tool 7.5.2 Finite Model Finding by SAT Solvers Exercises References Part III Logic in Programming 8 Prolog: Programming in Logic 8.1 Prolog's Working Principle 8.1.1 Horn Clauses in Prolog 8.1.2 Resolution Proof in Prolog 8.1.3 A Goal-Reduction Procedure 8.2 Prolog's Data Types 8.2.1 Atoms, Numbers, and Variables 8.2.2 Compound Terms and Lists 8.2.3 Popular Predicates over Lists 8.2.4 Sorting Algorithms in Prolog 8.3 Recursion in Prolog 8.3.1 Program Termination 8.3.2 Focused Recursion 8.3.3 Tail Recursion 8.3.4 A Prolog Program for N-Queen Puzzle 8.4 Beyond Clauses and Logic 8.4.1 The Cut Operator ``!'' 8.4.2 Negation as Failure 8.4.3 Beyond Clauses 8.4.4 Variations and Extensions Datalog Constraint Logic Programming Answer Set Programming Exercises References 9 Hoare Logic 9.1 Formal Verification of Computer Systems 9.1.1 Verification of Imperative Programs 9.1.2 Verification of Functional Programs 9.2 Hoare Triples 9.2.1 Hoare Rules Assignment Rule Implication Rule Conditional Rule Iteration Rule Sequence Rule 9.2.2 Examples of Formal Verification 9.2.3 Partial and Total Correctness 9.3 Automated Generation of Assertions 9.3.1 Verification Conditions 9.3.2 Proof of Theorem 9.3.4 Assignments Sequences Conditionals Iterations 9.3.3 Implementing VC in Prolog 9.4 Obtaining Good Loop Invariants 9.4.1 Invariants from Generalizing Postconditions 9.4.2 Program Synthesis from Invariants 9.4.3 Choosing A Good Language for Assertions 9.4.4 Verification Tools for Conventional Languages Exercises References 10 Temporal Logic 10.1 An Approach from Modal Logic 10.1.1 Modal Operators 10.1.2 Kripke Semantics 10.1.3 Restrictions and Limitations 10.2 Linear Temporal Logic 10.2.1 Timeline as Interpretation Sequence 10.2.2 Properties of LTL 10.2.3 Model Checking with Kripke Frames 10.3 Semantic Tableaux for LTL 10.3.1 Rules for Modal Operators 10.3.2 Deciding Satisfiability by Tableaux 10.4 Binary Temporal Operators 10.4.1 The until and release Operators 10.4.2 The weak until and strong release Operators 10.4.3 Extension of Semantic Tableau 10.5 Verification of Concurrent Programs 10.5.1 Model Checking with Finite State Machines 10.5.2 Properties of Concurrent Programs 10.5.3 The bakery(2) Program Exercises References Part IV Logic of Computability 11 Decidable and Undecidable Problems 11.1 A Bit of History 11.1.1 Gödel's Incompleteness Theorems 11.1.2 Three Well-Known Computing Models 11.1.3 Halting Problem 11.2 Turing Machines 11.2.1 Formal Definition of Turing Machines 11.2.2 High-Level Description of Turing Machines 11.2.3 Recognizable Versus Decidable 11.3 Decidability of Problems 11.3.1 Encoding of Decision Problems 11.3.2 Decidable Problems 11.3.3 Undecidable Problems 11.3.4 Reduction 11.3.5 Rice's Theorem 11.4 Computability of Counting Bijections 11.4.1 Properties of Counting Bijections 11.4.2 Equivalence of Recognizable and Recursively Enumerable 11.4.3 Equivalence of Recognizable and Computably Countable 11.4.4 Identifying Unrecognizable Languages 11.5 Turing Completeness 11.5.1 Turing Completeness of Prolog 11.5.2 Turing Completeness of Rewrite Systems Exercises References 12 Decision Procedures 12.1 DPLL(T): Extend DPLL with Theories T 12.1.1 Propositional Abstraction 12.1.2 Examples of DPLL(T) 12.1.3 DPLLT(X): An Algorithm of DPLL(T) 12.2 Equality with Uninterpreted Functions 12.2.1 Uninterpreted Functions 12.2.2 The Congruence Closure Problem 12.2.3 The NOS Algorithm 12.2.4 Ground Congruence by Completion 12.3 Linear Arithmetic 12.3.1 Simplex Method by Example 12.3.2 The Simplex Algorithm 12.3.3 Linear Programming 12.3.4 Integer Programming 12.3.5 Difference Logic 12.4 Making DPLL(T) Practical 12.4.1 Making DPLL(T) Efficient 12.4.2 Combination of Theories Nelson and Oppen's Combination Algorithm 12.4.3 SMT-LIB: A Library of SMT Problems 12.4.4 SMT-COMP: Competition of SMT Solvers Exercises References Index