The problem of guaranteeing the absence of a complete set of reductions
Tóm tắt
This article is the twelfth of a series of articles discussing various open research problems in automated reasoning. Here we focus on finding criteria for guaranteeing the absence of a complete set of reductions. We include a suggestion for evaluating a proposed solution to this research problem.
Tài liệu tham khảo
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).
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).
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., Robinson, G., Carson, D., and Shalla, L., ‘The concept of demodulation in theorem proving’, Journal of the ACM 14, 698–709 (1967).