A case study in automated theorem proving: Finding sages in combinatory logic
type: Item
instance of: scholarly article
title: A case study in automated theorem proving: Finding sages in combinatory logic
zbMATH Open document ID: 0636.68121
DOI: 10.1007/BF00381147
author: Larry Wos
author: William McCune
published in: Journal of Automated Reasoning
publication date: 1987-01-01T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 03B40
Mathematics Subject Classification ID: 03B35
zbMATH DE Number: 4037274
zbMATH Keywords: automated reasoning
zbMATH Keywords: paramodulation
zbMATH Keywords: demodulation
zbMATH Keywords: proof checking
zbMATH Keywords: bidirectional search
zbMATH Keywords: combinatory logic
zbMATH Keywords: ITP
zbMATH Keywords: automated theorem proving
zbMATH Keywords: fixed-point property
Wikidata QID: Q114267045
reviewed by: Jiří Zlatuška
MaRDI profile type: Publication
cites work: A foray into combinatory logic
cites work: Q3829089
cites work: A new use of an automated reasoning assistant: Open questions in equivalential calculus an the study of infinite domains
Recommended article: Erratum to ``A case study in automated theorem proving: finding sages in combinatory logic''
Recommended article: Automated theorem proving and logic programming: a natural symbiosis
Recommended article: Q4732137
Recommended article: Q3490992
Recommended article: Automatic theorem proving in paraconsistent logics: Theory and implementation
Recommended article: Q3216155
Recommended article: Q4380155
Recommended article: Q4247684
Recommended article: Automated theorem proving by resolution in non-classical logics
Recommended article: Computer-Assisted Proofs in Analysis and Programming in Logic: A case Study
description: scientific article; zbMATH DE number 4037274