15-381: Artificial IntelligenceAssignment 2: Game Theory and LogicDue: Thursday, September 27, 2001 (before class)This is the second assignment for 15-381. Similar to the first assignment itcontains both written exercises and a programming assignment.Written ExercisesExercise 1(a) For the game tree given below, show which branches would be pruned byalpha-beta and write down all the node values propagated by the algo-rithm.17 6 8 629 5 3MAXMINA2A1A3(b) Which action should the MAX player choose?Exercise 2(a) For the game tree given below, show which branches would be pruned byalpha-beta and write down all the node values propagated by the algo-rithm.11194 2 12849131 1291013MAXMINMAXA1A2A3(b) Reorder the children of nodes so that the maximum number of nodes arecut from the tree.Exercise 3Do exercise 5.8 on page 147 in Artificial Intelligence: A Modern Approach.Programming AssignmentFor this programming assignment you will be implementing a theorem proverfor a clause logic using the resolution principle1. Well-formed sentences in thislogic are clauses. As discussed in class, we will be using the disjunctive forminstead of the implicative form, since this form is more suitable for automaticmanipulation. The syntax of sentences in the clause logic is the following:Clause ::= Literal ∨···∨LiteralLiteral ::= ¬Atom | AtomAtom ::= Tr u e | False | P | Q | ...We will regard two clauses as identical if they have the same literals. Forexamples, q ∨¬p∨q, q∨¬p,and¬p∨qare equivalent for our purposes. Forthis reason we adopt a standardized representation of clauses, with duplicateliterals always eliminated.When modeling real domains, clauses are often written on the formLiteral ∧···∧Literal ⇒ Literal.1You need to be familiar with the comp onents of a logic in order to solve this implemen-tation assignment. If needed, re-read section 6.2, 6.3, and 6.4 i n the Artificial Intelligence: AModern Approach.2In this case we need to transform the clauses such that they conform to thesyntax of the clause logic. This can always be done using the following simplerules:1. p ⇒ q is equivalent to ¬p ∨ q2. ¬(p ∨ q ∨ ...)isequivalentto¬p∧¬q∧...3. ¬(p ∧ q ∧ ...)isequivalentto¬p∨¬q∨...4. (p ∧ q) ∧ ... is equivalent to p ∧ q ∧ ...5. (p ∨ q) ∨ ... is equivalent to p ∨ q ∨ ...6. ¬(¬p)isequivalenttopThe proof theory of the clause logic contains only the resolution rule:¬a ∨ l1∨···∨lna∨L1∨···∨Lml1∨...ln∨L1∨···∨LmIf there are no literals l1,... ,lnand L1,... ,Lmthe resolution rule has the form:¬aaFalseRemember that inference rules are used to generate new valid sentences,given that a set of old sentences are valid. For the clause logic this means thatwe can use the resolution rule to generate new valid clauses given a set of validclauses. Consider a simple example where p ⇒ q, z ⇒ y,andpare valid clauses.To prove that q is a valid clause, we first need to rewrite the rules to disjunctiveform: ¬p ∨ q, ¬z ∨ y,andp. Resolution is then applied to the first and the lastclause, and we get:¬p ∨ qpqIf False can be deduced by resolution, the original set of clauses is inconsis-tent. When making proofs by contradiction this is exactly what we want to do.The approach is illustrated by the resolution principle explained below.The Resolution PrincipleTo prove that a clause is valid using the resolution method, we attempt to showthat the negation of that clause is unsatisfiable, meaning it cannot be true underany truth-assignment. This is done using the following algorithm:1. Negate the clause and add each literal in the resulting conjunction ofliterals to the set of clauses already known to be valid.2. Find two clauses for which the resolution rule can be applied. Change theform of the produced clause to the standard form and add it to the set ofvalid clauses.33. Repeat 2 until False is produced, or until no new clauses can be produced.If no new clauses can be produced, report failure; the original clause isnot valid. If False is produced, report success; the original clause is valid.Consider again our example. Assume we now want to prove that ¬z ∨ y isvalid. First we negate the clause and get z ∧¬y. Then each literal is added tothe set of valid clauses. The resulting set of clauses is:1. ¬p ∨ q2. ¬z ∨ y3. p4. z5. ¬yResolution on 2 and 5 gives:1. ¬p ∨ q2. ¬z ∨ y3. p4. z5. ¬y6. ¬zFinally, we apply the resolution rule on 4 and 6, which produces False.Thus,the original clause ¬z ∨ y is valid.Part I: The ProgramYour program should read a text file containing the initial set of valid clauses,and a clause for each literal in the negated clause that we want to test validityof. Each line in the file defines a single clause. The literal of each clause areseparated by a blank space, and “∼” is used to represent negation.Your program should implement the resolution algorithm as specified in theprevious section. The output is “Invalid clause” if the clause can not be shownto be valid, or the list of clauses in the proof tree for deducing False. In eithercase you should also output the size of the final set of valid clauses.Let us consider a correct solution for testing the validity of ¬z ∨ y in ourearlier example. The input file would be:~p q~z ypz~y4A possible output could be:1. ~p q {}2. ~z y {}3. p {}4. z {}5. ~y {}6. ~z {2,5}7. False {4,6}Size of final clause set: 7Note how the program keeps track of the parents of new clauses. This is usedfor extracting the clauses in the proof tree.Part II: Loki in Pittsburgh?It is now time to put your resolution prover to work! In Norse mythology thereare gods and giants. One person, Loki, is both a giant and a god, so if you meetsomeonewhoisbothoftheseyouknowyouhavemetLoki. Abravepersonwhois violent and not admired is a giant. If a person is violent but not brave, orneither brave nor admired, then that person is also giant. A person who is bothwise and handsome must surely be a god. A one-eyed person is wise becausehe has given one of his eyes to drink from the spring of wisdom. A person whostill has both eyes, but who is not violent, is also wise. Only handsome peoplecan get married. If you are not married, but admired, then you are for certainhandsome. Formally, these rules can be described by the following clauses:God ∧ Giant ⇒ LokiBrave ∧ Violent ∧¬Admired ⇒ Giant¬Brave ∧ Violent ⇒ Giant¬Brave ∧¬Admired ⇒ GiantWise ∧
View Full Document
Unlocking...