HW 4 -- Prop Logic

The questions below are due on Wednesday October 11, 2023; 11:59:00 PM.
 

This week's Colab notebook can be found here: Colab Notebook (Click Me!)

1) Propositional Logic§

1.1) Model checking§

Let’s explore proof by model checking. We are interested in finding out which other sentences are entailed by the sentence (A \Rightarrow B) \Rightarrow C. We can do this by comparing the sets of models (assignments of truth values to propositions) in which the sentences are true.

Consider a domain with three propositional variables, A, B, and C.

1. Recall that M(\gamma) is the set of models in which sentence \gamma is true. We can conclude that sentence \alpha entails sentence \beta via model-checking if
   Choose the correct one:

   	M(\alpha) \subseteq M(\beta)
   	M(\beta) \subseteq M(\alpha)
   	M(\alpha) \subset M(\beta)
   	M(\beta) \subset M(\alpha)
   	M(\beta) \equiv M(\alpha)
   	|M(\beta)| > |M(\alpha)|

   
2. Check all models in which (A \Rightarrow B) \Rightarrow C is true.

   	A=t, B=t, C=t
   	A=t, B=t, C=f
   	A=t, B=f, C=t
   	A=t, B=f, C=f
   	A=f, B=t, C=t
   	A=f, B=t, C=f
   	A=f, B=f, C=t
   	A=f, B=f, C=f

   
3. Check all models in which A \Rightarrow (B \Rightarrow C) is true.

   	A=t, B=t, C=t
   	A=t, B=t, C=f
   	A=t, B=f, C=t
   	A=t, B=f, C=f
   	A=f, B=t, C=t
   	A=f, B=t, C=f
   	A=f, B=f, C=t
   	A=f, B=f, C=f

   
4. Check all that are true.

   	(A \Rightarrow B) \Rightarrow C and A \Rightarrow (B \Rightarrow C) are equivalent
   	(A \Rightarrow B) \Rightarrow C entails A \Rightarrow (B \Rightarrow C)
   	A \Rightarrow (B \Rightarrow C) entails (A \Rightarrow B) \Rightarrow C

   

1.2) Concepts in logic§

Consider a domain with propositions A, B, C, and D, and the particular model m = \{A = t, B = f, C = t, D = f\}. For each of these sentences, indicate whether it is valid, unsatisifiable, not valid but true in m, or not unsatisifiable but false in m.

1. A \Rightarrow \neg A -- valid unsatisfiable not valid, but true in m not unsatisfiable, but false in m

   
2. \neg (A \wedge B) \Rightarrow (\neg A \vee \neg B) -- valid unsatisfiable not valid, but true in m not unsatisfiable, but false in m

   
3. B \Rightarrow C \wedge D -- valid unsatisfiable not valid, but true in m not unsatisfiable, but false in m

   
4. A \Rightarrow C \wedge D -- valid unsatisfiable not valid, but true in m not unsatisfiable, but false in m

   
5. (A \wedge C) \Leftrightarrow (B \wedge D) -- valid unsatisfiable not valid, but true in m not unsatisfiable, but false in m

   
6. A \vee B \vee C \vee D -- valid unsatisfiable not valid, but true in m not unsatisfiable, but false in m

   
7. D \Leftrightarrow \neg D -- valid unsatisfiable not valid, but true in m not unsatisfiable, but false in m

   

2) Propositional Logic Semantics Review§

2.1) Propositional Sentence Evaluation§

Note: for these questions, refer to the top of the Colab notebook. Write a function that takes a propositional sentence and evaluates it against a single model. You may find python's builtin isinstance useful. For example, isinstance(sentence, And) returns whether a sentence is an And.

For reference, our solution is 15 line(s) of code.

3) Propositional Logic Coding Problems§

3.1) Warmup§

In this problem, CNF formulas are represented as lists of lists of nonzero integers. The sign of the integer represents whether the corresponding proposition is negated or not. For example, the formula ((x1 or not x2) and (x3 or x2)) would be represented as [[1, -2], [3, 2]]. Complete the following function to confirm your understanding of this representation.

For reference, our solution is 2 line(s) of code.

3.2) DPLL§

Use your helper functions to complete an implementation of DPLL.

For reference, our solution is 59 line(s) of code.

4) Logic for State Estimation§

Consider a "search and rescue" robot who will be charged with navigating a sometimes dangerous grid to find and help people in need. Assume a partially observable domain, consider the subproblem of inferring what locations in a grid contain smoke or fire based on a limited set of observations and our knowledge about the relationship between smoke and fire.

4.1) Warming up with sympy§

In this problem, we will be using the sympy library for propositional logic to do inference. This will redefine the logic data structures and operations we were using in the previous problems and give us much faster inference.

Please take a moment to review the documentation: https://docs.sympy.org/latest/modules/logic.html.

Then complete the following warm up questions.

Feel free to import any additional components from the library.

4.1.1) Sympy Warmup 1§

Use sympy to determine whether the following formula is satisfiable: (\neg x_1 \land x_2) \Rightarrow ((x_2 \lor x_3) \land (x_1 \lor \neg x_3)).

Note that the return type should be bool.

For reference, our solution is 4 line(s) of code.

4.1.2) Sympy Warmup 2§

Use sympy to determine whether the following formula is satisfiable: (x_1 \lor x_2) \land (\neg x_1 \lor \neg x_2) \land (x_1 \lor \neg x_2) \land (\neg x_1 \lor x_2).

For reference, our solution is 4 line(s) of code.

4.2) Search and Rescue§

Now, we will look at the actual inference problem that we are interested in. We will consider several problems with varying grid sizes and different sets of observations. For example, consider the grid below:

# Fire, Unknown, Clear, Smoke
GRID0 = np.array([
  ["F", "U", "C"],
  ["S", "C", "U"],
  ["U", "U", "C"]
], dtype=object)

This grid has 9 locations and 5 observations: there is fire in the top left, smoke below it, and the center, top right, and bottom right locations are all known to be clear of smoke or fire.

We will assume the following axioms:

1. Each location has exactly one of {smoke, fire, clear}.
2. There is smoke at a location if and only if there is a fire in at least one of the adjacent (above, below, left, right) locations. Diagonals are not adjacent!

Note that as a corollary, there cannot be two fires in adjacent locations.

Take a moment to run your human inference engine: which unknown values in the grid above can be determined?

4.2.1) Search and Rescue Inference§

Write a program that takes a grid as input and infers unknown values.

Your program should output a new grid with all determinable unknown values replaced with the inferred value. If an unknown value cannot be determined, it should be left unknown.

Your program should use sympy.

For reference, our solution is 57 line(s) of code.

4.2.2) Beware§

Consider the following grid:

GRIDX = np.array([
    ["U", "U", "S", "U"],
    ["C", "U", "U", "S"],
    ["S", "U", "U", "U"],
    ["C", "S", "S", "S"]])

Use the staff solution for infer_unknown_values(click View Answer) on this input. The result should violate your expectations.

Note the line in infer_unknown_values:

       for elm in ["C", "S", "F"]:

Change that line so the that it reads:

        for elm in ["F", "S", "C"]:

Now what do you get? What's going on?

5) Feedback§

1. How many hours did you spend on this homework?

   -- <4 4-6 6-8 8-10 10-12 12-14 >14

   

2. Do you have any comments or suggestions (about the problems or the class)?