Description |
1 Propositional logic: 1.1 Declarative sentences 1.2 Natural deduction 1.2. 1 Rules for natural deduction 1.2.2 Derived rules 1.2.3 Provable equivalence 1.3 Propositional logic as a formal language 1.4 Semantics of propositional logic 1.4.1 The meaning of logical connectives 1.4.2 Soundness of propositional logic 1.4 .3 Completeness of propositional logic 1.5 Normal forms 1.5.1 Semantic equivalence, satisfiability, and validity 1.5.2 Conjunctive normal forms and validity 1.5.3 Horn clauses and satisfiability 1.6 SAT solvers 2 Predicate logic 2.1 Predicate log ic as a formal language 2.1.1 Terms 2.1.2 Formulas 2.1.3 Free and bound variables 2.1.4 Substitution 2.2 Proof theory of predicate logic 2.2.1 Natural deduction rules 2.2.2 Quantifier equivalences 2.3 Semantics of predicate logic 2.3.1 Models 2.3.2 Semantic entailment 2.3.3 The semantics of equality 2.4 Undecidability of predicate logic 2.5 Expressiveness of predicate logic 3 Program correctness 3.1 Notion of program correctness 3.1.1 Hoare triples 3.1.2 Partial and total correctn ess 3.1.3 Program variables and logical variables 3.2 Proof calculus for partial correctness 3.2.1 Proof rules 3.2.2 Proof tableaux 3.3 Proof calculus for total correctness 3.4 Programming by contract 4 Other Applications such as Logic in databas es, Logic programming, Puzzle solving 5 Practice with Verification tools |