实验室建立了原创的基于矛盾体分离的动态自动演绎推理理论与方法，从本质上突破性地发展了基于逻辑的自动推理理论与方法，其成果具国际领先水平。
基于原创的自动推理理论与方法，实验室研发了一系列命题逻辑问题求解系统，已解决来源于应用领域的 19 亿多个实际问题，规模最大的相当于 3.13 万亿个元器件组成的逻辑电路。在基准问题求解数量、求解时间等多方面已超过该 领域国际最高水平竞赛 SAT Competition 2016 Main Track 的冠军得主 MapleCOMSPS，且所研发的求解器已有效应用于 C 程序和 PLC 程序的自动验证，为保障多个重要领域的复杂系统的可信运行起到了不可替代的作用。
基于原创的自动推理理论与方法，实验室设计了一系列一阶逻辑自动推理系统（证明器），已验证来自于程序验证、集成电路验证、安全协议、数学等实际领域的结论 25 万余个，解决了一些国际上著名证明器（包括英国剑桥大学 Isabelle、德国慕尼黑工业大学 E、英国曼彻斯特大学 Vampire、美国阿尔贡国家实验室 Prover9 等）还未解决的问题，并与国际知名证明器结合证明了 99 个最难（国际上没证明器能够解决的）问题；未发现国内其它基于逻辑的动态自动演绎推理系统。
