Springer Nature is making SARS-CoV-2 and COVID-19 research free. View research | View latest news | Sign up for updates

The problem of finding a semantic strategy for focusing inference rules


This article is the fifteenth of a series of articles discussing various open research problems in automated reasoning. Here we focus on finding a strategy — other than a simple syntactic one — that can be used for focusing the attention of the inference rule(s) in use. The problem proposed for research asks one to find semantic criteria for selecting the clauses needed to complete the application of an inference rule. Suggestions for test problems are included. We note that Yuan Yu has solved two of these problems using a rather different approach with the Boyer-Moore theorem prover; his work is reported elsewhere in this issue of the Journal of Automated Reasoning.

This is a preview of subscription content, log in to check access.


  1. 1.

    Boyer, R. and Moore, J., A Computational Logic, Academic Press, New York (1979).

  2. 2.

    McCharon, J., Overbeek, R., and Wos, L., ‘Complexity and related enhancements for automated theorem-proving programs’, Computers and Mathematics with Applications 2, 1–16 (1976).

  3. 3.

    Wos, L., Automated Reasoning: 33 Basic Research Problems, Prentice-Hall, Englewood Cliffs, New Jersey (1987).

Download references

Author information

Additional information

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.

Rights and permissions

Reprints and Permissions

About this article

Cite this article

Wos, L. The problem of finding a semantic strategy for focusing inference rules. J Autom Reasoning 6, 337–339 (1990).

Download citation

Key words

  • Automated reasoning
  • semantic criteria
  • syntactic criteria
  • inference rules
  • unsolved research problem