论文部分内容阅读
任意一个一阶谓词公式F,先找到其中的个体常元和函数符号,并由此产生公式F的Herbrand域,然后用Herbrand域中的项替代公式F中的变元,以消去量词符号而得到公式F的函数形式.公式F的所有可能的函数形式组成的集合就是Herbrand扩张.研究了寻找一阶谓词公式与Herbrand扩张之间的关系.