逻辑推理的消解（resolution）方法是由J.A.Robinson于1965年提出的。之后，J.R.Slagle于1967年提出了语义消解，D.W.Loveland和D.Luckham于1970年提出了线性消解，R.S.Boyer于1971年提出锁消解。我国有些学者把resolution翻译成归结。

1982年汪湘浩和他的学生研究了归结（即，消解）方法中的取因子问题并提出了广义归结方法sup[116]。广义归结方法包含了普通归结方法和非子句归结方法（N.V.默里，1982）。在汪湘浩的指导下，他的学生在归结方法的研究中提出了一些有用的改进策略。例如，刘叙华等把广义归结推广到了带等词的逻辑上sup[292]。孙吉贵，刘叙华等使用C-PROLOG语言在SUN工作站上设计实现了基于广义归结和基于归结的两个定理机器证明系统GRM，RM，证明了《数学原理》中PART 1：Mathematical Logic中Section A与Section B中全部定理（350个）。他们讨论GRM和RM的时空复杂性，并在实现设计中提出新的全局调度策略及归结式的化简、排序策略，以单子句恒真、恒假的判断代替了广义归结中的自归结，实现了带OCCUR检查的模式匹配sup[14]。N.V.Murray在1982年提出NC-消解。刘叙华和孙吉贵比较了广义归结与NC-归结sup[293]。

刘叙华认为各种消解方法的相容性（compatibility）是改进消解方法的一种途径。在20世纪70年代刘叙华就证明了，语义消解和锁消解是相容的，基于此结果，他提出了锁语义消解。进而，他证明语义消解与线性消解是不相容的。到了1986年刘叙华又证明了，当限制到HORN公式上，线性消解和锁消解在某些提条件下是相容的。到了1991年，刘叙华和他的学生提出了半锁（semi-lock）消解，并证明它和线性消解是相容的，进而，他们提出了线性半锁消解sup[291]。

众所周知，正单元消解对于HORN公式是（反驳）完全的，陆汝钤证明了正单元消解加上“有序”的限制后对HORN公式仍是完全的sup[298]。这一结果推广了L.Henschen和L.Wos的结果[J.Assoc.Comput.Mach.，Vol.21，1974，pp.590-605]。进而，陆汝钤证明了，强有序输入消解对HORN公式也是完全的sup[300][301]。李大法也研究了关于HORN公式的消解方法sup[273]。

R.Boyer和L.Moore经过十多年的努力建立了一个定理证明器（下文称BM证明器），陆汝占和孙永强等对Boye-Moore方法进行了扩充和修改sup[62][64]。陆汝占和孙永强等还给出一种新的语义归结方法，称为着色归结方法，证明了PI着色碰撞与电子排列次序无关，同时给出该方法的完备性证明sup[63]。

Robinson于1965年提出的合一（unification）算法，仅适用于没有量词的合取范式。清华大学李大法提出了适用于带量词公式的合一算法，该算法不需要Skolem化，因而可以应用于基于自然推导的定理自动证明系统。李大法实现了他的算法，并解决了Andrews，Bledsoe和Pelletier提出的挑战sup[272][275]。P.B.Andrews和G.P.Huet分别把J.A.Robinson的消解原理和合一算法推广到了高阶逻辑。D.A.Miller在他的博士论文中sup[205]提出在扩张树中可以删除高层Shallow公式，李大发则认为应删除底层公式sup[274]。李大法还对J.von Plato提出的仿射和射影几何公理系统进行了改进和简化sup[276][277]。

Z.Galil于1977年提出了如下问题，是不是消解树中每个最短的（concensus）路径都是正则的（regular）？黄文奇等给出一个反例，从而否定地回答了这一问题sup[263]。黄文奇、李未以及金人超、宋恩民、余向东、许如初等把数学、物理学以及社会学中的思想应用于SAT算法sup[259][262][283]。黄文奇和金人超设计出了求解SAT问题的拟物拟人算法——Solar，基于该算法的SAT Slover在北京“SAT问题快速算法国际邀请赛”（1996年3月）上获得第一名sup[261]。

