Q0 (mathematical logic)

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 ETPS Archived 2011-04-11 at the Wayback Machine are based on Q0. In August 2009, TPS won the first-ever competition among higher-order theorem proving systems.

This article is issued from Wikipedia. The text is available under Creative Commons Attribution-Share Alike 4.0 unless otherwise noted. Additional terms may apply for the media files.