Research on Automated Deduction

模型消去定理证明过程与自顶向下推理过程一样，存在重复求解相同目标的缺陷。这个问题可以通过引理或缓存来改善，但是要研究的“颠倒元解释”方法提供了一个更全面的解决方案，该解决方案需要通过自下而上的推理引擎执行模型消除过程，这也允许对搜索策略进行更多的控制。理论解析是一种将理论纳入解析定理证明程序的框架，使其不必直接求解理论的公理，从而提高效率。虽然许多将理论整合到解决定理证明器中的方法可以被视为理论解决的实例，但理论解决对如何整合理论提供的指导很少。在部分理论解析中，谓词和函数匹配规则以及残数的多边表示被开发为使用理论解析的方法。许多以前在拟群理论中开放的问题最近已经被自动推理系统解决了，比如Davis-Putnam过程的有效实现。在与其他自动演绎研究人员和该领域的一位数学家专家的合作中，将投入额外的努力来获得准群理论的新结果。

The model elimination theorem-proving procedure, like top-down reasoning procedures, has the defect of repeatedly solving the same goals. The problem can be ameliorated by lemmas or caching, but the ``upside-down meta-interpretation'' approach to be investigated offers a more comprehensive solution that entails executing the model elimination procedure by a bottom-up reasoning engine, which also enables more control over search strategy. Theory resolution is a framework for incorporating theories into a resolution theorem-proving program, thereby making it unnecessary to resolve directly upon axioms of the theory and improving efficiency. Although many ways of incorporating theories into a resolution theorem prover can be seen as instances of theory resolution, theory resolution provides little guidance on how to incorporate theories. Predicate-and function-matching rules and a multilateral representation for residues in partial theory resolution are being developed as methodologies for using theory resolution. Numerous previously open problems in the theory of quasigroups have been solved recently by automated reasoning systems such as efficient implementations of the Davis-Putnam procedure. In collaboration with other automated deduction researchers and a mathematician expert on the domain, additional effort will be devoted to obtain new results in the theory of quasigroups.