Implementing the `Fool's model' of combinatory logic

DOI10.1007/BF01880331zbMath0749.03007OpenAlexW2095025636MaRDI QIDQ1181718

Robert K. Meyer, Lawrence Powers, Martin W. Bunder

Publication date: 27 June 1992

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

Full work available at URL: https://doi.org/10.1007/bf01880331

zbMATH Keywords

theorem provingimplementationcombinatory logicFool's modelsimplicational calculus

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Combinatory logic and lambda calculus (03B40)

Related Items (4)

Ternary relations and relevant semantics ⋮ A (machine-oriented) logic based on pattern matching ⋮ 2002 Annual Conference of the Australasian Association for Logic ⋮ Principal types of BCK-lambda-terms

Cites Work

• Linear logic
• Condensed detachment as a rule of inference
• The semantics of entailment. III
• In memoriam Carew Arthur Meredith (1904-1976)
• New axiomatics for relevant logics. I
• A new type assignment for λ-terms
• A filter lambda model and the completeness of type assignment
• Principal type-schemes and condensed detachment
• The undecidability of entailment and relevant implication
• A Machine-Oriented Logic Based on the Resolution Principle
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Implementing the `Fool's model' of combinatory logic