Combinatory abstraction using \({\mathbf B}\), \({\mathbf B}^ \prime\) and friends

DOI10.1016/0304-3975(94)90114-7zbMath0838.03012OpenAlexW2030827886MaRDI QIDQ1346635

Peter Trigg, J. Roger Hindley, Martin W. Bunder

Publication date: 6 April 1995

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(94)90114-7

zbMATH Keywords

deduction theoremabstraction algorithmcomplete basiscombinatory completenessabstractabilitycombinatory basispartial basis

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Related Items

Lambda terms definable as combinators ⋮ The decidability of a fragment of \(\text{BB}'\text{IW}\)-logic ⋮ The proofs of α → α in P – W ⋮ A lambda proof of the P-W theorem ⋮ Extracting \(\mathsf{BB'IW}\) inhabitants of simple types from proofs in the sequent calculus \(LT_\to^t\) for implicational ticket entailment ⋮ Ticket Entailment is decidable ⋮ On principal types of combinators

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Notes on the axiomatics of the propositional calculus
• Algebraizable logics
• Solution to the P − W problem
• Standard and Normal Reductions
• A system of formal logic without an analogue to the curry W operator