HW 5 -- First Order Logic

The questions below are due on Monday March 17, 2025; 11:59:00 PM.
 

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

1) Propositional proof§

There are three suspects for a murder: Adams, Brown, and Clark.

1. Adams says "I didn't do it. The victim was an old acquaintance of Brown's. But Clark hated him."
2. Brown states "I didn't do it. I didn't know the guy. Besides I was out of town all week."
3. Clark says "I didn't do it. I saw both Adams and Brown in town around the victim that day; one of them must have done it."
4. We know that exactly one of the suspects is guilty.

Assume that the two innocent people are telling the truth, but that the guilty people might not be. So, the statements from the suspects can be encoded as "If suspect_is_innocent, then some other facts are true".

Let the propositional variables have the following definitions:

• A = Adams is innocent
• B = Brown is innocent
• C = Clark is innocent
• X = Brown knew the victim
• Y = Brown was out of town
• Z = Adams was out of town
• W = Clark hated the victim

1.1) Adams, Brown and Clark - The CNF§

We can write down propositional logic axioms for each of the four statements defining this problem. For propositional resolution, we need to convert these sentences to CNF. We will ask you to convert one sentence at a time. Enter one CNF formula corresponding to the specified sentence in each of the answer spaces below. (Refer to Lecture 9 slide 22 for a refresher on how to convert expressions to CNF).

Enter each CNF formula as a list of lists of literal strings. A literal string is either a propositional symbol, e.g. 'A' or the negation of a propositional symbol, e.g. '~A'. A typical clause will look like: ['A', '~B', '~C']. And a CNF formula is a list of clauses. Do not include any spaces in the strings.

1. The first axiom is: A \Rightarrow (X \land W)
   Enter the CNF as a formula following the syntax described above.

   
2. The second axiom is: B \Rightarrow (\neg X \land Y)
   Enter the CNF as a formula following the syntax described above.

   
3. The third axiom is: C \Rightarrow (\neg Y \land \neg Z \land (\neg A \lor \neg B))
   Enter the CNF as a formula following the syntax described above.

   
4. The fourth axiom is: (\neg A \lor \neg B \lor \neg C) \land ((A \land B) \lor (A \land C) \lor (B \land C))
   Enter the CNF as a formula following the syntax described above.

   

1.2) Adams, Brown and Clark: Proof of guilt§

We will continue our investigation of the Adams, Brown and Clark affair. In this episode, we prove conclusively that Brown is guilty. We will do that by using resolution refutation starting from the set of clauses that we derived in the previous episode.

1	\neg A \lor X
2	\neg A \lor W
3	\neg B \lor \neg X
4	\neg B \lor Y
5	\neg C \lor \neg Y
6	\neg C \lor \neg Z
7	\neg C \lor \neg A \lor \neg B
8	A \lor C
9	A \lor B
10	B \lor C
11	A \lor B \lor C

Note that we have dropped a duplicate clause that we derived from both the third and fourth of the original axioms.

In addition to the clauses derived from the original axioms, what additional clause do we need to add so as to be able to conclude that Brown is guilty using resolution refutation?

Now, enter the steps in a valid resolution proof. Each step will indicate the indices of two parent clauses (as integers) and the resolvent clause (as a list of literal strings), e.g. [3, 4, ['~X', 'A']]. The resolvent clause in each of the steps entered can be used in subsequent steps by using its index, starting with 13. Indicate a contradiction by entering an empty list for the clause, e.g. [1, 2, []]

The entries below illustrate the format; the number of required steps in the proof is not necessarily as indicated.

2) Semantics of FOL§

2.1) Entailment§

2.2) Modeling clay§

Consider the following set of sentences:

1. \text{isNumber}(0)
2. \forall x . \; \text{isNumber}(x) \Rightarrow \text{isNumber}(\text{successor}(x))
3. \forall x, y . \; \text{greater}(x, y) \Rightarrow (x = \text{successor}(y) \lor \exists z . \; x = \text{successor}(z) \land \text{greater}(z, y))
4. \forall x, y . \; \text{greater}(x, y) \Leftarrow (x = \text{successor}(y) \lor \exists z . \; x = \text{successor}(z) \land \text{greater}(z, y))

