Et interaktivt teorembevisværktøj

Et interaktivt teorembevisværktøj ( interactive theorem solver ) er software , der hjælper forskeren med at udvikle formelle beviser . Beviser produceres i processen med menneske-maskine-interaktion. Typisk inkluderer sådan software en form for interaktiv beviseditor eller anden grænseflade, hvorigennem en person kan søge efter beviser, der er gemt på computeren, såvel som automatiserede bevisverifikationsprocedurer udført af computeren.

Sammenligning af systemer

Navn nyeste version Udvikler(e) Implementeringssprog Evner
højere ordens logik Afhængige typer lille kerne Evidensautomatisering Bevis ved refleksion kodegenerering
ACL2 8.2 Matt Kaufmann og J Strother Moore Almindelig Lisp Ikke uskrevet Ikke Ja Ja [1] genererer eksekverbar kode
Agda 2.6.0.1 Ulf Norell, Nils Anders Danielsson og Andreas Abel ( Chalmers Tekniske Universitet og Göteborgs Universitet ) Haskell Ja Ja Ja Ikke Delvist genererer eksekverbar kode
Albatros 0,4 Helmut Brandl OKaml Ja Ikke Ja Ja ukendt ikke implementeret endnu
Coq 8.11.0 INRIA OKaml Ja Ja Ja Ja Ja Ja
F* i depotet Microsoft Research og INRIA F* Ja Ja Ikke Ja Ja [2] Ja
HOL Light i depotet John Harrison OKaml Ja Ikke Ja Ja Ikke Ikke
HOL4 Kananaskis-12 (eller i depotet) Michael Norrish, Konrad Slind og andre Standard ML Ja Ikke Ja Ja Ikke Ja
Isabelle 2019 Larry Paulson ( Cambridge ), Tobias Nipkow ( München ) og Makarius Wenzel StandardML , Scala Ja Ikke Ja Ja Ja Ja
Læne v3.4.2 [3] Microsoft Research C++ Ja Ja Ja Ja Ja ukendt
LEGO (ikke tilknyttet LEGO) 1.3.1 Randy Pollack ( Edinburgh ) Standard ML Ja Ja Ja Ikke Ikke Ikke
Mizar 8.1.05 Bialystok Universitet Gratis Pascal Delvist Ja Ikke Ikke Ikke Ikke
NuPRL 5 Cornell University Almindelig Lisp Ja Ja Ja Ja ukendt Ja
PVS 6,0 SRI International Almindelig Lisp Ja Ja Ikke Ja Ikke ukendt
Tolv 1.7.1 Frank Pfenning og Carsten Schürmann Standard ML Ja Ja ukendt Ikke Ikke ukendt

Brugergrænseflade

En populær grænseflade til interaktive teorembevisværktøjer er den Emacs-baserede Proof General udviklet ved University of Edinburgh . Coq inkluderer CoqIDE, som er skrevet i OCaml/ Gtk . Isabelle inkluderer Isabelle/jEdit, som er baseret på jEdit og Isabelle/ Scala -rammen for dokumentcentreret bevisbehandling. Til Visual Studio Code er der også en udvidelse designet til at fungere med Isabelle. Det blev udviklet af Makarius Wenzel [5] .

Se også

Noter

  1. ↑ Hunt, Warren; Matt Kaufman; Robert Bellarmine Krug; J Moore; Erik W. Smith. Meta-ræsonnement i ACL2  //  Springer Lecture Notes in Computer Science : journal. - 2005. - Bd. 3603 . - S. 163-178 .
  2. ↑ Søg efter "bevis ved refleksion": arXiv : 1803.06547
  3. ↑ Lean Theorem Prover Releases-side . GitHub . Arkiveret fra originalen den 5. september 2020.
  4. ↑ Farmer, William M.; Guttman, Joshua D.; Thayer, F. Javier. IMPS: Et interaktivt matematisk bevissystem  //  Journal of Automated Reasoning. - 1993. - Bd. 11 , nr. 2 . - S. 213-248 . - doi : 10.1007/BF00881906 .
  5. ↑ Wenzel, Makarius Isabelle . Hentet 31. maj 2020. Arkiveret fra originalen 4. juni 2020.

Litteratur

Links

Kataloger