Homework #2: Proof of Concept

This assignment will be performed by individuals. We encourage you to discuss problems or insights, but you should perform the work yourself.

Assignment Overview

The assignment consists of a set of questions on logic (first-order logic and propositional logic) and a set of questions on uncertainty (Bayes nets).

Logic

The logic section has three parts which should occur in sequence.

Transform the given problems into first-order logic. You should have expressions describing the knowledge base and queries. You may use any reasonable connector/logical function (quantifiers, implication, negation, disjunction, conjunction, ...).
Define a finite universe for each quantified variable in the problem and rewrite the problem in propositional CNF form using the translation engine.
Run the CNF formula through a solver (we are providing you a and problem domain with which you can use with your search engine to solve CNF problems). Translate the resulting truth assignment into a solution for the FOL problem as well as the actual questions.

Problems

These problems come from the GRE (graduate record examination) section on analytical reasoning. Look up problems one and three in the analytical reasoning section of ETS's GRE practice questions. These define two separate scenarios each with one question. Encode the scenarios as the knowledge base and the answer choices as statements which are satisfiable in the given KB if and only if they are correct.

Solvers

Use the FOL to CNF translator to construct the CNF version of your problem (comments on how to use the translator are in the file).

Use the SAT problem for your search engines to solve the propositional formulas. There are comments on how to use the SAT problem in the code.

Note: you need not use your own team's engine to perform the search. You may use another team's.

Questions

What was the most difficult part of constructing your encoding?
Did you need to encode any information that was not explicit in the problem?
What advantages or disadvantages did encoding into FOL and then translating to CNF propositional form have over simply encoding in CNF? Did the advantages differ between the scenarios?
Give one characteristic that you could have added to one of the problems that would have made it more difficult to translate into propositional form.
Was the previous bullet really a question?
What about this bullet?
As always: what was right and wrong with this assignment? What did you learn? What was exciting? What would have been fun to do next (if only we had the time)?

Uncertainty

Consider the following Bayesian network:

The nodes in the graph are tied to the following events:

sleep: You got a good night's sleep on Tuesday.
coke: There's Coke in the drink machine Wednesday night.
all-night: You manage to stay up working on the homework all night Wednesday.
easy: The kindly professor made an easy exam.
test: You pass the test on Thursday.
finish: You finish the homework (due Thursday... maybe the prof's not so kindly).
pass: You pass the course.

Perform the following tasks using this network:

Write in reasonable numbers for the conditional probability of each cause given its effects. All effects with multiple causes should be noisy-OR style. No probability that you choose should be less than 0.01 or greater than 0.99. Explain your choices briefly.
Note at least three separate conditional independences.
Give the formula for (no numbers) and the solutions of (only one number) the following queries:
- P(all-night)
- P(pass|all-night)
Is this a polytree?

Note: your course grade is independent of your calculated probability of passing given that you calculate it correctly.

Questions

Just one here: how would you have changed the links in this Bayes net to more closely describe the situation (from your point of view)?

Submission

You should submit a paper copy of the problems in FOL, propositional logic, and CNF form as well as the solution to the problem. You should describe your method for performing each step of the translation (e.g., you encoded ball order with the predicate Before(ball1,ball2) which means that ball1 has a lower number in the order than ball2). You should mention insights and difficulties you ran into along the path to passing this subset of the GRE.

For the second part, you should submit a drawing of the Bayes net labelled with the probabilities. You should also submit paper copies of your answers to the other questions.

No code submission necessary for this assignment!