DOC PREVIEW
Stanford CS 157 - Study Notes

This preview shows page 1-2-3-19-20-38-39-40 out of 40 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 40 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 40 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 40 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 40 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 40 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 40 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 40 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 40 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 40 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

1Review Session!2Finals Info• Time: Thursday,December 12, 3:30-6:30pm• Location: TBD• Alternate Time: TBD• Alternate Location: TBD • Material covered: everything3Table of Contents• Propositional Logic• Propositional Proofs• Propositional Resolution• Relational Logic• Relational Logic Semantics• Herbrand• Relational Logic Proofs• Unification• Relational Resolution• Applications• Strategies• Ordered Resolution•Epilog• Equality and Induction4Propositional Logic• Constants– Alphanumeric words– Start with lower case letter– Cannot include punctuation or other funny characters• Compound Sentences– Build compound sentences using below operators¬∧ ∨⇔⇐⇒5Propositional Logic• Interpretations– Any assignment of truth values to each of the constants. • Valid / Contingent / Unsatisfiable– How do you figure these out? • Truth table• Using validities, such as deMorgan’s Laws, Implication Introduction, Implication Distribution6Propositional Proofs• Logical entailment– If every interpretation that satisfies the set of premises also satisfies the conclusion, then the set of premises logically entails the conclusion• How do you show logical entailment?– Truth table method– Inference rules (MP, MT, EE, DN)– Axiom schemata (II, ID, CR, EQ, OQ) + MP• Soundness & Completeness7Propositional Resolution• Clausal form (INDO)• Negated goal• Resolution issues{ ~p, ~q }{ p, q}{q, ~q}{p, ~p}{}{ ~p, q }{ p, q}{q}{q, q}{ p, q }{ p }No resolvents{q} { p, ~p }{ p, ~p }{ p, ~p }8Relational Logic•Term–Variable– Object constant– Functional term• Sentences– Relational sentences– Logical sentences– Quantified sentences9Relational Logic• Remember:– Terms are NOT sentences in relational logicmomma1(sutin) – Relational sentences can only be formed with terms. loves2(sutin, person1(dad))• Relations vs. Functions– Relational sentences evaluate to True or False– Functional terms evaluate to things in the universe of discourse10Relational Logic• Quantifiers (∀ and ∃)– Order of appearance matters∀x.∃y.loves(x,y)∃y.∀x.loves(x,y)– A variable is bound by the “closest” available quantifier for the variable∃y.∀x.(∃y.q(y) ⇒ (∃x.∃y.∃z.∀x.p(z,x) ∨∀u.q(x)))11Relational Logic• More quantifiers (∀ and ∃)– You probably don’t want implications in ∃−quantified sentences"sutin loves some cats”Universe of discourse = { all animals }∃y.(cat(y) ⇒ loves(sutin, y))∃y.(cat(y) ∧ loves(sutin, y))12Relational Logic• More quantifiers (∀ and ∃)– On the other hand, you might consider using implications for ∀−quantified sentences“sutin loves all dogs”Universe of discourse = { all animals }∀y.(dog(y) ⇒ loves(sutin, y))∀y.(dog(y) ∧ loves(sutin, y))13Relational Logic Semantics• Model“an arbitrary set of ground, atomic sentences in which all arguments are constants”Sentence: ∀y.(dog(y) ⇒ loves(walter, y))Universe: { fluffy, poopy, duffy, goofy}Model 1: { dog(goofy), loves(walter, goofy) }Model 2: { dog(poopy), dog(goofy) }14Herbrand• Herbrand universe– Set of all constants used in our sentences• Herbrand base– Set of all ground atomic sentences formed using the constants from the Herbrand universe• Herbrand model– Any subset of the Herbrand base• Example: See problem set #2 problem #815Herbrand• Herbrand method– Add negated conclusion to the set of premises— “satisfaction set”– Loop over Herbrand interpretations and cross out the ones that do not satisfy the satisfaction set– If all interpretations have been crossed out, then premises logically entail the conclusion• When negating goal, Skolemize if the goal is universally quantified16Relational Proofs• Universal Instantiation (UI)∀y.hates(mike, y)  hates(mike, mother(mike))∀x.∃y.hates(x, y) ∃y.hates(woojin, y)∀x.∃y.hates(x, y) ∃y.hates(mother(y), y)17Relational Proofs• Existential Instantiation (EI)∃y.hates(woojin, y)  hates(woojin, someone)∃y.hates(woojin, y)  hates(woojin, woojin)∃y.hates(x, y)  hates(x, f(x))∃y.hates(x, y)  hates(x, mother(x))∃y.hates(x, y)  hates(x, woojin)18Relational Proofs• Use inference rules (MP, MT, AE, AI) or axiom schemata like before…19Unification• Pure & Impure substitutions• Composition of substitutions• Composable & Noncomposable substitutions•Unifier• Most General Unifier20Unification•Unifier?p(u,v) { u y, x  v } = p(y,v)p(y,x) { a y, x  v } = p(y,v)p(a, f(x)) { x  a, f(x)  b } = p(a, b)p(x, b) { x  a, f(x)  b } = p(a, b)21Unification• Most General Unifier– Follow the flow chart on p.20 of lecture #9 notes22Relational Resolution• Clausal form (INSEADO)• Negated goal– Watch out for quantifiers when negating• When resolving two clauses, you can– Rename the variables– Unify the clauses23Relational Resolution• INSEADO example:∃y.∀x.∃z.[ (p(x,y) & ∃y.q(y)) ⇒ (∃x.∃y.∃z.∀x.p(z,x) | ∀u.q(x)) ]24Relational Resolution• Common mistakes:1. { ~p(x), q(b) }2. { p(a), q(x)}3. No resolvents1. { p(x), q(x) }2. { ~p(a) }3. { q(x) } 1,21. { p(x), q(x) }2. { ~p(a) }3. { p(a), q(a) } UI4. { q(a) } 2,31. { ~r(x, y), ~r(y, z), r(x, z) }2. No resolvents25Relational Resolution•Example:“Assume that binary relation R has the properties of irreflexivityand transivity. Using resolution, show that R is asymmetric.”Premises: ~r(x,x)r(x,y) & r(y,z) ⇒ r(x,z)Goal: r(x,y) ⇒ ~r(y,x)26Relational Resolution•Example:{ ~r(x,x) } 1. Premise{ r(x,y) & r(y,z) ⇒ r(x,z) } 2. Premise{ r(x,y) } 3. Neg Goal{ r(y,x) } 4. Neg Goal27Applications• Logical Entailment“is smart(tim) logically entailed by the premises?”Add: smart(tim) ⇒ goal• Answer Extraction / Fill-in-the-Blank Resolution“find a term x such that smart(x) is true”Add: smart(x) ⇒ goal(x)28Strategies• Elimination Strategies– Identical Clause Elimination– Pure Literal Elimination– Tautology Elimination– Subsumption Elimination• Restriction Strategies– Unit Restriction– Input Restriction– Linear Restriction– Set of Support Restriction29Strategies• All elimination strategies are complete• Unit Resolution is incomplete– Lecture 12, Slide 26• Input Resolution is incomplete– Lecture 12, Slide 29• Linear Resolution is complete• Set of Support Resolution is


View Full Document

Stanford CS 157 - Study Notes

Documents in this Course
Lecture 1

Lecture 1

15 pages

Equality

Equality

32 pages

Lecture 19

Lecture 19

100 pages

Epilog

Epilog

29 pages

Equality

Equality

34 pages

Load more
Download Study Notes
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Study Notes and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Study Notes 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?