Research in Automated Reasoning

点击翻译按钮获取中文摘要

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.