1Relational LogicComputational Logic Lecture 5Michael Genesereth Spring 20042Propositional LogicConstants refer to atomic propositions.raining snowing wetCompound sentences capture relationships among propositions.raining ∨ snowing wet23Relational LogicConstants refer to objects and relationships.joe mary loves happySimple sentences express relationships among objects.loves(joe,mary) Compound sentences capture relationships among relations.loves(x,y) loves(y,x)loves(x,y) ∧ loves(y,x) happy(x)4Plan of ActionRelational Logic Syntax and Informal SemanticsFormal SemanticsHerbrand MethodRelational ProofsUnificationRelational ResolutionApplicationsStrategiesModel EliminationEpilogEquality35WordsVariables begin with characters from the end of the alphabet (from u through z).u, v, w, x, y, zConstants begin with digits or letters from the beginning of the alphabet (from a through t). a, b, c, arthur, betty, cathy, 1, 2, ...6ConstantsObject constants refer to objects in the universe of discourse.Function constants denote functions.father, mother, age, plus, timesRelation constants refer to relations.person, happy, parent, lovesThere is no syntactic distinction between object constants, function constants, and relation constants. The type of each such word is determined from context.47ArityThe arity of a function constant or a relation constant is the number of arguments it takes.Unary Function constants: father1, motherBinary Function constants: plus2, times2Ternary Function constants: price3Unary Relation constants: person1, happy1Binary Relation constants: parent2, loves2Ternary Relation constants: between3The arity of a function constant or a relation constant is optionally notated as a subscript on the constant.8TermsA term is either a variable, an object constant, ora functional term.Terms refer to items in the universe of discourse.Terms are analogous to noun phrases in natural language.59Functional TermsA functional term is an expression formed from an n-ary function constant and n terms enclosed in parentheses and separated by commas.father1(joe)age1(joe)plus2(x,2)Functional terms are terms and, as such, can be nested.plus2(age1(father1(joe)),age1(mother1(joe)))10SentencesThere are three types of sentences.Relational sentences - analogous to the simple sentencesin natural languageLogical sentences - analogous to the compound sentencesin natural languageQuantified sentences - sentences that express the significanceof variables611Relational SentencesA relational sentence is an expression formed from an n-ary relation constant and n terms enclosed in parentheses and separated by commas.happy1(art)loves2(art,cathy)Relational sentences are not terms and cannot be nested in terms or relational sentences.No! happy1(person1(joe)) No!happy1(joe)person1(joe)12Logical SentencesLogical sentences in Relational Logic are analogous to those in Propositional Logic.¬loves(art,cathy)(loves(art,betty) ∧ loves(betty,art))(loves(art,betty) ∨ loves(art,cathy))(loves(x,y) loves(y,x))(loves(x,y) ⇐ loves(y,x))(loves(x,y) ⇔ loves(y,x))Parenthesization rules are the same as for Propositional Logic.713Quantified SentencesQuantified sentences can be nested within other sentences.∀x.apple(x) ∨ ∃x.pear(x))∀x.∀y.loves(x,y)14Syntax TestObject Constants: art, betty, cathy, 1, 2, ...Function Constants: father1, mother1,age1, plus2, times2Relation Constants: person1, happy1, reflexive2,parent2, loves2, lt2lt(father(art),mother(betty))plus(father(art),betty)happy(person(cathy))loves(x,y) loves(y,x)reflexive(z) z(x,x)815ReminderFunctional terms and relational sentences look similar.However, they are not the same.Functional terms may be used within other functional terms.Functional terms may be used within relational sentences.Relational sentences may not be used in functional terms.Relational sentences may not be used in relational sentences.16Infix Syntax for Functionsplus(2,3)↔2+3minus(2,3) ↔ 2 − 3times(2,3) ↔ 2 × 3quotient(2,3) ↔ 2 ÷ 3expt(2,3) ↔ 2 ↑ 3union(s,t) ↔ s ∪tintersection(s,t) ↔ s ∩ t917Infix Syntax for Relationseq(2,3)↔2=3nq(2,3) ↔ 2 ≠ 3lt(2,3) ↔ 2 < 3gt(2,3) ↔ 2 > 3leq(2,3) ↔ 2 ≤ 3geq(2,3) ↔ 2 ≥ 3member(s,t) ↔ s ∈tsubset(s,t) ↔ s ⊂ tsubseteq(s,t) ↔ s ⊆ t18Operator Precedence↑× ÷+ −∩∪= ≠ < > ≤ ≥∈∉⊂ ⊃ ⊆ ⊇¬ ∀ ∃∧∨⇐ ⇔ 1019MushroomsUnary relation constants: mushroom, purple, poisonousPurple mushrooms are poisonous.If a thing is a purple mushroom, then it is poisonous.If a thing is mushroom and it is purple, then it is poisonous.∀x.(mushroom(x) ∧ purple(x) poisonous(x))No purple mushroom is poisonous.There is no thing that is a mushroom and purple and poisonous.¬∃x.(mushroom(x) ∧ purple(x) ∧ poisonous(x))20More MushroomsUnary relation constants: mushroom, purple, poisonousA mushroom is poisonous only if it is purple.If a thing is a mushroom, it is poisonous only if it is purple.If a thing is a mushroom and it is poisonous, then it is purple.∀x.(mushroom(x) ∧ poisonous(x) purple(x))A mushroom is not poisonous unless it is purple.If a thing is a mushroom, it is not poisonous if it is not purple.If a thing is a mushroom and it is poisonous, then it is purple.∀x.(mushroom(x) ∧ poisonous(x) purple(x))1121Interpersonal RelationsObject constants: mike, maureenBinary relation constant: lovesEverybody loves Maureen.∀x.loves(x,maureen)Maureen loves everyone who loves her.∀x.(loves(x,maureen) loves(maureen,x))Nobody loves Mike.¬∃x.loves(x,mike)Nobody who loves Maureen loves Mike.∀x.(loves(x,maureen) ¬loves(x,mike))22More Interpersonal RelationsObject constants: mike, maureenBinary relation constant: lovesEverybody loves somebody.∀x.∃y.loves(x,y)There is somebody whom everybody loves.∃y.∀x.loves(x,y)1223Abelian GroupsAssociativity AxiomCommutativity AxiomIdentity AxiomsInverse Axioms(x+y)+z=x+(y+z)x+y=y+x0+y=yy +0= yx+inv(x)=0inv(x) + x = 024Open Partial OrdersNon-reflexivity¬x<xAsymmetryx<y ¬y<xTransitivityx<y ∧ y<z x<z1325Binary TreesRepresentation as a term:pair(pair(a,b),pair(c,d))Membership axioms:in(x,x)in(x,pair(y,z)) ⇐ in(x,y) ∨ in(x,z)a b c d26Variable Length ListsExample[a,b,c,d]Representation as Termcons(a,cons(b,cons(c,cons(d,nil))))LanguageObjconst: nilFunconst: consRelconst: memberMembership axioms:member(x,cons(x,y))member(x,cons(y,z)) ⇐ member(x,z)a
View Full Document
Unlocking...