1. Consider the following model:

   Universe = {happy, grumpy, sleepy, doc, sneezy}    # these are actual dwarves
   Map from constant symbols to objects: {‘0’ -> doc}
   Predicate: isNumber = {doc}
   Function: successor = {{happy, happy}, {grumpy, grumpy}, {sleepy, sleepy}, {sneezy, sneezy}, {doc, doc}}
   Relation: greater = {{happy, happy}}
   

   Which sentences are true in this model?
   Enter a Python list whose elements are in {1, 2, 3, 4}.

   

2. Now consider the model

   Universe = Natural numbers
   Map from constant symbols to objects: {‘0’ -> 0}
   Function: successor = lambda x: x + 1
   Relation: greater = > relation on integers
   Predicate: isNumber = Universe
   

   Which sentences are true in this model?
   Enter a Python list whose elements are in {1, 2, 3, 4}.

   

3. Finally, consider the model where

   Universe = Natural numbers
   Map from constant symbols to objects: {‘0’ -> 1000}
   Function: successor = lambda x: x
   Relation: greater = all pairs of integers
   Predicate: isNumber = Universe
   

   Which sentences are true in this model?
   Enter a Python list whose elements are in {1, 2, 3, 4}.

   

3) First-order Logic Syntax and Semantics§

3.1) Atom Evaluation§

Note: for these questions, refer to the top of the Colab notebook. Write a function that takes a FOL atom and evaluates it against a single model.

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

3.2) First-order Logic Sentence Evaluation§

Use your implementation of evaluate_atom to complete the following implementation of FOL sentence evaluation.

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

In addition to all the utilities defined at the top of the Colab notebook, the following functions are available in this question environment: evaluate_atom. You may not need to use all of them.

4) Formalization§

4.1) First words§

For each of the following, write down a first-order logical sentence that captures the meaning of the English remark, using the allowed predicates. Your formulation may be different from ours; if you can't get what we're looking for, write a private question on Piazza. Also note the following operator precedence in FOL: quantifiers apply over the entire expression to their right, and's (i.e., conjunctions \land) are applied before or's (i.e., disjunctions \lor), and \neg immediately applies (takes higher precedence than and or or) to its argument.

1. Every student who takes AI has fun.
   
   Mark all that have the intended meaning

   	\forall x . \;\text{IsStudent}(x) \land \text{TakesAI}(x) \land \text{HasFun}(x)
   	\forall x . \;\neg\text{IsStudent}(x) \lor \neg \text{TakesAI}(x) \land \text{HasFun}(x)
   	\forall x . \;\neg\text{IsStudent}(x) \lor \neg \text{TakesAI}(x) \lor \text{HasFun}(x)
   	\forall x . \;\text{IsStudent}(x) \land \text{TakesAI}(x) \Rightarrow \text{HasFun}(x)

   
