DMTCS Proceedings, Computational Logic and Applications, CLA '05

Font Size:  Small  Medium  Large

Classical Combinatory Logic

Karim Nour


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 2;SymProp of Barbanera and Berardi.

Full Text: GZIP Compressed PostScript PostScript PDF original HTML abstract page

Valid XHTML 1.0 Transitional