Implementing the `Fool's model' of combinatory logic (Q1181718): Difference between revisions
From MaRDI portal
Removed claims |
Set OpenAlex properties. |
||
(3 intermediate revisions by 3 users not shown) | |||
Property / author | |||
Property / author: Martin W. Bunder / rank | |||
Normal rank | |||
Property / reviewed by | |||
Property / reviewed by: Hans Jürgen Ohlbach / rank | |||
Normal rank | |||
Property / MaRDI profile type | |||
Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: A filter lambda model and the completeness of type assignment / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3691634 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: A new type assignment for λ-terms / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q5547552 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Linear logic / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Principal type-schemes and condensed detachment / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4722037 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Condensed detachment as a rule of inference / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: In memoriam Carew Arthur Meredith (1904-1976) / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: New axiomatics for relevant logics. I / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4103076 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3469090 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3228599 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q5734410 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: A Machine-Oriented Logic Based on the Resolution Principle / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3864488 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: The semantics of entailment. III / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4732137 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: The undecidability of entailment and relevant implication / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3829089 / rank | |||
Normal rank | |||
Property / full work available at URL | |||
Property / full work available at URL: https://doi.org/10.1007/bf01880331 / rank | |||
Normal rank | |||
Property / OpenAlex ID | |||
Property / OpenAlex ID: W2095025636 / rank | |||
Normal rank |
Latest revision as of 11:28, 30 July 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Implementing the `Fool's model' of combinatory logic |
scientific article |
Statements
Implementing the `Fool's model' of combinatory logic (English)
0 references
27 June 1992
0 references
The paper studies `Fool's models' of combinatory logic. A `fool's model' is a family of sets of propositional formulas, built with the implication symbol only, which is closed under condensed detachment of implicational calculus. Alternatively, it is a model of combinatory logic in set theory. `Fool's models' allow the investigation of properties of combinators. On the other hand, the correlation between implicational calculus and combinatory logic via the `fool's models' permits the application of methods of combinatory logic to theorem proving in implicational calculus. As a technical result, it is shown that the pure implicational calculus \(T\to\) consisting of the combinators \(B\), \(B'\), \(I\) and \(W\) is complete in the sense that all theorems can be generated by straightforward resolution with the condensed detachment rule. Furthermore, \(R\to\) is minimal among the systems with this property. An implementation of the `fool's model' ideas is presented in the last section. Some suggestions for exploiting it to do theorem proving in the implicational calculus are made.
0 references
Fool's models
0 references
combinatory logic
0 references
implicational calculus
0 references
theorem proving
0 references
implementation
0 references