方程逻辑

方程逻辑（equational logic），理学-计算机科学技术-计算机科学理论-可计算模型-形式化，以等式符号为唯一谓词符号的一阶逻辑，是一种通过等式替换进行推理的形式系统。又称等式逻辑。方程逻辑是一种特殊的一阶逻辑，其谓词符号只有一个等号“=.”。1935年，Birkhoff将方程逻辑的模型论发展成泛代数，并给出了方程逻辑在泛代数语义下的完备性定理及其证明。20世纪80年代方程逻辑被Dijkstra和Scholten等用于程序的形式化，随后被用于定理证明。该逻辑还用于群论的形式化和定理证明。关于方程逻辑的研究现在已经扩展到二阶方程逻辑（second order equational logic）、多类方程逻辑（many sorted equational logic）、模糊方程逻辑（fuzzy equational logic）等。方程逻辑的语言和谓词逻辑的语言是相同的，除了谓词符号只含有一个“=”。方程逻辑的项和谓词逻辑的项的定义是相同的，其定义如下：常量是项；变量是项；如果是项，则是项，其中是元函数符号。方程逻辑中等式的形式为，式中和均为项。