Research on 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.