The kernel strategy and its use for the study of combinatory logic
type: Item
instance of: scholarly article
title: The kernel strategy and its use for the study of combinatory logic
zbMATH Open document ID: 0802.03010
DOI: 10.1007/BF00881795
author: Larry Wos
published in: Journal of Automated Reasoning
publication date: 1994-12-07T00:00:00Z
review text: The combinators \(S\) and \(K\) provide a basis for the study of all the combinatory logic. Fragments of this logic are usually studied instead, normally by replacing \(S\) and/or \(K\) by other combinators. Another strategy (the ``kernel strategy'') is proposed in this paper. It is very useful in studying questions concerned with fixed-point properties in relation to normal forms and paradoxes (applied in the context of an automated reasoning program). For each fragment studied, a kernel strategy (sound and complete) is used in attempt to determine whether the strong or the weak fixed-point property holds. ``To use the strategy, one selects a fragment of combinatory logic, a subset whose basis is obtained by replacing \(S\) and/or \(K\) by some set of combinators. If the first stage of the two-stage kernel strategy succeeds, then the fragment under study is proved to satisfy the weak fixed-point property and, further, to satisfy the reducible weak fixed-point property. The second stage of the strategy focuses on any successes of the first stage, each of which is called a kernel, and attempts to use the kernel to construct a fixed- point combinator. If the second stage succeeds, then the fragment is proved to satisfy the strong fixed-point property''. \textit{W. McCune} and the author's paper: ``The absence and the presence of fixed-point combinators'' [Theor. Comput. Sci. 87, No. 1, 221-228 (1991; Zbl 0731.03012)] may be consulted. Open problems are pointed out and direct applications for combinatory logic are emphasized.
Mathematics Subject Classification ID: 03B40
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 484768
zbMATH Keywords: combinatory logic
zbMATH Keywords: fixed-point properties
zbMATH Keywords: normal forms
zbMATH Keywords: paradoxes
zbMATH Keywords: automated reasoning
zbMATH Keywords: fragment
Wikidata QID: Q114267042
reviewed by: Cristian Masalagiu
describes a project that uses: OTTER
MaRDI profile type: Publication
cites work: The lambda calculus, its syntax and semantics
cites work: Set theory in first-order logic: Clauses for Gödel's axioms
cites work: Combinatory logic. Vol. II
cites work: Q4722037
cites work: Complexity and related enhancements for automated theorem-proving programs
cites work: The absence and the presence of fixed point combinators
cites work: A case study in automated theorem proving: Finding sages in combinatory logic
cites work: Q5624683
cites work: Q3994754
cites work: Erratum to ``A case study in automated theorem proving: finding sages in combinatory logic''
cites work: Q3883568
cites work: Q4296171
cites work: Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
cites work: The Concept of Demodulation in Theorem Proving
description: scientific article; zbMATH DE number 484768