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.
Buy single article
Instant access to the full article PDF.
Price includes VAT for USA
Subscribe to journal
Immediate online access to all issues from 2019. Subscription will auto renew annually.
This is the net price. Taxes to be calculated in checkout.
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).
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).
Grau, A., ‘Ternary Boolean algebra’, Bulletin of the American Mathematical Society 53, 567–572 (1947).
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).
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).
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).
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).
Wos, L., Automated Reasoning: 33 Basic Research Problems, Prentice-Hall, Englewood Cliffs, New Jersey (1987).
Wos, L., Overbeek, R., Lusk, E., and Boyle, J., Automated Reasoning: Introduction and Applications, Prentice-Hall, Englewood Cliffs, New Jersey (1984).
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).
Wos, L., Robinson, G., Carson, D., and Shalla, L., ‘The concept of demodulation in theorem proving’, Journal of the ACM, 14, 698–709 (1967).
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.
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
- Automated reasoning
- complete set of reductions
- unsolved research problem