程序验证（五）：一阶理论的过程 主要讨论 T E T_E TE​的量词自由片段以及 T A T_A TA​ 等价理论的判定 等价及未解释函数理论(Theory of Equality and Uninterpreted Functions) 除=外的谓词实际上使我们的讨论不必要地复杂化，去除这些累赘谓词的方法如下： 对每个谓词 p p p，引入一个新的(fresh)函数符号 f p f_