Description
General Instructions
This (and every) assignment has a written part and a programming part.
The full assignment with our supporting code and scripts can be downloaded as logic.zip.
This icon means a written answer is expected in logic.pdf.
This icon means you should write code in submission.py.
All written answers must be in order and clearly and correctly labeled to receive credit.
You should modify the code in submission.py between
# BEGIN_YOUR_CODE
and
# END_YOUR_CODE
but you can add other helper functions outside this block if you want. Do not make changes to files other than submission.py.
Your code will be evaluated on two types of test cases, basic and hidden, which you can see in grader.py. Basic tests, which are fully provided to you, do not stress your code with large inputs or tricky corner cases. Hidden tests are more complex and do stress your code. The inputs of hidden tests are provided in grader.py, but the correct outputs are not. To run the tests, you will need to have graderUtil.py in the same directory as your code and grader.py. Then, you can run all the tests by typing
python grader.py
This will tell you only whether you passed the basic tests. On the hidden tests, the script will alert you if your code takes too long or crashes, but does not say whether you got the correct output. You can also run a single test (e.g., 3a-0-basic) by typing
python grader.py 3a-0-basic
We strongly encourage you to read and understand the test cases, create your own test cases, and not just blindly run grader.py.
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.
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.”
To print out the contents of the knowledge base, you can call kb.dump(). For the example above, you get:
==== Knowledge base [3 derivations] ===
* Or(Not(Rain),Wet)
* Rain
– Wet
In the output, ‘*’ means the fact was explicitly added by the user, and ‘-‘ means that it was inferred. Here is a table that describes how logical formulas are represented in code. Use it as a reference guide:
Name Mathematical notation Code
Constant symbol stanford Constant(‘stanford’) (must be lowercase)
Variable symbol x Variable(‘$x’) (must be lowercase)
Atomic formula (atom) Rain
LocatedIn(stanford,x) Atom(‘Rain’) (predicate must be uppercase)
Atom(‘LocatedIn’, ‘stanford’, ‘$x’) (arguments are symbols)
Negation ¬Rain Not(Atom(‘Rain’))
Conjunction Rain∧Snow And(Atom(‘Rain’), Atom(‘Snow’))
Disjunction Rain∨Snow Or(Atom(‘Rain’), Atom(‘Snow’))
Implication Rain→Wet Implies(Atom(‘Rain’), Atom(‘Wet’))
Equivalence Rain↔Wet (syntactic sugar for Rain→Wet∧Wet→Rain) Equiv(Atom(‘Rain’), Atom(‘Wet’))
Existential quantification ∃x.LocatedIn(stanford,x) Exists(‘$x’, Atom(‘LocatedIn’, ‘stanford’, ‘$x’))
Universal quantification ∀x.MadeOfAtoms(x) Forall(‘$x’, Atom(‘MadeOfAtoms’, ‘$x’))
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 Rain→Wet in symbols (see examples.py). Note: Don’t forget to return the constructed formula!
[2 points] “If it’s summer and we’re in California, then it doesn’t rain.”
[2 points] “It’s wet if and only if it is raining or the sprinklers are on.”
[2 points] “Either it’s day or night (but not both).”
You can run the following command to test each formula:
python grader.py 1a
If your formula is wrong, then the grader will provide a counterexample, which is a model that your formula and the correct formula don’t agree on. For example, if you accidentally wrote And(Atom(‘Rain’), Atom(‘Wet’)) for “If it is raining, it is wet,”, then the grader would output the following:
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 Rain→Wet (TRUE), but does not satisfy the incorrect formula Rain∧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 ∃x.Light(x)∧Shines(x) in symbols (see examples.py).
Tip: 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)
[2 points] “Every person has a mother.”
[2 points] “At least one person has no children.”
[2 points] Create a formula which defines Daughter(x,y) in terms of Female(x) and Child(x,y).
[2 points] Create a formula which defines Grandmother(x,y) in terms of Female(x) and Parent(x,y).
Problem 3: Liar puzzle
Someone crashed the server, and accusations are flying. For this problem, we will encode the evidence in first-order logic formulas to find out who crashed the server. You’ve narrowed it down to four suspects: John, Susan, Mark, and Nicole. You have the following information:
John says: “It wasn’t me!”
Susan says: “It was Nicole!”
Mark says: “No, it was Susan!”
Nicole says: “Susan’s a liar.”
You know that exactly one person is telling the truth.
You also know exactly one person crashed the server.
[8 points] Fill out liar() to return a list of 6 formulas, one for each of the above facts. Be sure your formulas are exactly in the order specified.
You can test your code using the following commands:
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
To solve the puzzle and find the answer, tell the formulas to the knowledge base and ask the query CrashedServer(‘$x’), by running:
python grader.py 3a-run
Problem 4: Logical Inference
Having obtained some intuition on how to construct formulas, we will now perform logical inference to derive new formulas from old ones. Recall that:
Modus ponens asserts that if we have two formulas, A→B and A in our knowledge base, then we can derive B.
Resolution asserts that if we have two formulas, A∨B and ¬B∨C in our knowledge base, then we can derive A∨C.
If A∧B is in the knowledge base, then we can derive both A and B.
[5 points] Some inferences that might look like they’re outside the scope of Modus ponens are actually within reach. Suppose the knowledge base contains the following two formulas:
KB={(A∨B)→C,A}.
Your task: First, convert the knowledge base into conjunctive normal form (CNF). Then apply Modus ponens to derive C. Please show how your knowledge base changes as you apply derivation rules.
Hint: You may use the fact that P→Q is equivalent ¬P∨Q.
Remember, this isn’t about you as a human being able to arrive at the conclusion, but rather about the rote application of a small set of transformations (which a computer could execute).
[5 points] Recall that Modus ponens is not complete, meaning that we can’t use it to derive everything that’s true. Suppose the knowledge base contains the following formulas:
KB={A∨B,B→C,(A∨C)→D}.
In this example, Modus ponens cannot be used to derive D, even though D is entailed by the knowledge base. However, recall that the resolution rule is complete.
Your task: Convert the knowledge base into CNF and apply the resolution rule repeatedly to derive D.
Problem 5: 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:
If the following constraints hold:
Each number x has exactly one successor, which is not equal to x.
Each number is either odd or even, but not both.
The successor of an even number is odd.
The successor of an odd number is even.
For every number x, the successor of x is larger than x.
Larger is a transitive property: if x is larger than y and y is larger than z, then x is larger than z.
Then we have the following consequence:
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.
[8 points] Fill out ints() to construct 6 formulas for each of the constraints. The consequence has been filled out for you (query in the code). You can test your code using the following commands:
python grader.py 5a-0
python grader.py 5a-1
python grader.py 5a-2
python grader.py 5a-3
python grader.py 5a-4
python grader.py 5a-5
python grader.py 5a-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 5a-run
[10 points] Suppose we added another constraint:
A number is not larger than itself.
Prove that there is no finite, non-empty model for which the resulting set of 7 constraints is consistent. This means that if we try to prove this theorem by model checking only finite models, we will find that it is false, when in fact the theorem is true for a countably infinite model (where the objects in the model are the numbers).
Problem 6: 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.
[5 points] Example: Every person likes some cat. General template:
$Clause ← every $Noun $Verb some $Noun
[3 points] Example: There is some cat that every person likes. General template:
$Clause ← there is some $Noun that every $Noun $Verb
[4 points] 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
After implementing these functions, you should be able to try some simple queries using nli.py! For example:
$ 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.