Q0 (mathematical logic)
id:
q0-mathematical-logic-294-16276085
title:
Q0 (mathematical logic)
text:
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
are based on Q0. In August 2009, TPS won the first-ever competition
among higher-order theorem proving systems.
brand slug:
wiki
category slug:
encyclopedia
description:
original url:
https://en.wikipedia.org/wiki/Q0_(mathematical_logic)
date created:
date modified:
2023-10-25T18:33:25Z
main entity:
{"identifier":"Q7265672","url":"https://www.wikidata.org/entity/Q7265672"}
image:
fields total:
13
integrity:
13