dmtcs:3469 -
Discrete Mathematics & Theoretical Computer Science,
January 1, 2005,
DMTCS Proceedings vol. AF, Computational Logic and Applications (CLA '05)
-
https://doi.org/10.46298/dmtcs.3469
Classical Combinatory LogicArticle
Authors: Karim Nour 1
0000-0003-1943-272X
Karim Nour
1 Laboratoire de Mathématiques
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 "à la Hilbert''. We present in this paper a combinatory logic which corresponds to propositional classical logic. This system is equivalent to the system $λ ^{Sym}_{Prop}$ of Barbanera and Berardi.
Roman Kuznets, Lecture notes in computer science, Proof Identity for Classical Logic: Generalizing to Normality, pp. 332-348, 2007, 10.1007/978-3-540-72734-7_24.