Table of Contents First-Order Logic Why FOL? Syntax and semantics of FOL Using FOL Knowledge engineering in FOL Inference in FOL Reducing first-order inference to propositional inference Unification(合一 Generalized Modus Ponens(一般化分离规则 Forward and backward chaining Resolution 4口◆4⊙t1三1=，￥9QC
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Table of Contents First-Order Logic Why FOL? Syntax and semantics of FOL Using FOL Knowledge engineering in FOL Inference in FOL Reducing first-order inference to propositional inference Unification (合一) Generalized Modus Ponens（一般化分离规则） Forward and backward chaining Resolution
Syntax of FOL:Basic elements ~Constants/常量 KingJohn,2,USTC,.. ,Predicates/谓词 Brother,>. ~Functions/函数 Sqrt,LeftLegOf, ~Variables/变量 x,y,a,b,. ,Connectives/连接词 一，→，，V,台 ·Equality/等词 ~Quantifiers/量词 ,3 口卡回t·三4色，是分Q0
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Syntax of FOL: Basic elements ▶ Constants/常量 KingJohn, 2, USTC, … ▶ Predicates/谓词 Brother, >, … ▶ Functions/函数 Sqrt, LeftLegOf, … ▶ Variables/变量 x, y, a, b, … ▶ Connectives/连接词 ¬, ⇒,∧,∨,⇔ ▶ Equality/等词 = ▶ Quantifiers/量词 ∀, ∃
Atomic sentences（原子语句) Term function (term1,,termn)or constant or variable Atomic sentence predicate (term1,..,termn)or term1 term2 E.g.,Brother(KingJohn,RichardTheLionheart) >(Length(LeftLegOf(Richard)),Length(LeftLegOf(KingJohn))) 4口◆4⊙t1三1=，￥9QC
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Atomic sentences（原子语句） Term = function (term1, …, termn) or constant or variable Atomic sentence = predicate (term1, …, termn) or term1 = term2 ▶ E.g., Brother(KingJohn, RichardTheLionheart) >(Length(LeftLegOf(Richard)), Length(LeftLegOf(KingJohn)))
Complex sentences(复合语句) Complex sentences are made from atomic sentences using connectives S,S1∧S2,S1VS2,S1→S2,S1台S2. E.g. Sibling(KingJohn,Richard)=Sibling(Richard,KingJohn) >(1,2)V≤(1,2) >(1,2)A>(1,2) 口卡4三4色进分QC
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Complex sentences（复合语句） Complex sentences are made from atomic sentences using connectives ¬S, S1 ∧ S2, S1 ∨ S2, S1 ⇒ S2, S1 ⇔ S2, E.g. Sibling(KingJohn, Richard) ⇒ Sibling(Richard, KingJohn) > (1, 2)∨ ≤ (1, 2) > (1, 2) ∧ ¬ > (1, 2)
Truth in first-order logic ·语句的真值由一个模型和对句子符号的解释来判定。 Sentences are true with respect to a model and an interpretation ~Model contains objects(domain elements域元素)and relations among them 我们需要一个对分别被常量、谓词和函数符号指代的对象、 关系和函数进行详细说明的解释 Interpretation specifies referents(指代)for constant symbols→ objects predicate symbols → relations function symbols functional relations An atomic sentence predicate(term1,..,termn)is true iff the objects referred to by term1,...termn are in the relation referred to by predicate 4口◆4⊙t1三1=，￥9QC
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Truth in first-order logic ▶ 语句的真值由一个模型和对句子符号的解释来判定。 Sentences are true with respect to a model and an interpretation ▶ Model contains objects (domain elements 域元素) and relations among them ▶ 我们需要一个对分别被常量、谓词和函数符号指代的对象、 关系和函数进行详细说明的解释 Interpretation specifies referents（指代）for constant symbols → objects predicate symbols → relations function symbols → functional relations ▶ An atomic sentence predicate(term1, …, termn) is true iff the objects referred to by term1, …, termn are in the relation referred to by predicate