关于三值逻辑程序中否定和蕴涵完备化程序的不动点语义

逻辑程序具有丰富的表达能力和非确定性等特点，在定理机器证明、关系数据库系统、程序验证、模块化程序设计和非单调推理等方面都有了广泛的应用。本文是继续文[8]的工作。首先通过两个反例，指出了文[7]中关于否定完备化程序comp（→，pr）和蕴涵完备化程序comp（→，pr）的两个重要定理都存在一定程度的错误。然后对这两个定理进行了修改，用后继算予tpt和fitting算予fpr的不动点语义，分别给出了否定完备化程序（somp（→，pr）和蕴涵完备化程序comp（→，pr）的herbrand模型的充分条件和必要