Can lambda-calculus be used for knowledge representation?
The &lambda;-calculus was invented to be a logic and foundation of  mathematics (1-4). The most well-known logic to use &lambda;-calculus for formulae (as opposed to proofs in the Curry-Howard approach) is HOL (= Higher-Order Logic). The most well-developed implementation of HOL is Isabelle/HOL (5). To the extent that you believe logic can represent knowledge, you can use HOL to do that, hence &lambda;-calculus.

There is a third approach to using &lambda;-calculus as logic: higher-order Prolog (aka &lambda;Prolog) (6), which -- like Prolog -- is based proof search, but in HOL.

The relationship between the three approaches (HOL, Curry-Howard and &lambda;Prolog) is not well-understood.




1. A. Church, A Formulation of the Simple Theory of Types.



2. P. B. Andrews, Churchs Type Theory.



3. F. Cardone, J. R. Hindley, History of Lambda-calculus and Combinatory Logic.



4. J. B. Rosser, Highlights of the history of the lambda-calculus.



5. T. Nipkow L. C. Paulson, M. Wenzel, A Proof Assistant for Higher-Order Logic.



6. D. Miller, G. Nadathur, P. Pfenning, A. Scedrov, Uniform Proofs As A Foundation For Logic Programming.