About: MINLOG     Goto   Sponge   NotDistinct   Permalink

An Entity of Type : yago:WikicatProofAssistants, within Data Space : dbpedia.org associated with source document(s)
QRcode icon
http://dbpedia.org/c/57333mmqAY

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

AttributesValues
rdf:type
rdfs:label
  • MINLOG (en)
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)
dct:subject
Wikipage page ID
Wikipage revision ID
Link from a Wikipage to another Wikipage
Link from a Wikipage to an external page
sameAs
has 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)
gold:hypernym
prov:wasDerivedFrom
page length (characters) of wiki page
foaf:isPrimaryTopicOf
is Link from a Wikipage to another Wikipage of
is foaf:primaryTopic of
Faceted Search & Find service v1.17_git147 as of Sep 06 2024


Alternative Linked Data Documents: ODE     Content Formats:   [cxml] [csv]     RDF   [text] [turtle] [ld+json] [rdf+json] [rdf+xml]     ODATA   [atom+xml] [odata+json]     Microdata   [microdata+json] [html]    About   
This material is Open Knowledge   W3C Semantic Web Technology [RDF Data] Valid XHTML + RDFa
OpenLink Virtuoso version 08.03.3331 as of Sep 2 2024, on Linux (x86_64-generic-linux-glibc212), Single-Server Edition (378 GB total memory, 69 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software