"If the president of USA is in China for a visit, it will not be possible for him to post a tweet. And if he cannot send a tweet, we can have a quite weekend."

1. How would you describe scenario this using logic formula(s)?
2. What are the logical connectives?
3. Based on deduction, is this statement TRUE or FALSE?
4. Can some statements in logic always evaluate to TRUE?

F: P ∧ Q → P ∨ ¬Q

1. Can F be TRUE? (in other words, is F satisfiable?)
2. Can F be always TRUE? (in other words, is F valid?)
3. How to systematically check satisfiability / validity of a formula? (by hand)
4. Is there a way to organize the formula in advance so that checking can be bit easier?

The 4-Queens Problem consists in placing four queens on a 4 x 4 chessboard so that no two queens can capture each other. That is, no two queens are allowed to be placed on the same row, the same column or the same diagonal.

The following figure illustrates a solution to the 4-Queens Problem: none of the 4 queens can capture each other.

|---+---+---+---|
|   |   | Q |   |
|---+---+---+---|
| Q |   |   |   |
|---+---+---+---|
|   |   |   | Q |
|---+---+---+---|
|   | Q |   |   |
|---+---+---+---|

1. Can you solve this puzzle with another solution?
2. How would you solve this problem using a program?
3. Can we solve this problem using logical representation?
4. What about 100-Queens?

Here is one SAT solver (https://www.comp.nus.edu.sg/~gregory/sat/) from Gregory J. Duck of NUS you can try with your browser (no installation needed). (You are encouraged to learn about the .cnf format using their tutorial.cnf) (If you are interested in SAT solver and would like to try something more efficient, take a look at MiniSAT http://minisat.se)

DPLL (https://en.wikipedia.org/wiki/DPLL_algorithm) stands for Davis-Putnam-Logemann-Loveland.

((X + 1 > 0) ∨ (X + Y > 0)) ∧ ((X < 0) ∨ (x + y > 4)) ∧ (¬ (X + Y > 0))

1. (Try to solve these ineqations by hand)
2. Does it remind you some patterns we just saw?
3. What's missing from the solver in order to crack this problem?

This combination forms another algorithm known as DPLL(T)! A solver combining SAT solving with specific theories is often referred as SMT (Satisfiability Modulo Theory) solver. Most popular systems including Z3, CVC4 … The verification system we will learn in the lecture, Dafny, is powered by Boogie which is in turns solved by SMT solvers.

Also, in addition to the logical connectives, we have introduced many new "symbols" of math. In particular, we've introduced the symbols of integer inequality and addition.

"No one can access some websites (a probation list of websites) during the stay in China"
"Twitter is among the probation list"
"Trump is the president of USA" 
"Trump cannot post a tweet"

1. Try to formulate the scenario above using logical constructs we have seen before
2. Focus on the first statement, do you see the need of additional constructs?

First-order logic extends propositional logic with 1) predicates, 2) functions, and 3) quantifiers. Also, while FO-logic formulas evaluate to TRUE of FALSE just like in propositional logic, FO-logic terms evaluate to domain-specific values. With this foundation, we can now talk about the value inside a term and things like addition (+) / integer inequalities (> = < ) and so on!

And exactly because of these theory-specific reasonings, FO-logic can suitably serves as the logical language for program specifications.

1. What kinds of program properties you can think of?
2. How would you, using FO-logic, write down some properties of a program?
3. Can you write the same properties in different ways?

Parallel to SMT solvers, we also have some FO-logic specific solvers such as Vampire, E3, Princess, these solvers are often called theorem provers. A good overview of theorem proving can be found here (http://www.cs.miami.edu/~tptp/OverviewOfATP.html) As we progress later in the course with Dafny (a verifcation language designed with native support of FO-logic constructs), you will have more experience with verifying your programs using logic. The process of writing down the specification using logic can be tricky, but dont feel frustrated because you are not alone! (We will have a guest lecture addressing these frictions one encounter during program verification :))