Q0 (mathematical logic) (original) (raw)

Q0 is Peter Andrews' formulation of the simply-typed lambda calculus,and provides a foundation for mathematics comparable to first-order logic plus set theory.It is a form of higher-order logic and closely related to the logics of the HOL theorem prover family. The theorem proving systems TPS and ETPSare based on Q0. In August 2009, TPS won the first-ever competitionamong higher-order theorem proving systems.