Nothing Special   »   [go: up one dir, main page]

About: MINLOG

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

MINLOG is a proof assistant developed at the University of Munich by the team of Helmut Schwichtenberg. MINLOG is based on first order natural deduction calculus. It is intended to reason about , using minimal rather than classical or intuitionistic logic. The primary motivation behind MINLOG is to exploit the proofs-as-programs paradigm for program development and program verification. Proofs are, in fact, treated as first-class objects, which can be normalized. If a formula is existential, then its proof can be used for reading off an instance of it or changed appropriately for program development by proof transformation. To this end, MINLOG is equipped with tools to extract functional programs directly from proof terms. This also applies to non-constructive proofs, using a refined . The

Property Value
dbo:abstract
  • MINLOG is a proof assistant developed at the University of Munich by the team of Helmut Schwichtenberg. MINLOG is based on first order natural deduction calculus. It is intended to reason about , using minimal rather than classical or intuitionistic logic. The primary motivation behind MINLOG is to exploit the proofs-as-programs paradigm for program development and program verification. Proofs are, in fact, treated as first-class objects, which can be normalized. If a formula is existential, then its proof can be used for reading off an instance of it or changed appropriately for program development by proof transformation. To this end, MINLOG is equipped with tools to extract functional programs directly from proof terms. This also applies to non-constructive proofs, using a refined . The system is supported by automatic proof search and normalization by evaluation as an efficient term rewriting device. (en)
dbo:wikiPageExternalLink
dbo:wikiPageID
  • 33078890 (xsd:integer)
dbo:wikiPageLength
  • 1175 (xsd:nonNegativeInteger)
dbo:wikiPageRevisionID
  • 1003761297 (xsd:integer)
dbo:wikiPageWikiLink
dct:subject
gold:hypernym
rdf:type
rdfs:comment
  • MINLOG is a proof assistant developed at the University of Munich by the team of Helmut Schwichtenberg. MINLOG is based on first order natural deduction calculus. It is intended to reason about , using minimal rather than classical or intuitionistic logic. The primary motivation behind MINLOG is to exploit the proofs-as-programs paradigm for program development and program verification. Proofs are, in fact, treated as first-class objects, which can be normalized. If a formula is existential, then its proof can be used for reading off an instance of it or changed appropriately for program development by proof transformation. To this end, MINLOG is equipped with tools to extract functional programs directly from proof terms. This also applies to non-constructive proofs, using a refined . The (en)
rdfs:label
  • MINLOG (en)
owl:sameAs
prov:wasDerivedFrom
foaf:isPrimaryTopicOf
is dbo:wikiPageWikiLink of
is foaf:primaryTopic of
Powered by OpenLink Virtuoso    This material is Open Knowledge     W3C Semantic Web Technology     This material is Open Knowledge    Valid XHTML + RDFa
This content was extracted from Wikipedia and is licensed under the Creative Commons Attribution-ShareAlike 3.0 Unported License