Chapters 16, Relations and Quantifiers, and 19, Checking Satisfiability.
Before you start on this week's material, you may find it helpful to review this summary of the logic we have covered thus far.
This video is a brief recap of most of the logic we have covered so far. You may find it useful, to jog your memory and check your understanding.
We have been focusssed on Truth and Logic.
This week we will introduce Language. We have studied predicates, operations on predicates, and algebraic properties of these operations, expressed in the sequent calculus. Introducing language is a major step forward.
The big new idea is that we may consider statements that admit interpretation in any universe,and reason about properties that will be valid for any interpretation of these statements as predicates in some universe.
We start with a couple of videos introducing quantifiers.
In this video we introduce the interpretation of statements such as, "Mary loves Everybody". We use sections in Haskell to help us do this.
In this video we briefly mention more examples of sections, and
then introduce λ-functions, which we use to help us interpretat statements such
as, "Somebody loves Everybody".
This video starts with more examples of sections in Haskell, and
then introduces some new ideas — in particular
λ-functions.
The next videos introduce some ideas of a formal language.
In this video we introduce the idea of a formal language — a language whose expressions can be represented in Haskell.
We begin with a simple example. We introduce a language of clausal forms. We start from a collection of atoms, or propositional letters. In this language we can form literals, which assert or deny a single predicate, clauses, which are disjunctions of literals, and forms, which are conjunctions of clauses.
The following videos continue with the idea of a formal language.
In this video we return to the idea of a formal language — a language whose expressions can be represented in Haskell.
In this video we link the language of forms to our derivations of CNF.
Our next step is to introduce Sudoku as a non-trivial example of a problem we can express in our simple language of forms, solve with logic.
First we see how to express the rules of Sudoku in Haskell. Given
a total function
s :: Int -> Int -> Int -> Bool
that represents the way a sudoku puzzle is filled in by saying that
s i j k == True iff the number k is
written in square
i, j, where i,j,k are numbers in [1..9].
Slides (6,7)
Video
In this video we translate this code for checking a solution
described by a function s :: Int -> Int -> Int -> Bool
into an expression in our language of Forms.
This form uses 729 propositional letters Si,j,k, where i,j,k are numbers in
[1..9].
The idea is that the way the Sudoku puzzle is filled in corresponds
to a valuation of these letters: the value of Si,j,k
is True iff k is
written in square
i,j, and the rules are obeyed iff this valuation
satisfies the Form.
So to solve a sudoku puzzle we need only to find a valuation
that for each of the initial entries given
in the puzzle,
makes the corresponding Si,j,k
True,
and satisfies the Form that expresses the rules.
Sudoku is just a game, but it a good, accessible example of a type of problem that of great practical significance. Here we discuss the Sudoku problem within this wider context.
We are now ready to start developing the DPLL algorithm.
DPLL is an algorithm that searches for a valuation that satisfies some clausal Form (CNF). For example, we will use it to search for a solution for a Sudoku puzzle.
This video introduces the key idea behind the DLPP algorithm. If we decide to make some literal true, we may reduce the problem to a simpler problem. We will build our DPLL algorithm by using this idea.
Use a tiny example to introduce the idea.
We return to the example introduced in the previous video, and begin to represent the problem in Haskell.
Use a tiny example to introduce the idea.
We introduce the idea of using a divide and conquer algorithm.
We continue with the simple example and its representation in Haskell.
There are more videos to come for this week. For the time being, we finish with some Haskell remarks.
In this video we give an example showing how Haskell's types can help us to avoid confusions.
We then discuss the types of the Boolean operations lifted to
predicates, and show how λ-functions can be used to
define these operations.