Implementing the `Fool's model' of combinatory logic

DOI10.1007/BF01880331zbMATH Open0749.03007OpenAlexW2095025636MaRDI QIDQ1181718FDOQ1181718

Authors: 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

Recommendations

• A foray into combinatory logic
• scientific article; zbMATH DE number 3916223
• Systems of illative combinatory logic complete for first-order propositional and predicate calculus
• Completeness of two systems of illative combinatory logic for first-order propositional and predicate calculus

zbMATH Keywords

combinatory logicimplementationtheorem provingFool's modelsimplicational calculus

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (5)

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

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1181718)