The problem of reasoning from inequalities |
| |
Authors: | Larry Wos |
| |
Affiliation: | (1) Argonne National Laboratory, 9700 South Cass Ave., 60439-4801 Argonne, IL, USA |
| |
Abstract: | This article is the twenty-first of a series of articles discussing various open research problems in automated reasoning.
The problem proposed for research asks one to find an inference rule that performs as paramodulation does, but with the focus
on inequalities rather than on equalities. Since, too often, inequalities that are present in the input play a passive role
during a reasoning program's attempt to complete an assignment, such an inference rule would markedly add to program effectiveness
by giving inequalities the potential of playing a key role. For evaluating a proposed solution to this research problem, we
suggest as possible test problems theorems from group theory and theorems from ring theory.
This work was supported by the Applied Mathematical Sciences subprogram of the Office of Energy Research, U.S. Department
of Energy, under Contract W-13-109-Eng-38. |
| |
Keywords: | Automated reasoning inequalities paramodulation unsolved research problem |
本文献已被 SpringerLink 等数据库收录! |
|