6 825 Midterm Solutions Fall 2006 November 7 2006 1 Search 16 points Let s formulate resolution theorem proving as a search problem A state is a set of clauses The descendants of a state are all the ways that the state can be augmented by the result of a possible resolution in that state which yields a new clause not in the state The goal is a state that includes a contradiction null clause Answer the following questions and provide a brief explanation justifying your answers 1 Assuming we are dealing with propositional logic clauses which search should you use Depth First Breadth First Uniform Cost or A We know the space is bounded so all the methods will eventually find an answer the only question is how much work they will do Using depth first means that we will only resolve a particular pair of clauses only once but we might find a proof that is very long Breadth first will find the shortest proof but it will end up resolving the same pair of clauses potentially many times as it considers different orders of doing resolution along different branches Uniform cost will behave like breadth first with additional overhead A with a heuristic related to size of clauses so that it prefers to do unit resolutions could be faster on average than uniform cost or breadth first but it would still repeat resolutions on different branches The key point is that the way this search has been set up is wasteful because it s searching over different orders of doing the resolutions but that doesn t affect the answer proofs don t depend on the order of the resolutions In fact one should do all the possible resolutions at each step so we don t have to search over order This is called a level saturation strategy 2 Is your search guaranteed to terminate Will it find a contradiction if one exists We know that repeatedly applying propositional resolution without duplication will eventually either run out of resolutions or find a contradiction if one exists So any systematic search method will eventually terminate and find a contradiction if one exists 3 Assuming we are dealing with first order logic clauses would you need to change the formulation of the problem and or your choice of search to get a theorem prover that is guaranteed to find a contradiction if one exists If so explain how 1 One part of the answer is that we need factoring and paramodulation unless we axiomatize equality in addition to resolution to get completeness The other part is that now the search space can be infinite Consider the following clauses P x P f x P f y Note that the resolvent is P f f y and then you can use it again and again So depth first is out as a possible search strategy 4 Is your search guaranteed to terminate Will it find a contradiction if one exists If a contradiction does not exist the search may not terminate semi decidability of first order logic If a contradiction exists the search will terminate due to the refutation completeness of resolution factoring paramodulation 2 Entailment 8 points Let S1 and S2 be sentences in propositional logic let I1 be the set of interpretations that make S1 true and let I2 be the set of interpretations that make S2 true Assume that I1 is a subset of I2 Mark all of the statements which must be true in this case 1 S1 entails S2 Yes 2 S2 entails S1 No 3 S2 can be proven from S1 with any sound proof system Not necessarily 4 S2 can be proven from S1 with any complete proof system Yes 5 The sentence S1 S2 is satisfiable Yes 6 The sentence S1 S2 is valid Yes 7 The sentence S2 S1 is satisfiable Not necessarily This one is tricky This sentence might not be satisfiable if for instance S2 is true and S1 is false 8 The sentence S2 S1 is valid No if it s not satisfiable it can t possibly be valid 2 3 Writing FOL 6 points Write the following sentence in standard First Order Logic notation Use only the following oneplace predicates Dog Cat and Bird and the following two place predicates Eat and Hate where the first argument is the subject and the second is the object that is Hate x y means that x hates y Some dogs hate all cats who eat birds d Dog d c Cat c b Bird b Eat c b Hate d c 4 Logical Inference 9 points 1 Write a possible result of applying resolution on P y f y P x y and P A w P x A 2 Write a possible result of applying paramodulation on P f x f y g x and Q z P g h z For example P f h z Q z P f y 3 Write the clause form for x y P x y y Q x y Two clauses P x sk1 x Q x sk2 x Q x y P x z 3 5 First Order 21 points Here are some English sentences and their translation into clausal form 1 Every state has a governor G f x1 x1 2 The governor of a state is in the state G x2 y2 In x2 y2 3 In is transitive In x3 y3 In y3 z3 In x3 z3 4 Governors are Republicans G x4 y4 R x4 5 MA a state is in the US In M A US 6 Prove that There is a Republican in the US Write the clause you would need to include to prove this R x6 In x6 US We d like to prove the conclusion using resolution refutation This proof is kind of tricky so we re going to tell you in English what the steps should be For each step say which of the previous clauses P1 and P2 in the table it can be derived from using resolution what the resulting clause is and what the unifier is Step 7 8 9 10 11 12 P1 P2 Clause Unifier Every governor is in their state one term 1 2 In f x1 x1 x2 f x1 y2 x1 If a state is in some location then its governor is in that location two terms 3 7 In x1 z3 In f x1 z3 x3 f x1 y3 x1 The governor of a state is a Republican one term 1 4 R f x1 x4 f x1 y4 x1 The governor of MA is in the US one term 5 8 In f M A U S x1 M A z3 U S There is no state whose governor is in the US one term 6 9 In f x1 U S x6 f x1 False 10 11 nil x1 M A 4 6 Bayesian networks 20 points 1 8 pts Draw a Bayesian network among the following binary variables that model the outcome of an election I candidate is Incumbent M has lots of Money for advertising A uses …