About: Q0 (mathematical logic)

An Entity of Type: Thing, from Named Graph: http://dbpedia.org, within Data Space: dbpedia.org

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.

Property	Value
dbo:abstract	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. (en)
dbo:wikiPageExternalLink	http://plato.stanford.edu/entries/type-theory-church/ http://www.owlofminerva.net/files/fom.pdf http://plato.stanford.edu/entries/type-theory-church/%23ForBasEqu http://gtps.math.cmu.edu/tps.html https://web.archive.org/web/20100224074552/http:/www.springer.com/mathematics/book/978-1-4020-0763-7 https://web.archive.org/web/20190112232531/https:/pdfs.semanticscholar.org/28bf/123690205ae5bbd9f8c84b1330025e8476e4.pdf https://pdfs.semanticscholar.org/28bf/123690205ae5bbd9f8c84b1330025e8476e4.pdf
dbo:wikiPageID	30698100 (xsd:integer)
dbo:wikiPageLength	8698 (xsd:nonNegativeInteger)
dbo:wikiPageRevisionID	1104137960 (xsd:integer)
dbo:wikiPageWikiLink	dbr:Peter_B._Andrews dbr:Conservative_extension dbr:Simply_typed_lambda_calculus dbc:Logic_in_computer_science dbr:Higher-order_logic dbr:HOL_theorem_prover dbr:Kluwer_Academic_Publishers dbr:Doi:10.4444/100.111
dbp:wikiPageUsesTemplate	dbt:= dbt:Cite_book dbt:Cite_journal dbt:Math dbt:Reflist dbt:Harvnb
dcterms:subject	dbc:Logic_in_computer_science
rdfs:comment	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. (en)
rdfs:label	Q0 (mathematical logic) (en)
owl:sameAs	wikidata:Q0 (mathematical logic) https://global.dbpedia.org/id/4typd
prov:wasDerivedFrom	wikipedia-en:Q0_(mathematical_logic)?oldid=1104137960&ns=0
foaf:isPrimaryTopicOf	wikipedia-en:Q0_(mathematical_logic)
is dbo:wikiPageRedirects of	dbr:Q_zero dbr:Q0_(Mathematical_Logic) dbr:Q0_logic dbr:Q0_Logic
is dbo:wikiPageWikiLink of	dbr:Q_zero dbr:Q0_(Mathematical_Logic) dbr:Q0_logic dbr:Peter_B._Andrews dbr:Q0_Logic
is foaf:primaryTopic of	wikipedia-en:Q0_(mathematical_logic)