Classical combinatory logic

zbMATH Open1193.03031arXiv0905.1100MaRDI QIDQ3576002FDOQ3576002

Authors: Karim Nour 

Publication date: 28 July 2010

Abstract: Combinatory logic shows that bound variables can be eliminated without loss of expressiveness. It has applications both in the foundations of mathematics and in the implementation of functional programming languages. The original combinatory calculus corresponds to minimal implicative logic written in a system "`a la Hilbert". We present in this paper a combinatory logic which corresponds to propositional classical logic. This system is equivalent to the system $lambd{a}_{Prop}^{Sym}$ of Barbanera and Berardi.

Full work available at URL: https://arxiv.org/abs/0905.1100

Recommendations

• scientific article; zbMATH DE number 823591
• scientific article; zbMATH DE number 2038177
• scientific article; zbMATH DE number 1302066
• Combinator logics
• scientific article; zbMATH DE number 993359

zbMATH Keywords

combinatory logiclambda-calculuspropositional classical logic

Mathematics Subject Classification ID

Classical propositional logic (03B05) Combinatory logic and lambda calculus (03B40) Functional programming and lambda calculus (68N18)

Cited In (6)

• Title not available (Why is that?)
• Classical logic as limit completion
• First-order logic without bound variables: compositional semantics
• Title not available (Why is that?)
• The Logic of Calculation
• Title not available (Why is that?)

This page was built for publication: Classical combinatory logic

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