Combinatory logic is a formal system, equivalent to λ calculus, that can express functions without the use of formal variables. Every term is a function and there is just one binary operation, application.

Combinatory Terms

Application () — left-associative functional application

CombinatorK, CombinatorS — fundamental combinators

CombinatorB  ▪  CombinatorC  ▪  CombinatorI  ▪  CombinatorW  ▪  CombinatorY

Construct — Wolfram Language application

Function — abstraction in λ calculus

Groupings  ▪  FixedPoint

Automated Theorem Proving »

FindEquationalProof — generate representations of proofs in combinatory logic

ProofObject  ▪  AxiomaticTheory