Implementing the `Fool's model' of combinatory logic

DOI10.1007/BF01880331zbMath0749.03007MaRDI QIDQ1181718

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

Publication date: 27 June 1992

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

zbMATH Keywords

theorem proving; implementation; combinatory logic; Fool's models; implicational calculus

Mathematics Subject Classification ID

03B35: Mechanization of proofs and logical operations

03B47: Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics)

03B40: Combinatory logic and lambda calculus

Related Items

2002 Annual Conference of the Australasian Association for Logic, Ternary relations and relevant semantics, Principal types of BCK-lambda-terms

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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