谓词逻辑的回顾 合式公式 谓词符号集合、函数符号集合 (包括常量符 号)》 -基于 来定义项集 t::=xc ft,...,t) 归纳地定义基于(， )的合适公式 φ：=P(t1,t2,,tn)1(φ)1（φvφ）1（φ∧φ）1 (中→中)1(xφ)|（目xφ） (P∈ ·自由变量、约束变量、代换谓词逻辑的回顾 • 合式公式 – 谓词符号集合 、函数符号集合 （包括常量符 号） – 基于 来定义项集 t ::= x | c | f(t, …, t) – 归纳地定义基于（ , ）的合适公式  ::= P(t1 , t2 , …, tn ) | (  ) | (   ) | (   ) | ( →  ) | (x  ) | ( x  ) ( P ) • 自由变量、约束变量、代换