2. All problem sets from all students have been graded at some time point before the end the semester.
   We use the following abbreviations: \text{Pset}(p,s) means \text{ProblemSetByStudent}(p, s), \text{Graded}(p, t) means \text{GradedAtTime}(p, t) and \text{End}(t) means \text{EndOfSemester}(t). \text{Graded}(p, t) is true if and only if p is graded exactly at t, and \text{End}(t) is true if and only if t is exactly the end of semester. We also use \text{Before}(t, t'), which means time point t is strictly before t'.
   In the following logic formulas, we are going to use t, t' for time, s for students, and p for problemsets.
   Mark all that have the intended meaning

   	\forall t'. \lnot \text{End}(t') \lor (\forall s,p. \text{Pset}(p,s) \Rightarrow (\exists t. \text{Before}(t,t')\land \text{Graded}(p,t)))
   	\forall s,p,t.\exists t'. \left(\text{Pset}(p,s) \land \text{Graded}(p,t)\lor \lnot \text{Before}(t,t')\Rightarrow \lnot \text{End}(t')\right)
   	\forall s,p,t,t'. \left(\text{Pset}(p,s)\land \text{End}(t')\land \lnot \text{Before}(t,t') \Rightarrow \lnot \text{Graded}(p,t)\right)
   	\exists t'. \forall s,p,t. \left(\text{Pset}(p,s)\land \text{Graded}(p,t)\land \text{End}(t')\Rightarrow \text{Before}(t,t')\right)

   
3. This one is particularly tricky. Each breakout room has at least three unique students.
   We use the following abbreviations: \text{In}(s,r) means \text{InBreakoutRoom}(s,r). \textit{Eq}(s_1, s_2) is a predicate that is true when s_1 and s_2 are the same student.
   In the following logic formulas, we are going to use r for rooms, and s_1, s_2, s_3, s_4 for students.
   Mark all that have the intended meaning

   	\forall r,s_1,s_2,s_3. \left(\text{In}(s_1,r) \land \text{In}(s_2,r)\land \text{In}(s_3,r)\Rightarrow \lnot \text{Eq}(s_1, s_2) \land \lnot \text{Eq}(s_1, s_3) \land \lnot \text{Eq}(s_2, s_3)\right)
   	\forall r. \exists s_1,s_2,s_3. \text{In}(s_1, r) \land \text{In}(s_2, r) \land \text{In}(s_3, r) \land \lnot \text{Eq}(s_1, s_2) \land \lnot \text{Eq}(s_1, s_3) \land \lnot \text{Eq}(s_2, s_3)
   	\forall r. \exists s_1. \forall s_2,s_3. \exists s_4. \lnot \text{Eq}(s_2, s_4) \land \lnot \text{Eq}(s_3, s_4) \land \text{In}(s_1, r) \land \text{In}(s_4, r)
   	\forall r. \exists s_1,s_2,s_3. \left(\text{In}(s_1, r) \land \text{In}(s_2, r) \land \text{In}(s_3, r) \Rightarrow \lnot \text{Eq}(s_1, s_2) \land \lnot \text{Eq}(s_1, s_3) \land \lnot \text{Eq}(s_2, s_3)\right)

   
4. People who work from home can never work and relax in the same room.
   In the following logic formulas, we are going to use p for people, and r for rooms.
   Mark all that have the intended meaning

   	\forall p .\; \forall r . \;\text{WorksFromHome}(p) \land \text{WorksInRoom}(p, r) \Rightarrow \neg \text{RelaxesInRoom}(p, r)
   	\neg \exists p, r . \;\text{WorksFromHome}(p) \land \text{WorksInRoom}(p, r) \land \text{RelaxesInRoom}(p, r)
   	\neg \exists p, r . \;\text{WorksFromHome}(p) \Rightarrow \text{WorksInRoom}(p, r) \land \text{RelaxesInRoom}(p, r)
   	\forall p .\;\neg \exists r . \;\text{WorksFromHome}(p) \land \text{WorksInRoom}(p, r) \land \text{RelaxesInRoom}(p, r)
   	\forall p .\;\neg \exists r . \;\text{WorksFromHome}(p) \land \text{WorksInRoom}(p, r) \Rightarrow \text{RelaxesInRoom}(p, r)

   

5) FOL Proof§

5.1) FOL clausal form§

Convert each of these sentences into clausal form.

Enter each formula as a list of lists of literal strings. A literal string is either a term, e.g. 'O(x,y)' or the negation of a term, e.g. '~O(x,y)'. A typical clause will look like: ['D(y)', '~O(x,y)', '~L(x)']. And a CNF formula is a list of clauses. If you need a Skolem function, call it sk, e.g. sk(x). In these problems, you will not need more than one Skolem function. Do not include any spaces in the strings.

1. Anybody who owns a dog is an animal lover!
   \forall x . \; (\exists y . \; D(y) \land O(x,y)) \Rightarrow L(x)
   

   

2. Every animal lover owns a dog!
   \forall x . \; L(x) \Rightarrow (\exists y . \; D(y) \land O(x,y))
   

   

3. Dr. Evil doesn’t own a dog. From this, we would like to conclude that he is not an animal lover. We can draw this conclusion based on one of the sentences above. Which one?

   Enter a number (1 or 2)

   

5.2) FOL resolution§

