The problem of self-analytically choosing the set of support
Tóm tắt
This article is the seventh of a series of articles discussing various open research problems in automated reasoning. Here we focus on self-analysis and the set of support strategy. The problem proposed for research asks for one to find a means for an automated reasoning program to self-analytically determine which clauses to be in the set of support at various points during the program's attempt to complete a given assignment. For evaluating a proposed solution to this research problem, we include suggestions concerning possible test problems.
Tài liệu tham khảo
Gödel, K., The Consistency of the Axiom of Choice and of the Generalized Continuum-Hypothesis with the Axioms of Set Theory, Princeton University Press, Princeton (1940).
McCharen, J., Overbeek, R., and Wos, L., ‘Complexity and related enhancements for automated theorem-proving programs’, Computers and Mathematics with Applications 2, 1–16 (1976).
Robinson, J. ‘Automatic deduction with hyper-resolution’, International Journal of Computer Mathematics 1, 227–234 (1965).
Robinson, J., ‘A machine-oriented logic based on the resolution principle’, J. ACM 12, 23–41 (1965).
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., and Carson, D., ‘Efficiency and completeness of the set of support strategy in theorem proving’, J. ACM 12, 536–541 (1965).