The problem of choosing the type of subsumption to use
Tóm tắt
This article is the eighteenth of a series of articles discussing various open research problems in automated reasoning. The problem proposed for research asks one to find criteria for choosing the type of subsumption (if any) to use for completing a specific assignment. Since subsumption can be expensive (in terms of computer time), the application of such criteria to select the most effective variant of subsumption for attacking a specific problem might materially affect the liklihood of success. As possible test problems for evaluating a proposed solution to this research problem, we suggest SAM's lemma, theorems from Tarskian geometry, and theorems from equivalential calculus.
Từ khóa
Tài liệu tham khảo
Guard, J., Oglesby, F., Bennett, J., and Settle, L., ‘Semi-automated mathematics’, J. ACM 16, 49–62, (1969).
Lusk, E., and Overbeek, R., The Automated Reasoning System ITP, Technical Report ANL-84-27, Argonne National Laboratory (April 1984).
Lusk, E., and Overbeek, R., Logic Machine Architecture Inference Mechanisms—Layer 2 User Reference Manual Release 2.0, Technical Report ANL-82-84, Rev. 1, Argonne National Laboratory (April 1984).
McCune, W., OTTER 2.0 Users Guide, Technical Report ANL-90/9, Argonne National Laboratory (1990).
McCune, W., ‘Experiments with discrimination tree indexing and path indexing for term retrieval’, MSC Preprint P191-1190, Mathematics and Computer Science Division, Argonne National Laboratory, 1990 (to appear in J. Automated Reasoning).
Overbeek, R., ‘An implementation of hyper-resolution’, Computational Mathematics with Applications 1, 201–214 (1975).
Quaife, A. ‘Automated development of Tarski's geometry’, J. Automated Reasoning 5, 97–118 (1989).
Robinson, J., ‘A machine-oriented logic based on the resolution principle’, J. ACM 12, 23–41 (1965).
Robinson, J., ‘Automatic deduction with hyper-resolution’, Internat. J. Computer Mathematics 1, 227–234 (1965).
Tarski, A., ‘What is elementary geometry?’, in L. Henkin, P. Suppes and A. Tarski (eds) The Axiomatic Method, with Special Reference to Geometry and Physics, North-Holland, Amsterdam (1959), pp. 16–29.
Wos, L., Automated Reasoning: 33 Basic Research Problems, Prentice-Hall, Englewood Cliffs, New Jersey (1987).
Wos, L., Overbeek, R., and Lusk, E., ‘Subsumption, a sometimes undervalued procedure’, Preprint P93-0789, Mathematics and Computer Science Division, Argonne National Laboratory, 1989 (to appear in Festschrift for J. A. Robinson, ed. J.-L. Lassez).
Wos, L., Overbeek, R., Lusk, E., and Boyle, J., Automated Reasoning: Introduction and Applications Prentice-Hall, Englewood Cliffs, New Jersey (1984).
Wos, L., Winker, S., Veroff, R., Smith, B., and Henschen, L., ‘A new use of an automated reasoning assistant: Open questions in equivalential calculus and the study of infinite domains’, Artificial Intelligence 22, 303–356 (1984).