张健于1992开始研究自动推理。重写技术是处理等式理论的一种有效方法，它已成功地应用到带等词的一阶谓词逻辑中定理的自动证明。张健将几种重写证明技术与经典的消解证明方法加以比较sup[156]。张健还以一阶逻辑的方法处理约束满足问题，他研究了一阶逻辑公式可满足性的局部搜索法，并与命题逻辑中的可满足性过程加以比较，以皇后问题和哈密顿回路问题为例，说明基于一阶逻辑能处理较大的问题实例sup[159]。关于张健在2000年前的工作可参考他的专著sup[157]。当解释的论域是一个固定大小的有限集合时，一阶逻辑公式的可满足性问题可以等价的归约为SAT问题，为了利用现有的高效SAT工具，张健和黄拙提出了一种从一阶逻辑公式生成SAT问题实例的算法，并描述了一个自动的转换工具，给出了相应的实验结果，还讨论了通过增加公式来消除同构从而减小搜索空间的一些方法，实验表明，这一算法是有效的，可以用来解决数学研究和实际应用中的许多问题sup[44]。张健和徐贵红研究了一阶逻辑推理工具对语义网的推理支持。语义网的关键推理问题可以化为公式的可满足性判定问题，一阶逻辑的自动定理证明器可以证明不可满足性，而有限模型查找器为可满足的公式在有限域内构造模型。张健提出在语义网的推理中，同时使用定理证明器和有限模型查找器。实验结果表明，这样可以解决描述逻辑工具的不足，并可以弥补定理证明器对可满足的公式推理的不完备性sup[145]。

吴尽昭和刘卓军将一阶谓词演算的定理证明转化为代数簇的计算，从而获得了代数化的Herbrand过程，又通过一阶多项式间的求余运算，给出了余式方法并证明了它的完备性。同时，证明了归结原理是余式方法的一种特例sup[140][357]。

由于在消解过程中，一个子句可以被使用任意多次，致使消解证明可能需要指数多步。为了限制消解步数，日本学者Iwama等人提出了只读消解，即要求每个子句最多只能被用一次。Iwama意识到判定一公式是否有只读消解证明是NP-完全的。赵希顺与德国学者合作给出了严格证明。众所周知，对任意固定的k，一个公式是否有k-消解证明是多项式时间可解的。但赵希顺证明了，只读k-消解证明的存在性却变成NP-完全的了sup[237][238]。

苏开乐和他的学生在知识结构（knowledge structure）的语义基础上，通过挖掘知识结构语义中各元素的关系，把知识的计算归约于可满足性问题（SAT）。因为SAT Solver在符号化计算方面以及在计算规模和效率上都要明显优于BDD，实验结果证实了这种方法的有效性sup[101]。苏开乐和他的学生还把各种形式化方法（如：有界模型检测）应用于知识推理和信息安全技术sup[102]。苏开乐和他的学生所实现的MAX-SAT算法在2008年和2009年的SAT年会举办的相关竞赛中取得优异成绩。

张文辉在20世纪90年代研究命题逻辑的自动推理。他主要研究cut-消去的复杂性及其对证明结构的影响sup[386][387]。

近年来，由于描述逻辑在语义网中的广泛应用，描述逻辑的自动推理技术也是研究热点。描述逻辑的推理一般用结构包含算法（structural subsumption algorithms）进行推理，该类算法对某些描述逻辑是合理和完备的。对包含析取、取非、存在限制等算子的描述逻辑的推理则一般求助于tableaux方法。我国研究人员古华茂提出了一种ALCN概念可满足性判定的完全析取范式（CDNF）算法，该算法比Tableau算法能节省线性甚至指数倍于输入概念描述长度的空间代价sup[29]。叶育鑫在tableaux基础上，通过引入回跳和布尔约束传播优化技术，提出一种SHOIQ（D）的本体一致性检测算法以提高算法推理效率sup[153]。牛悦则提出了一种模块提取方法，该方法通过分析符号解释域的边界与公理之间的关系计算出基于边界的模块，减少推理的搜索空间，使用边界模块进行推理后，推理性能显著提高sup[83]。张健和徐贵红利用描述逻辑公式与一阶谓词逻辑公式的对应关系，借助一阶逻辑公式的有限模型查找工具和自动定理证明器，在描述逻辑的推理技术上另辟蹊径，以解决描述逻辑工具的某些不足sup[145]。