Now, we will use the sentence you chose in part 5.1.3 as an assumption, also assume that Dr. Evil does not own a dog, and then prove from these assumptions that Dr. Evil is not an animal lover. The first step in doing a resolution proof is to convert the premises to clausal form. You already did part of that! Below, you will select each of the premises that we will need for a proof.

1. Clause 1 One clause from the previous problem that involves a dog, that is, predicate D. Recall the process of standardizing variables apart for clauses that will be used in a resolution proof.

   Choose one:

   	~D(x1)
   	D(sk(x1))
   	~L(x1) v D(x2)
   	~L(x1) v D(sk(x1))
   	~D(x2) v ~O(x1, x2) v L(x1)

   

2. Clause 2 One clause from the previous problem that involves an owner, that is, predicate O.

   Choose one:

   	~O(x2,x3)
   	O(x2,sk(x2))
   	~L(x2) v O(x2,x3)
   	~L(x2) v O(x2,sk(x2))
   	~D(x3) v ~O(x2, x3) v L(x3)

   

3. Clause 3 We need to add to our premises that Dr. Evil doesn’t own a dog. Choose the clausal form; use constant symbol ‘DrE’ for Dr. Evil.

   Choose one:

   	O(DrE, x3)
   	~O(DrE, x3)
   	O(DrE, x3) v D(x3)
   	~O(DrE, x3) v ~D(x3)
   	~O(DrE, x3) v D(x3)

   

4. Clause 4 We also need to negate the desired conclusion and convert it to clausal form.

   Choose one:

   	L(x4)
   	~L(x4)
   	L(sk())
   	~L(sk())
   	L(DrE)
   	~L(DrE)

   

5. Clause 5 Now, we can actually do the proof, using FOL resoluton, starting with the four clauses above. We get another clause by resolving clauses 1 and 4.
   

   Enter a clause as a list of lists of literal strings.

   

6. Clause 6 We get the next clause by resolving clauses 2 and 4.

   Enter a clause as a list of lists of literal strings.

   

7. Clause 7 We then resolve clauses 3 and 5.

   Enter a clause as a list of lists of literal strings.

   

8. Now we get a contradiction between clauses 6 and 7 and we're done!

6) First-order Logic Inference§

6.1) FOL Binary Resolution§

Complete the following implementation of first-order binary resolution. Given two clauses, return all possible new clauses that result from applying the binary resolution rule.

Hint 1: The helper function unify may return an empty dict for certain inputs. Note that this means the inputs can be successfully unified without any variable substitution.

Hint 2: In your code, you can use if unify(a, b, {}) is not None to test if the unification is successful.

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

6.2) FOL Resolution Prover§

Complete the following implementation of a first-order resolution prover. Given a sentence in CNF form, and a single query clause, check if the sentence entails the query. See unit tests for examples.

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

In addition to all the utilities defined at the top of the Colab notebook, the following functions are available in this question environment: binary_resolution. You may not need to use all of them.

7) (Bonus) Real-World Applications§

The ideas we've covered in this homework (Propositional Logic and First-Order Logic) were extremely influential in AI and underpin several important modern applications.

To follow up last week's real-world applications of propositional logic, propositional logic is also commonly used in tools for digital circuit design to simulate and simplify circuits.

First order logic has widespread use cases within computer science. It forms the structure for many automated theorem provers. These automated theorem provers are then used in formal verification tools. Formal verification attempts to prove or disprove the correctness of a system or program. To do so, it must ensure there exists a formal proof that a program follows a given formal specification. Automated theorem provers such as Vampire or Coq rely on first order logic to do so.

Formal verification methods are used across a variety of companies. With these formal verification tools and first order logic, we're able to prove that a program has no bugs or security vulnerabilities.

In the real world, formal verification tools have protected and provide gurantees for essential systems including the C programming language and x86 assembly language.

We have a class at MIT (Formal Reasoning About Programs) that teaches more about formal verification methods if you want to learn more!

8) Feedback§

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

   -- 2 3 4 5 6 7 8 more

   

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