摘要:
基于回答集(稳定模型)语义的逻辑程序设计提供了一种非单调、不完全知识表示与推理的重要方法。最近,各种有效的回答集求解系统的出现,大大地推动了逻辑程序的应用,包括常识推理、智能规划、智能诊断、任务调度和语言学研究等理论方面以及美国航天飞机设计的具体应用领域。一般地,判定一个逻辑程序是否回答集是NP-完全的,这使得我们相信(至少目前如此),没有多项式时间的算法来求解其稳定模型。所以,具有多项式时间可计算其稳定模型的逻辑程序自然就是理想的一个子类。例如Marek等提出的前向链(FC)正规逻辑程序、序一致(order-consistent)逻辑程序以及调用一致(call-consistent)逻辑程序等。类似于前向链构造方法,我们提出了逻辑程序回答集的一个新特征:一个逻辑程序P的一个回答集M恰好对应于P的一个极大强相容子程序Q,使得任何Q之外的P的非单调规则r都是关于P弱自相容的。另外,我们定义了一类逻辑程序——弱自相容逻辑程序,它们具有(几乎所有)FC-正规逻辑程序的性质:回答集存在并多项式时间可计算、半单调性以及协调的证明模式;并且,弱自相容逻辑程序类真包含FC-正规逻辑程序类。
自相容缺省理论与FC-正规逻辑程序有许多相似的地方,但是在逻辑程序中的自相容概念并没有得到充分的研究。一般认为自相容概念要比前向链正规概念更一般,但是它们究竟是什么关系并没有结论。为了深入了解它们之间的关系,我们将缺省理论中的自相容概念(包括相容性和Λ算子)引入到逻辑程序中,在深入研究这样的逻辑程序后,发现尽管自相容性概念是句法定义上的约束,但是它具有非常接近语义定义的特点。从而提出了弱自相容逻辑程序类,并揭示了弱自相容逻辑程序真包含FC-正规逻辑程序类。关于这一类逻辑程序的两个推理问题(谨慎推理和轻信推理)复杂性的研究发现,它们与FC-正规逻辑程序的对应问题一样难。更进一步的研究发现,这一类的逻辑程序是难判定的,FC-正规性的判定目前还不知道,但我们相信FC-正规性的判定不会比弱自相容性的判定更容易。与其它易处理的逻辑程序——序一致逻辑程序和调用一致逻辑程序比较发现,它们不可比。这说明了它们出发点的差别。
本文的主要结论包括两个方面:首先是回答集的一个新特征;另一方面是一类真包含FC-正规并具有与FC-正规(几乎)一样性质的弱自相容逻辑程序类。该结论直接蕴含了两个亟待解决的问题:该回答集的新特征如何应用在当前的回答集求解系统中,从实际解决问题的效果上来揭示它的时效,目前已经有人在尝试这种回答集求解的方法,它的应用前景还有待深入研究;另一个问题正如前面所述,判定弱自相容性是co-NP完全的,那么FC-正规性到底有多难?是否有更容易判定且具有类似性质的逻辑程序?
当然,回答集程序的可应用性已经得到了普遍的认同,要把回答集程序设计应用到更多的实际应用中,例如计算机安全模型、程序正确性诊断,还面临很多挑战,全世界回答集程序设计的研究队伍正在不断地冲刺这些挑战。