非单调逻辑（Non-monotonic logic）
目录 |
非单调逻辑是（在前提的集合和单一的句子之间的）推论关系不是单调递增的形式逻辑。
与单调推理（经典逻辑）相对，非单调推理是指知识库加入新知识后，原有的推论会被推翻的逻辑。也就是说，知识库的推论不随着知识增长而增长，即非单调递增。这时，必须使用某种正确的维持机制，确保推理继续进行。因此，非单调推理多是在知识不完全的情况下发生的。
多数形式逻辑都有单调性的推论关系，就是说，如果一个句子可以从前提的集合中推理出来，则它也可以从把这个前提集合作为子集包含的任何前提集合中推理出来，这意味着向理论增加一个公式永不引起它的推论集合的减小。在直觉上，单调性指示出学习一些新知识不能减小已知知识的集合。单调逻辑不能处理各种推理任务比如缺省推理（事实可以是已知的，只是因为缺乏反面的证据）、溯因推理（事实只按最合适的解释演绎出来）、关于知识的推理（在事实变成已知的时候，对一个事实的无知必须被撤消），和信念修正（新知识可以和旧信念矛盾。）
目前对于非单调推理的研究一般有两种途径：
一种方法认为经典逻辑对于研究非单调推理明显有不足的地方，因此最好是建立新的语义机制跟逻辑系统。在此基础上进行非单调推理的研究以解决一些问题，例如Reiter的缺省逻辑和Moore的自动认识逻辑，还有扩充逻辑程序（英语：extended logic program）。
另一种观点与此正好相反，坚持这种观点的人认为，在经典逻辑框架下研究非单调推理是完全可行的，关键是怎么使用经典逻辑。例如封闭世界假设，McCarthy的限定推理（Circumscription）和Poole提出的假设推理（default reasoning）。
缺省假定的一个例子是典型的鸟类辨识。作为结果，如果给出一个是鸟的动物，并且不知道其他事情，就假定它会飞。如果后来知道这个动物其实是企鹅，这个事实无论如何都必须被撤销。这个例子展示了建模缺省推理的逻辑不应当是单调的。形式化缺省推理的逻辑可以粗略的分为两类：可以处理任意的缺省假定的逻辑（缺省逻辑、可废止逻辑和回答集编程），和形式化不知道为真的事实可以被缺省假定为假的特殊缺省假定的逻辑（封闭世界假定和限制）。
溯因推理是推导已知事实的最可能解释的过程。溯因逻辑不应当是单调的，因为最可能的解释不是必然正确的。例如，看到潮湿的草地的最可能的解释是下雨了；但是在知道了草地潮湿的真正原因是浇水了的时候，这个解释应当被撤销。因为获得了增加的知识（洒水车经过了），旧的解释（下雨了）被撤消了，建模解释的任何逻辑都是非单调的。
信念修正是改变信念来调和出可能同旧信念矛盾的一个新信念。在新信念是正确的假定下，某些旧信念必须撤销来维持一致。适应增加新信念的这种撤销使用于信念修正的任何逻辑都是非单调的。信念修正方法是对次协调逻辑的替代选择，它容忍矛盾而不是尝试去除它。