Matches in DBpedia 2016-04 for { <http://dbpedia.org/resource/Automath> ?p ?o }
Showing triples 1 to 43 of
43
with 100 triples per page.
- Automath abstract "Automath (automating mathematics) was a formal language, devised by Nicolaas Govert de Bruijn starting in 1967, for expressing complete mathematical theories in such a way that an included automated proof checker can verify their correctness. The Automath system included many novel notions that were later adopted and/or reinvented in areas such as typed lambda calculus and explicit substitution. Dependent types is one outstanding example. Automath was also the first practical system that exploited the Curry–Howard correspondence. Propositions were represented as sets (called \"categories\") of their proofs, and the question of provability became a question of non-emptiness (type inhabitation); de Bruijn was unaware of Howard's work, and stated the correspondence independently.L.S. van Benthem Jutting, as part of this Ph.D. thesis in 1976, translated Edmund Landau's Foundations of Analysis into Automath and checked its correctness.Automath was never widely publicized at the time, however, and so never achieved widespread use; nonetheless, it proved very influential in the later development of logical frameworks and proof assistants. The Mizar system, a system of writing and checking formalized mathematics that is still in active use, was influenced by Automath.".
- Automath wikiPageExternalLink aut.
- Automath wikiPageExternalLink automath2002.
- Automath wikiPageExternalLink automath.
- Automath wikiPageID "8532185".
- Automath wikiPageLength "2361".
- Automath wikiPageOutDegree "15".
- Automath wikiPageRevisionID "685329231".
- Automath wikiPageWikiLink Automated_proof_checking.
- Automath wikiPageWikiLink Category:Proof_assistants.
- Automath wikiPageWikiLink Category:Type_theory.
- Automath wikiPageWikiLink Curry–Howard_correspondence.
- Automath wikiPageWikiLink Dependent_type.
- Automath wikiPageWikiLink Edmund_Landau.
- Automath wikiPageWikiLink Explicit_substitution.
- Automath wikiPageWikiLink Formal_language.
- Automath wikiPageWikiLink Logical_framework.
- Automath wikiPageWikiLink Mizar_system.
- Automath wikiPageWikiLink Nicolaas_Govert_de_Bruijn.
- Automath wikiPageWikiLink Proof_assistant.
- Automath wikiPageWikiLink QED_manifesto.
- Automath wikiPageWikiLink Type_inhabitation.
- Automath wikiPageWikiLink Typed_lambda_calculus.
- Automath wikiPageWikiLinkText "Automath".
- Automath wikiPageUsesTemplate Template:About.
- Automath wikiPageUsesTemplate Template:Formalmethods-stub.
- Automath wikiPageUsesTemplate Template:Reflist.
- Automath subject Category:Proof_assistants.
- Automath subject Category:Type_theory.
- Automath hypernym Language.
- Automath type Language.
- Automath type Assistant.
- Automath type Method.
- Automath type Redirect.
- Automath comment "Automath (automating mathematics) was a formal language, devised by Nicolaas Govert de Bruijn starting in 1967, for expressing complete mathematical theories in such a way that an included automated proof checker can verify their correctness. The Automath system included many novel notions that were later adopted and/or reinvented in areas such as typed lambda calculus and explicit substitution. Dependent types is one outstanding example.".
- Automath label "Automath".
- Automath sameAs Q2872609.
- Automath sameAs Automath.
- Automath sameAs Automath.
- Automath sameAs m.0276wnf.
- Automath sameAs Q2872609.
- Automath wasDerivedFrom Automath?oldid=685329231.
- Automath isPrimaryTopicOf Automath.