15-780: Graduate AILecture 3. FOL proofsGeoff Gordon (this lecture)Tuomas SandholmTAs Erik Zawadzki, Abe OthmanAdmin2HW1Out todayDue Tue, Feb. 1 (two weeks)hand in hardcopy at beginning of classCovers propositional and FOLDon’t leave it to the last minute!3Collaboration policyOK to discuss general strategiesWhat you hand in must be your own workwritten with no access to notes from joint meetings, websites, etc.You must acknowledge all significant discussions, relevant websites, etc., on your HW4Late policy5 late days to split across all HWsthese account for conference travel, holidays, illness, or any other reasonsAfter late days, out of 70th %ile for next 24 hrs, 40th %ile for next 24, no credit thereafter (but still must turn in)Day = 24 hrs or part thereof, HWs due at 10:30AM5Office hoursMy office hours this week (usually 12–1 Thu) are canceledEmail if you need to discuss something with me6Review7NPDecision problemsReductions: A reduces to B means B at least as hard as AEx: k-coloring to SAT, SAT to CNF-SATSometimes a practical toolNP = reduces to SATNP-complete = both directions to SATP = NP?8Propositional logicProof trees, proof by contradictionInference rules (e.g., resolution)Soundness, completenessFirst nontrivial SAT algorithmHorn clauses, MAXSAT, nonmonotonic logic9FOLModelsobjects, function tables, predicate tablesCompositional semanticsobject constants, functions, predicatesterms, atoms, literals, sentencesquantifiers, variables, free/bound, variable assignments10Proofs in FOLSkolemization, CNF Universal instantiationSubstitution lists, unificationMGU (unique up to renaming, exist efficient algorithms to find it)11Proofs in FOL12QuizCan we unifyknows(John, x) knows(x, Mary)What aboutknows(John, x) knows(y, Mary)13QuizCan we unifyknows(John, x) knows(x, Mary)What aboutknows(John, x) knows(y, Mary)No!x → Mary, y → John14Standardize apartBut knows(x, Mary) is logically equivalent to knows(y, Mary)!Moral: standardize apart before unifying15First-order resolutionGiven clauses (α ∨ c), (¬d ∨ β), and a substitution list L unifying c and dConclude (α ∨ β) : LIn fact, only ever need L to be MGU of c, d16Example1718First-order factoringWhen removing redundant literals, we have the option of unifying them firstGiven clause (a ∨ b ∨ θ), substitution LIf a : L and b : L are syntactically identicalThen we can conclude (a ∨ θ) : LAgain L = MGU is enough19CompletenessUnlike propositional case, may be infinitely many possible conclusionsSo, FO entailment is semidecidable (entailed statements are recursively enumerable)Jacques Herbrand1908–1931First-order resolution (w/ FO factoring) is sound and complete for FOL w/o equality (famous theorem due to Herbrand and Robinson)20Algorithm for FOLPut KB ∧ ¬S in CNFPick an application of resolution or factoring (using MGU) by some fair rulestandardize apart premisesAdd consequence to KBRepeat21VariationsEqualityParamodulation is sound and complete for FOL+equality (see RN)Or, resolution + factoring + axiom schemaRestricted semanticsOnly check one finite, propositional KBNP-complete much better than REUnique names: objects with different names are different (John ≠ Mary)Domain closure: objects without names given in KB don’t existKnown functions: only have to infer predicates24UncertaintySame trick as before: many independent random choices by Nature, logical rules for their consequencesTwo new difficultiesensuring satisfiability (not new, harder)describing set of random choices25Markov logicAssume unique names, domain closure, known fns: only have to infer propositionsEach FO statement now has a known set of ground instancese.g., loves(x,y) ⇒ happy(x) has n2 instances if there are n peopleOne random choice per rule instance: enforce w/p p (KBs that violate the rule are (1–p) times less likely)26Richardson & DomingosIndependent Choice LogicGeneralizes Bayes nets, Markov logic, Prolog programs—incomparable to FOLUse only acyclic KBs (always feasible), minimal model (cf. nonmonotonicity)Assume all syntactically distinct terms are distinct (so we know what objects are in our model—perhaps infinitely many)Label some predicates as choices: values selected independently for each grounding27Inference under uncertaintyWide open topic: lots of recent work!We’ll cover only the special case of propositional inference under uncertaintyThe extension to FO is left as an exercise for the listener28Second order logicSOL adds quantification over predicatesE.g., principle of mathematical induction:∀P. P(0) ∧ (∀x. P(x) ⇒ P(S(x))) ⇒ ∀x. P(x)There is no sound and complete inference procedure for SOL (Gödel’s famous incompleteness theorem)OthersTemporal and modal logics (“P(x) will be true at some time in the future,” “John believes P(x)”)Nonmonotonic FOLFirst-class functions (lambda operator, application)…Who? What?Where?Wh-questionsWe’ve shown how to answer a question like “is Socrates mortal?”What if we have a question whose answer is not just yes/no, like “who killed JR?” or “where is my robot?”Simplest approach: prove ∃x. killed(x, JR), hope the proof is constructivemay not work even if constr. proof exists32Answer literalsInstead of ¬P(x), add (¬P(x) ∨ answer(x))answer is a new predicateIf there’s a proof of P(foo), can eliminate ¬P(x) by resolution and unification, leaving answer(x) with x bound to foo33ExampleExampleExampleInstance GenerationBounds on KB valueIf we find a model M of KB, then KB is satisfiableIf L is a substitution list, and if (KB: L) is unsatisfiable, then KB is unsatisfiablee.g., mortal(x) → mortal(uncle(x))38Bounds on KB valueKB0 = KB w/ each syntactically distinct atom replaced by a different 0-arg propositionlikes(x, kittens) ∨ ¬likes(y, x) → A ∨ ¬BKB ground and KB0 unsatisfiable ⇒ KB unsatisfiable39PropositionalizingLet L be a ground substitution listConsider KB’ = (KB: L)0KB’ unsatisfiable ⇒ KB unsatisfiableKB’ is propositionalTry to show contradiction by handing KB’ to a SAT solver: if KB’ unsatisfiable, doneWhich L?40ExampleLiftingSuppose KB’ satisfiable by model M’Try to lift M’ to a model M of KBassign each atom in M the value of its corresponding proposition in M’break ties by specificity where possiblebreak any further ties arbitrarily42Example¬kills(Jack, Cat)kills(Curiosity, Cat)¬kills(Foo, Cat)M’Discordant pairsAtoms kills(x, Cat), kills(Curiosity, Cat)each tight for its clause in