非标准逻辑中的自动演绎
非标准逻辑中的自动演绎（英语：automatic deduction in nonstandard logics），许多复杂的常识推理问题如能直接用高阶逻辑或非经典逻辑来处理最为自然，然而这种技术还不够成熟。因此从实用的角度看,扩充一阶逻辑的功能,将非标准逻辑中的自动演绎问题在条件许可情况下，尽量转化为在一阶逻辑范围内可以解决的问题，已引起广泛注意。这类问题涉及高阶逻辑、使用内涵算符的逻辑和非单调逻辑等。
高阶逻辑
与一阶逻辑的区别在于量词不但可限定个体变元，而且也可限定函词变元和谓词变元，其意义在于如果在一阶谓词逻辑中只能反映关于个体对象的命题，则在二阶逻辑中便能反映关于个体对象属性和相互关系的命题，在三阶逻辑中还能反映有关这些属性、相互关系的属性和相互关系的命题，依此类推。在某些情况下，谓词结构不很复杂而不需要作谓词抽象，一阶谓词逻辑的标准推理程序也可用于二阶谓词逻辑的简单推理,例如将Wang is a teacher（王是一位教师）表示成TEACHER(WANG)，这里的TEACHER作为谓词使用。如果提出一个本来属于二阶逻辑范围的问题：王是干什么的？（即王的属性是什么？）演绎系统将x(WANG)与TEACHER(WANG)相匹配而得x=TEACHER。这里的变元x是谓词变元，它的值是个特定的函词，而不是一般的个体。但如果王是个将军或诗人，表示为 GENERAL(WANG)∨POET(WANG)，那么便需要进行谓词抽象,即将上述命题述为LAMBDA(Y)(GENERAL(Y)∨POET(Y))(WANG)，这就是与x(WANG)相匹配的正确形式。这里采用了对谓词精确地定义而不需要显式地给出谓词名的LAMBDA记法（见LISP语言）。如何将经典技术加以扩充以解决更普遍的问题，是人们正在研究的课题。
使用内涵算符的逻辑
如果允许在自动演绎中使用诸如 BELIEVE（相信）、KNOW（知道）这样的内涵算符，那么由此而得的命题，其真值不但取决于组成部分的真值，而且还取决于组成部分的涵义。经典逻辑中的许多规则,例如等值置换规则,在内涵算符的作用域内不再适用。如 He believes the morning star is Venus（他认为晨星就是金星)和 He believes the evening staris Venus（他认为昏星就是金星）。如果第一命题为真，而且晨星指的就是昏星,也不能认为第二命题为真,因为完全有可能他不知道或不认为晨星就是昏星。因此，即使他认为晨星就是金星，也不能就此得出他认为昏星也是金星的结论。运用S.A.克里普克和J.辛迪加的可能世界语义学(possible-world semantics)可在通常的一阶逻辑内解决使用内涵算符的逻辑问题。R.C.莫尔深入研究了如何在人工智能中实际运用内涵算符的问题。这一问题属于模态逻辑范畴。
非单调逻辑
在经典逻辑中，如果前提的数目增多时，便会使结论数目也相应地单调增加。但在常识推理中，随着论据数目的增加有时反而要删除某些结论，非单调逻辑即因此得名。一个经常援引的例子是人们知道某物是鸟时，他就会得出某物会飞的结论。但当他进一步知道该物是鸵鸟时，那么上述结论就要推翻，因为鸵鸟不会飞。更实际的例子是，根据某种前提，秘书作出某天下午开部门负责人联席会议的决定。但这一天上午接到紧急通知，要会议主持人到市里听报告，于是原拟当天下午举行的会议撤销。这类问题就属于用非单调逻辑的常识推理。已出现一些运用非单调逻辑的自动演绎系统，但理论根据还不充分。
参见
