Research on Automated Deduction

自动推演研究

• 批准号: 9408630
• 负责人: Mark Stickel
• 金额: $ 15.29万
• 依托单位: SRI International
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 1995
• 资助国家: 美国
• 起止时间: 1995-08-01 至 1997-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9408630&HistoricalAwards=false
• 关键词: Research; Automated; Deduction

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.

模型消元定理证明过程与自上而下推理过程一样，都存在重复求解相同目标的缺陷。这个问题可以通过引理或缓存来改善，但是要研究的倒置元解释方法提供了一个更全面的解决方案，需要由自下而上的推理引擎执行模型消除过程，这也允许对搜索策略进行更多的控制。理论归结是将理论结合到归结定理证明程序中的框架，从而不需要直接根据理论的公理进行归结，从而提高了效率。尽管将理论合并到归结定理证明器中的许多方法可以被视为理论归结的实例，但理论归结对如何合并理论几乎没有提供指导。部分理论归结中的谓词和函数匹配规则和残基的多边表示正在开发中，作为使用理论归结的方法论。最近，自动推理系统，如Davis-Putnam过程的有效实现，解决了拟群理论中许多以前未解决的问题。在与其他自动演绎研究人员和该领域的一位数学家专家的合作下，将致力于在拟群理论方面获得新的结果。