Abstract
Barendregt defines combinatory logic as an equational system satisfying the combinatorsS andK with ((Sx)y)z=(xz)(yz) and (Kx)y=x; the set consisting ofS andK provides abasis for all of combinatory logic. Rather than studying all of the logic, logicians often focus onfragments of the logic, subsets whose basis is obtained by replacingS orK or both by other combinators. In this article, we present a powerful new strategy, called thekernel strategy, for studying fragments in the context of questions concerned with fixed point properties. Interest in such properties rests in part with their relation to normal forms and paradoxes. We show how the kernel strategy was used to answer a number of open questions, offering abundant evidence that the availability of the kernel strategy marks a singular advance for automated reasoning. In all of our experiments with this strategy applied by an automated reasoning program, the rate of success has been impressively high and the CPU time to obtain the desired information startlingly small. For each fragment we study, we use the kernel strategy to attempt to determine whether the strong or the weak fixed point property holds. WhereA is a given fragment with basisB, the strong fixed point property holds forA if and only if there exists a combinatory such that, for all combinatorsx,yx=x(yx), wherey is expressed purely in terms of elements ofB. The weak fixed point property holds forA if and only if for all combinatorsx there exists a combinatory such thaty=xy, wherey is expressed purely in terms of the elements ofB and the combinatorx. Because the use of the kernel strategy is so effective in addressing questions focusing on either fixed point property, its formulation marks an important advance for combinatory logic. Perhaps of especial interest to logicians is an infinite class of infinite sets of tightly coupled fixed point combinators (presented here), whose unexpected discovery resulted directly from the application of the strategy by an automated reasoning program. We also offer various open questions for possible research and focus on an automated reasoning program and input files that may prove useful for such research.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.References
Barendregt, H. P.,The Lambda Calculus: Its Syntax and Semantics, North-Holland, Amsterdam (1981).
Boyer, R., Lusk, E., McCune, W., Overbeek, R., Stickel, M., and Wos, L., ‘Set theory in first-order logic: Clauses for Gödel's axioms’,J. Automated Reasoning 2, 287–327 (1986).
Bundy, A., Personal correspondence (1988).
Curry, H. B., and Feys, R.,Combinatory Logic I, North-Holland, Amsterdam (1958).
Curry, H. B., Hindley, J. R., and Seldin, J. P.,Combinatory Logic II, North-Holland, Amsterdam (1972).
Hindley, J. R., and Seldin, J. P.,Introduction to Combinators and Lambda Calculus. Cambridge University Press, Cambridge (1986).
Jacopini, G., Personal correspondence (1989).
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).
McCune, W.,OTTER 2.0 Users Guide, Technical Report ANL-90/9, Argonne National Laboratory, Argonne, Illinois (1990).
McCune, W., Personal correspondence (1988).
McCune, W., and Wos, L., ‘The absence and the presence of fixed point combinators’,Theoretical Computer Science 87, 221–228 (1991).
McCune, W., and Wos, L., ‘A case study in automated theorem proving: Finding sages in combinatory logic’,J. Automated Reasoning 3(1), 91–108 (1987).
Piperno, A., Personal correspondence (1989).
Robinson, G., and Wos, L., ‘Paramodulation and theorem-proving in first-order theories with equality’, inMachine Intelligence 4 (eds. B. Meltzer and D. Michie), Edinburgh University Press, Edinburgh, pp. 135–150 (1969).
Smullyan, R., Personal correspondence (1987).
Smullyan, R.,To Mock a Mockingbird, Alfred A. Knopf, New York (1985).
Statman, R., Personal correspondence with Raymond Smullyan (1986).
Wos, L.,Automated Reasoning: 33 Basic Research Problems, Prentice-Hall, Englewood Cliffs, N.J. (1987).
Wos, L., and McCune, W. W.,Searching for Fixed Point Combinators by Using Automated Theorem Proving: A Preliminary Report. Technical Report ANL-88-10, Argonne National Laboratory, Argonne, Illinois (1988).
Wos, L., Overbeek, R., and Henschen, L., ‘Hyperparamodulation: a refinement of paramodulation’, inProceedings of the Fifth Conference on Automated Deduction. Lecture Notes in Computer Science, Vol. 87 (ed. R. Kowalski and W. Bibel), Springer-Verlag, New York, pp. 208–219 (1980).
Wos, L., Overbeek, R., Lusk, E., and Boyle, J.,Automated Reasoning: Introduction and Applications, 2nd ed., McGraw-Hill, New York (1992).
Wos, L., and Robinson, G., ‘Maximal models and refutation completeness: Semidecision procedures in automatic theorem proving’, inWorld Problems: Decision Problems and the Burnside Problem in Group Theory (eds. W. Boone, F. Cannonito, and R. Lyndon), North-Holland, New York, pp. 609–639 (1973).
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).
Wos, L., Robinson, G., Carson, D., and Shalla, L., ‘The concept of demodulation in theorem proving’,J. ACM 14, 698–709 (1967).
Zhang, J., Personal correspondence, Institute of Software, Academia Sinica (1992).
Author information
Authors and Affiliations
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
About this article
Cite this article
Wos, L. The kernel strategy and its use for the study of combinatory logic. J Autom Reasoning 10, 287–343 (1993). https://doi.org/10.1007/BF00881795
Received:
Issue Date:
DOI: https://doi.org/10.1007/BF00881795