Research in Automated Reasoning

将研究几种使自动推理系统更有效的方法。Prolog技术定理证明器（PTTP）是Prolog的逻辑和搜索空间的完全扩展，具有极高的推理率，可以非常快速地解决浅层定理证明问题。我们将探讨PTTP在传统分辨定理证明中的从属作用。PTTP可用于实现理论解析或关联推理原则程序，对新衍生子句的快速驳斥检查，e -统一和排序推理。在PTTP中开发了一个类似prolog的溯因推理系统，并将其用于文本理解系统中句子的语用处理。将开发和研究PTTP溯因推理方法的更抽象的公式，目的是提高系统的性能，使其能够更好地选择哪种溯因解释是最好的。Ohlbach的模态推理方法与传统的分辨定理证明是兼容的，因为它将模态公式转换为带有额外世界路径参数的经典公式，这些参数表示模态前缀。然后使用了基于模态可达性关系的世界路径统一算法。这一方法的部分实施已经制定，并将加以改进和调查。该方法保证了在模态逻辑中证明定理的同时节省开发解析系统的投资。将制定分案解决规则。对于非Horn问题，它将结合解决过程的通用性和命题问题上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.