Lambda the Ultimate

Predicate calculus is an indispensable tool for program verification. Therefore any program verifier has to be able to reason with quantified expressions, i.e. universally and existentially quantified expressions.

The proof engine of Modern Eiffel is able to perform such reasoning. The following article
"Quantified Expressions and Predicate Calculus" describes the way in which Modern Eiffel's proof engine handles quantified expressions.

The previous articles Introduction to the proof engine and Proofs by contradiction illustrate the basics of the proof engine.