ASP中的基本概念
Ruolin WangAbout 3 minAnswer Set ProgrammingAnswer Set Programming
一个一阶逻辑的语句,经过Skolem化后可以等价转化为子句:
复习一下一阶逻辑,有
那么对于刚好含有一个正文字的子句(确定子句),就可以写成以条件运算符表示的规则形式:
它是的等价形式。 确定子句的有限集合称为 (传统)逻辑程序。
任给一个逻辑程序,中所有常项的集合称为的Herbrand域。 一阶逻辑的一个解释由一个论域,和一个从项和公式到上函数和关系的映射构成。 而一个传统逻辑程序的一个Herbrand解释是一个三元组。 其中,论域就是的Herbrand域,映射把任何常项和常原子映射为其自身。 因此对于一个确定的,和都是确定的。 是一个“指派”集合,是中所有常原子集合(Herbrand基)的子集。 任何常原子在指派下为真,当且仅当。 一个Herbrand解释称为一个程序的Herbrand模型,如果该程序的所有规则在该解释下为真。Herbrand模型具有以下性质:
- 任意子句集,如果存在一阶模型,则必然存在Herbrand模型。
- 任何传统逻辑程序有Herbrand模型。
- 任何传统逻辑程序的任意两个Herbrand模型的交是该程序的一个Herbrand模型。
- 任何传统逻辑程序有唯一的最小Herbrand模型。
- 给定传统逻辑程序, ,如果,则。
传统逻辑程序只能推理正文字形式的结论。 为了推理含有负文字的逻辑程序,需要增加额外的规则。 “失败即否定(negation as failure, NAF)”就是这样的一个规则,即:如果常原子无法被推出,则推出。
经典的一阶逻辑是单调的,即:如果语句是语句集的逻辑结论,那么一定是的任意超集的结论。 说人话就是,新规则的加入不影响已有结论的成立。 在NAF规则下进行的推理是非单调的,增加新知识后原有结论可能不再成立。例如:
- 鸟会飞,Tweety是鸟 Tweety会飞
- 鸟会飞,Tweety是鸟,Tweety不会飞 Tweety不会飞
- 鸟会飞,企鹅不会飞,Tweety是鸟,Tweety是企鹅 Tweety不知是否会飞
- 企鹅是鸟,鸟会飞,企鹅不会飞,Tweety是鸟,Tweety是企鹅 Tweety不会飞