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 Model
s
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 |