A case study in automated theorem proving: Finding sages in combinatory logic

DOI10.1007/BF00381147zbMath0636.68121WikidataQ114267045 ScholiaQ114267045MaRDI QIDQ1098333

Larry Wos, William W. McCune

Publication date: 1987

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

zbMATH Keywords

automated reasoningautomated theorem provingdemodulationcombinatory logicbidirectional searchfixed-point propertyparamodulationproof checkingITP

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40)

Related Items (6)

The application of automated reasoning to questions in mathematics and logic ⋮ Evolving combinators ⋮ Larry Wos: visions of automated reasoning ⋮ The kernel strategy and its use for the study of combinatory logic ⋮ The absence and the presence of fixed point combinators ⋮ Automated proofs of equality problems in Overbeek's competition

Cites Work

• A new use of an automated reasoning assistant: Open questions in equivalential calculus an the study of infinite domains
• A foray into combinatory logic
• Unnamed Item

This page was built for publication: A case study in automated theorem proving: Finding sages in combinatory logic