Horn子句谓词逻辑作为归约语言及其语义学

本文为谓词逻辑的 Horn 子句语言塑造了一种归约语言,构作了它的语义学。此语义学是相当简洁的,它能满足严格数学处理所要求的公理基础的简明性,并使逻辑程序设计语言纳入正式函数程序设计的体系结构的轨道而作好理论准备。大体说来,归约语言的((CE,C,μ),(A,K),ρ)部分相当于通常所说的语法和指称语义学(由于这里的函数均为单类型的,指称语义学就要简单得多);(E′,C′,τ)部分,则相当于通常的操作语义学。