The problem of choosing the inference rule to employ |
| |
Authors: | Larry Wos |
| |
Affiliation: | (1) Argonne National Laboratory, 9700 South Cass Ave., 60439-4844 Argonne, IL, USA |
| |
Abstract: | This article is the second of a series of articles discussing various open research problems in automated reasoning. The problem proposed for research focuses on finding criteria or metarules for choosing the inference rule(s) to be employed by the automated reasoning program in use when instructing the program to complete a specific assignment. We include actual experiments that illustrate the difficulty of making an appropriate choice.This work was supported by the Applied Mathematical Sciences subprogram of the Office of Energy Research, U.S. Department of Energy, under contract W-31-109-Eng-38. |
| |
Keywords: | Automated reasoning automated reasoning programs commutator theorem inference rules ITP SAM's Lemma unsolved research problem |
本文献已被 SpringerLink 等数据库收录! |
|