Combinatory abstraction using B, B^ and friends

DOI10.1016/0304-3975(94)90114-7MaRDI QIDQ1346635zbMATH OpenOpenAlexFDO

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

Recommendations

• Abstraction problems in combinatory logic: A compositive approach
• scientific article; zbMATH DE number 4035776
• Compact bracket abstraction in combinatory logic
• The systematic construction of a one-combinator basis for lambda-terms
• On combinatory complete sets of proper combinators

Cites work

• scientific article; zbMATH DE number 3916223 (Why is no real title available?)
• scientific article; zbMATH DE number 3504935 (Why is no real title available?)
• scientific article; zbMATH DE number 3993540 (Why is no real title available?)
• scientific article; zbMATH DE number 3280068 (Why is no real title available?)
• A system of formal logic without an analogue to the curry W operator
• Algebraizable logics
• Notes on the axiomatics of the propositional calculus
• Solution to the P − W problem
• Standard and Normal Reductions

Cited in

(11)

• On principal types of combinators
• scientific article; zbMATH DE number 4127172 (Why is no real title available?)
• scientific article; zbMATH DE number 4085616 (Why is no real title available?)
• A lambda proof of the P-W theorem
• The systematic construction of a one-combinator basis for lambda-terms
• Extracting \(\mathsf{BB'IW}\) inhabitants of simple types from proofs in the sequent calculus \(LT_\to^t\) for implicational ticket entailment
• On repetitive right application of \(B\)-terms
• The proofs of α → α in P – W
• Ticket Entailment is decidable
• The decidability of a fragment of \(\text{BB}'\text{IW}\)-logic
• Lambda terms definable as combinators

This page was built for publication: Combinatory abstraction using \({\mathbf B}\), \({\mathbf B}^ \prime\) and friends

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