Springer Nature is making Coronavirus research free. View research | View latest news | Sign up for updates

The problem of guaranteeing the existence of a complete set of reductions

  • 17 Accesses

Abstract

This article is the eleventh of a series of articles discussing various open research problems in automated reasoning. Here we focus on finding criteria for guaranteeing the existence of a complete set of reductions. We include a suggestion for evaluating a proposed solution to this research problem.

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

References

  1. 1.

    Buchberger, B., ‘Basic features and development of the critical-pair/completion procedure’, in Proceedings of the First International Conference on Rewriting Techniques and Applications, Springer-Verlag Lecture Notes in Computer Science, Vol. 202, ed. J.-P. Jouannaud, Springer-Verlag, New York (1985).

  2. 2.

    Dershowitz, N., ‘Termination’, in Proceedings of the First International Conference on Rewriting Techniques and Applications, Springer-Verlag Lecture Notes in Computer Science, Vol. 202, ed. J.-P. Jouannaud, Springer-Verlag, New York (1985).

  3. 3.

    Grau, A., ‘Ternary Boolean algebra’, Bulletin of the American Mathematical Society 53, 567–572 (1947).

  4. 4.

    Huet, G. and Oppen, D., ‘Equations and rewrite rules: A survey’, pp. 349–405 in Formal Language Theory, Perspectives and Open Problems, ed. R. V. Book, Academic Press, New York (1978).

  5. 5.

    Knuth, D. and Bendix, P., ‘Simple word problems in universal algebras’, pp. 263–297 in Computational Problems in Abstract Algebra, ed. J. Leech, Pergamon Press, New York (1970).

  6. 6.

    Robinson, G. and Wos, L., ‘Paramodulation and theorem-proving in first-order theories with equality’, pp. 135–150 in Machine Intelligence 4, ed. B. Meltzer and D. Michie, Edinburgh University Press, Edinburgh (1969).

  7. 7.

    Winker, S., ‘Generation and verification of finite models and counterexamples using an automated theorem prover answering two open questions’, Journal of the ACM 29, 273–284 (1982).

  8. 8.

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

  9. 9.

    Wos, L., Overbeek, R., Lusk, E., and Boyle, J., Automated Reasoning: Introduction and Applications, Prentice-Hall, Englewood Cliffs, New Jersey (1984).

  10. 10.

    Wos, L. and Robinson, G., ‘Maximal models and refutation completeness: Semidecision procedures in automatic theorem proving’, pp. 609–639 in Word Problems: Decision Problems and the Burnside Problem in Group Theory, ed. W. Boone, F. Cannonito, and R. Lyndon, North-Holland, New York (1973).

  11. 11.

    Wos, L., Robinson, G., Carson, D., and Shalla, L., ‘The concept of demodulation in theorem proving’, Journal of the ACM, 14, 698–709 (1967).

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 guaranteeing the existence of a complete set of reductions. J Autom Reasoning 5, 399–401 (1989). https://doi.org/10.1007/BF00248325

Download citation

Key words

  • Automated reasoning
  • complete set of reductions
  • demodulators
  • unsolved research problem