Ett interaktivt verktyg för att bevisa teorem

Ett interaktivt teorembevisverktyg ( interactive theorem solver ) är programvara som hjälper forskaren att utveckla formella bevis . Bevis produceras i processen för interaktion mellan människa och maskin. Vanligtvis inkluderar sådan programvara någon form av interaktiv bevisredigerare eller annat gränssnitt genom vilket en person kan söka efter bevis lagrade på datorn, såväl som automatiska bevisverifieringsprocedurer som utförs av datorn.

Jämförelse av system

namn senaste versionen Utvecklare Implementeringsspråk Förmågor
högre ordningslogik Beroende typer liten kärna Bevisautomatisering Bevis genom eftertanke kodgenerering
ACL2 8.2 Matt Kaufmann och J Strother Moore Vanlig Lisp Inte oskrivet Inte Ja Ja [1] genererar körbar kod
Agda 2.6.0.1 Ulf Norell, Nils Anders Danielsson och Andreas Abel ( Chalmers tekniska högskola och Göteborgs universitet ) Haskell Ja Ja Ja Inte Delvis genererar körbar kod
Albatross 0,4 Helmut Brandl OCaml Ja Inte Ja Ja okänd inte implementerat ännu
Coq 8.11.0 INRIA OCaml Ja Ja Ja Ja Ja Ja
F* i förvaret Microsoft Research och INRIA F* Ja Ja Inte Ja Ja [2] Ja
HOL Light i förvaret John Harrison OCaml Ja Inte Ja Ja Inte Inte
HOL4 Kananaskis-12 (eller i förvaret) Michael Norrish, Konrad Slind och andra Standard ML Ja Inte Ja Ja Inte Ja
Isabelle 2019 Larry Paulson ( Cambridge ), Tobias Nipkow ( München ) och Makarius Wenzel StandardML , Scala Ja Inte Ja Ja Ja Ja
Mager v3.4.2 [3] Microsoft Research C++ Ja Ja Ja Ja Ja okänd
LEGO (ej ansluten till LEGO) 1.3.1 Randy Pollack ( Edinburgh ) Standard ML Ja Ja Ja Inte Inte Inte
Mizar 8.1.05 Bialystok universitet Gratis Pascal Delvis Ja Inte Inte Inte Inte
NuPRL 5 Cornell University Vanlig Lisp Ja Ja Ja Ja okänd Ja
PVS 6,0 SRI International Vanlig Lisp Ja Ja Inte Ja Inte okänd
Tolv 1.7.1 Frank Pfenning och Carsten Schürmann Standard ML Ja Ja okänd Inte Inte okänd

Användargränssnitt

Ett populärt gränssnitt för interaktiva teoremprovningsverktyg är den Emacs-baserade Proof General som utvecklats vid University of Edinburgh . Coq inkluderar CoqIDE som är skriven i OCaml/ Gtk . Isabelle inkluderar Isabelle/jEdit, som är baserat på jEdit och Isabelle/ Scalas ramverk för dokumentcentrerad bevisbehandling. För Visual Studio Code finns det också ett tillägg som är designat för att fungera med Isabelle. Det utvecklades av Makarius Wenzel [5] .

Se även

Anteckningar

  1. ↑ Hunt, Warren; Matt Kaufman; Robert Bellarmine Krug; J Moore; Erik W. Smith. Meta Reasoning in ACL2  //  Springer Lecture Notes in Computer Science : journal. - 2005. - Vol. 3603 . - S. 163-178 .
  2. ↑ Sök efter "bevis genom reflektion": arXiv : 1803.06547
  3. ↑ Sidan för utgivningar av magert teoremprover . GitHub . Arkiverad från originalet den 5 september 2020.
  4. ↑ Farmer, William M.; Guttman, Joshua D.; Thayer, F. Javier. IMPS: Ett interaktivt matematiskt bevissystem  //  Journal of Automated Reasoning. - 1993. - Vol. 11 , nr. 2 . - S. 213-248 . - doi : 10.1007/BF00881906 .
  5. ↑ Wenzel, Makarius Isabelle . Hämtad 31 maj 2020. Arkiverad från originalet 4 juni 2020.

Litteratur

Länkar

Kataloger