In this assignment, you will get some hands-on experience with logic. You'll see how logic can be used to represent the meaning of natural language sentences, and how it can be used to solve puzzles and prove theorems. Most of this assignment will be translating English into logical formulas, but in Problem 4, we will delve into the mechanics of logical inference.

NOTE: For this assignment only, there are only programming questions. Thus you do not need to submit a solution for the written portion. Also, there are no hidden test cases for the programming questions -- if you pass all the visible test cases, then you will get full credit!

To get started, launch a Python shell and try typing the following commands to add logical expressions into the knowledge base.

from logic import *
Rain = Atom('Rain')           # Shortcut
Wet = Atom('Wet')             # Shortcut
kb = createResolutionKB()     # Create the knowledge base
kb.ask(Wet)                   # Prints "I don't know."
kb.ask(Not(Wet))              # Prints "I don't know."
kb.tell(Implies(Rain, Wet))   # Prints "I learned something."
kb.ask(Wet)                   # Prints "I don't know."
kb.tell(Rain)                 # Prints "I learned something."
kb.tell(Wet)                  # Prints "I already knew that."
kb.ask(Wet)                   # Prints "Yes."
kb.ask(Not(Wet))              # Prints "No."
kb.tell(Not(Wet))             # Prints "I don't buy that."

==== Knowledge base [3 derivations] ===
* Or(Not(Rain),Wet)
* Rain
- Wet

The operations And and Or only take two arguments. If we want to take a conjunction or disjunction of more than two, use AndList and OrList. For example: AndList([Atom('A'), Atom('B'), Atom('C')]) is equivalent to And(And(Atom('A'), Atom('B')), Atom('C')).

Problem 1: Propositional logic

Write a propositional logic formula for each of the following English sentences in the given function in submission.py. For example, if the sentence is "If it is raining, it is wet," then you would write Implies(Atom('Rain'), Atom('Wet')), which would be $\text{Rain} \to \text{Wet}$ in symbols (see examples.py). Note: Don't forget to return the constructed formula!

1. "If it's summer and we're in California, then it doesn't rain."
2. "It's wet if and only if it is raining or the sprinklers are on."
3. "Either it's day or night (but not both)."

    python grader.py 1a
    

    Your formula (And(Rain,Wet)) says the following model is FALSE, but it should be TRUE:
    * Rain = False
    * Wet = True
    * (other atoms if any) = False
    

In this model, it's not raining and it is wet, which satisfies the correct formula $\text{Rain} \to \text{Wet}$ (TRUE), but does not satisfy the incorrect formula $\text{Rain} \wedge \text{Wet}$ (FALSE). Use these counterexamples to guide you in the rest of the assignment.

Problem 2: First-order logic

Write a first-order logic formula for each of the following English sentences in the given function in submission.py. For example, if the sentence is "There is a light that shines," then you would write Exists('$x', And(Atom('Light', '$x'), Atom('Shines', '$x'))), which would be $\exists x . \text{Light}(x) \wedge \text{Shines}(x)$ in symbols (see examples.py).

Tips:

• You can directly write '$x' instead of Variable('$x') to represent a variable symbol.
• Python tuples can span multiple lines, which help with readability when you are writing logic expressions (some of them in this homework can get quite large).

1. "Every person has a mother."

Note: You do NOT have to enforce that the mother is a "person".

2. "At least one person has no children."

Note: You do NOT have to enforce that the child is a "person".

3. Create a formula which defines Father(x,y) in terms of Male(x) and Parent(x,y).
4. Create a formula which defines Granddaughter(x,y) in terms of Female(x) and Child(x,y).

Note: It is ok for a person to be their own child.

Problem 3: Liar puzzle

1. Mark says: "It wasn't me!"
2. John says: "It was Nicole!"
3. Nicole says: "No, it was Susan!"
4. Susan says: "Nicole's a liar."
5. You know that exactly one person is telling the truth.
6. You also know exactly one person crashed the server.

1. Fill out liar() to return a list of 6 formulas, one for each of the above facts.
   The grader is set up such that you could run individual parts 3a-0 to 3a-5 to debug each formula only if you implement them in the order specified.

    python grader.py 3a-0
    python grader.py 3a-1
    python grader.py 3a-2
    python grader.py 3a-3
    python grader.py 3a-4
    python grader.py 3a-5
    python grader.py 3a-all  # Tests the conjunction of all the formulas
    

    python grader.py 3a-run
    

Problem 4: Odd and even integers

In this problem, we will see how to use logic to automatically prove mathematical theorems. We will focus on encoding the theorem and leave the proving part to the logical inference algorithm. Here is the theorem:

1. Each number $x$ has exactly one successor, which is not equal to $x$.
2. Each number is either odd or even, but not both.
3. The successor of an even number is odd.
4. The successor of an odd number is even.
5. For every number $x$, the successor of $x$ is larger than $x$.
6. Larger is a transitive property: if $x$ is larger than $y$ and $y$ is larger than $z$, then $x$ is larger than $z$.

• For each number, there is an even number larger than it.

Note: in this problem, "larger than" is just an arbitrary relation, and you should not assume it has any prior meaning. In other words, don't assume things like "a number can't be larger than itself" unless explicitly stated.

1. Fill out ints() to construct 6 formulas for each of the constraints. The consequence has been filled out for you (query in the code).
   The grader is set up such that you could run individual parts 4a-0 to 4a-5 to debug each formula only if you implement them in the order specified. You can test your code using the following commands:

       python grader.py 4a-0
       python grader.py 4a-1
       python grader.py 4a-2
       python grader.py 4a-3
       python grader.py 4a-4
       python grader.py 4a-5
       python grader.py 4a-all  # Tests the conjunction of all the formulas
       

   To finally prove the theorem, tell the formulas to the knowledge base and ask the query by running model checking (on a finite model):

       python grader.py 4a-run
       

Problem 5: Semantic parsing (extra credit)

Semantic parsing is the task of converting natural lanugage utterances into first-order logic formulas. We have created a small set of grammar rules in the code for you in createBaseEnglishGrammar(). In this problem, you will add additional grammar rules to handle a wider variety of sentences. Specifically, create a GrammarRule for each of the following sentence structures.

1. Example: Every person likes some cat. General template:

   $Clause ← every $Noun $Verb some $Noun

2. Example: There is some cat that every person likes. General template:

   $Clause ← there is some $Noun that every $Noun $Verb

3. Example: If a person likes a cat then the former feeds the latter. General template:

   $Clause ← if a $Noun $Verb a $Noun then the former $Verb the latter

    $ python nli.py
    
    > Every person likes some cat.
    
    >>>>> I learned something.
    ------------------------------
    > Every cat is a mammal.
    
    >>>>> I learned something.
    ------------------------------
    > Every person likes some mammal?
    
    >>>>> Yes.