Research in Automated Reasoning

几种使自动推理系统更加 有效的将被调查。 Prolog技术定理证明器（PTTP）已开发为 一个逻辑和搜索空间的Prolog完全扩展， 异常高的推理率，使其能够解决浅 证明定理的问题。 PTTP在一个 在传统归结定理证明器中， 探讨了 PTTP可用于实现理论解析或 链接推理原理程序，快速反驳检查 新派生子句、E-统一和排序推理。 一个Prolog类溯因推理系统已在 PTTP已被用于句子的语用处理， 文本理解系统。 更抽象的公式 PTTP的溯因推理方法将被开发和研究， 目标是提高系统的性能， 它能更好地选择哪种溯因解释是最好的。 Ohlbach的模态推理方法与 传统的解决定理证明，因为它转换模式 公式到带有额外世界路径参数的经典公式 表示模态前缀。 世界的特殊统一算法 依赖于模态可访问性关系的路径则为 采用 已经开发了这种方法的部分实现 并将进行完善和调查。 该方法承诺， 保留开发解决方案系统的投资，同时证明 模态逻辑中的定理 将制定一项分案解决规则。 对于非 霍恩问题与一些派生地面文字，它将结合联合收割机 决议程序的一般性和案件分割行为 Davis-Putnam过程在命题问题上的应用 问题

Several approaches to making automated reasoning systems more effective will be investigated. The Prolog Technology Theorem Prover (PTTP) has been developed as a logically and search-space complete extension of Prolog with an exceptionally high inference rate that permits it to solve shallow theorem-proving problems very rapidly. The use of PTTP in a subordinate role in conventional resolution theorem provers will be explored. PTTP can be used to implement the theory resolution or linked inference principle procedures, fast refutation checks for newly derived clauses, E-unification, and sort reasoning. A Prolog-like abductive reasoning system has been developed in PTTP and has been used for pragmatic processing of sentences in a system for text understanding. More abstract formulations of the PTTP's abductive reasoning method will be developed and studied with the objective of improving the performance of the system and enabling it to make better choices about which abductive explanation is best. Ohlbach's approach to modal reasoning is compatible with conventional resolution theorem provers, since it transforms modal formulas to classical formulas with extra world-path arguments that denote the modal prefix. Special unification algorithms for world paths, which depend on the modal accessibility relation, are then used. A partial implementation of this approach has been developed and will be refined and investigated. The approach promises to preserve the investment of developing resolution systems while proving theorems in modal logic. A case-splitting rule for resolution will be developed. For non- Horn problems with some derived ground literals, it will combine the generality of the resolution procedure and the case-splitting behavior and performance of the Davis-Putnam procedure on propositional problems.