Chapter 18, Expression Trees.
Chapter 20, Efficient CNF Conversion.
Chapter 23, Counting Satisfying Valuations.
This video introduces the idea that expressions are things we can study.
We look first at evaluating algebraic expressions by substituting values for variables, and then do the same for Boolean Algebra.
There are two videos covering the Tseytin procedure.
The first approaches the procedure purely algebraically.
in the second video, we show how the Tesytin procedure can be
implemented elegantly in Haskell.
Slides (2..7)
Video (7:13)
This video looks at the ordering of predicates. We first met
this as the satisfaction ordering a ⊨ b.
We look at the ordering of the 16 possible boolean functions of two variables. We can also view it as a diagram of the subsets of a situation with four individuals, each representative of one of the four possible combinations of two boolean properties A and B. Each boolean function corresponds to a property P, and the diagram shows { x | P(x) }.
Each arrow (directed edge) in the diagram represents the addition of an additional element to the set. Each arrow represents a valid implication.
In this video we focus on binary constraints: clauses with two literals. A 2-SAT problem is a conjunction of binary constraints. We will represent it as a partial ordering on literals.
In this video we look at the simplest example, a single clause, and see how we can use the ordering to count the satisfying valuations.
In this video we look at the next simplest example, chains of implications between atoms. We introduce the arrow rule.
In this video we look at more complicated patterns of implications, and introduce a method for counting the satisfying valuations.
In this video we look at yet another pattern of implications, and apply our a method for counting the satisfying valuations.
In this video we look at another example, then consider graphs with a cycle of implications. If we have cycles of implications, then all nodes in the cycle must take the same truth value.
These slides summarize the logic content of the course, as delivered in 2019. We will publish similar slides for this year before the final test.