A case study in automated theorem proving: Finding sages in combinatory logic
The paper presents an application of automated theorem proving to a study of a strong fixed-point property in a system with the B and W combinators. During the study, besides the one previously known solution (due to R. Statman), four new have been found. The paper contains a very detailed discussion of the uses of the two automated theorem proving programs, which assisted during the study. For related discussion, cf. also the following review.
scientific article; zbMATH DE number 4037274