Interaktiivinen lauseiden todistamistyökalu

Vuorovaikutteinen lauseiden todistamistyökalu ( interaktiivinen lauseen ratkaisija ) on ohjelmisto , joka auttaa tutkijaa muodollisten todisteiden kehittämisessä . Todisteita tuotetaan ihmisen ja koneen välisessä vuorovaikutuksessa. Tyypillisesti tällaiset ohjelmistot sisältävät jonkinlaisen interaktiivisen todisteiden editorin tai muun käyttöliittymän, jonka kautta henkilö voi etsiä tietokoneelle tallennettuja todisteita, sekä tietokoneen suorittamia automaattisia todisteiden varmistustoimenpiteitä.

Järjestelmien vertailu

Nimi uusin versio Kehittäjä(t) Toteutuskieli Ominaisuudet
korkeamman asteen logiikkaa Riippuvaiset tyypit pieni ydin Todisteiden automaatio Todistus heijastuksella koodin luominen
ACL2 8.2 Matt Kaufmann ja J Strother Moore Yhteinen Lisp Ei kirjoittamaton Ei Joo Kyllä [1] luo suoritettavaa koodia
Agda 2.6.0.1 Ulf Norell, Nils Anders Danielsson ja Andreas Abel ( Chalmersin teknillinen yliopisto ja Göteborgin yliopisto ) Haskell Joo Joo Joo Ei Osittain luo suoritettavaa koodia
Albatrossi 0.4 Helmut Brandl OCaml Joo Ei Joo Joo tuntematon ei ole vielä toteutettu
Coq 8.11.0 INRIA OCaml Joo Joo Joo Joo Joo Joo
F* arkistossa Microsoft Research ja INRIA F* Joo Joo Ei Joo kyllä ​​[2] Joo
HOL Light arkistossa John Harrison OCaml Joo Ei Joo Joo Ei Ei
HOL4 Kananaskis-12 (tai arkistossa) Michael Norrish, Konrad Slind ja muut Normaali ML Joo Ei Joo Joo Ei Joo
Isabelle 2019 Larry Paulson ( Cambridge ), Tobias Nipkow ( München ) ja Makarius Wenzel StandardML , Scala Joo Ei Joo Joo Joo Joo
Nojata v3.4.2 [3] Microsoftin tutkimus C++ Joo Joo Joo Joo Joo tuntematon
LEGO (ei sidoksissa LEGOon) 1.3.1 Randy Pollack ( Edinburgh ) Normaali ML Joo Joo Joo Ei Ei Ei
Mizar_ 8.1.05 Bialystokin yliopisto Ilmainen Pascal Osittain Joo Ei Ei Ei Ei
NuPRL 5 Cornellin yliopisto Yhteinen Lisp Joo Joo Joo Joo tuntematon Joo
PVS 6.0 SRI International Yhteinen Lisp Joo Joo Ei Joo Ei tuntematon
Kaksitoista 1.7.1 Frank Pfenning ja Carsten Schürmann Normaali ML Joo Joo tuntematon Ei Ei tuntematon

Käyttöliittymä

Suosittu interaktiivisten lauseiden todistamistyökalujen käyttöliittymä on Edinburghin yliopistossa kehitetty Emacs-pohjainen Proof General . Coq sisältää CoqIDEn, joka on kirjoitettu kielellä OCaml/ Gtk . Isabelle sisältää Isabelle/jEditin, joka perustuu jEditiin ja Isabelle/ Scala -kehykseen dokumenttikeskeiseen todisteiden käsittelyyn. Visual Studio Codessa on myös laajennus, joka on suunniteltu toimimaan Isabellen kanssa. Sen on kehittänyt Makarius Wenzel [5] .

Katso myös

Muistiinpanot

  1. ↑ Hunt, Warren; Matt Kaufman; Robert Bellarmine Krug; J Moore; Eric W. Smith. Metapäättely ACL2:ssa  //  Springerin luentomuistiinpanot tietojenkäsittelytieteessä : päiväkirja. - 2005. - Voi. 3603 . - s. 163-178 .
  2. ↑ Hae "todistuksia heijastuksella": arXiv : 1803.06547
  3. ↑ Lean Theorem Prover -julkaisusivu . GitHub . Arkistoitu alkuperäisestä 5.9.2020.
  4. ↑ Farmer, William M.; Guttman, Joshua D.; Thayer, F. Javier. IMPS: Interaktiivinen matemaattinen todistusjärjestelmä  //  Journal of Automated Reasoning. - 1993. - Voi. 11 , ei. 2 . - s. 213-248 . - doi : 10.1007/BF00881906 .
  5. ↑ Wenzel, Makarius Isabelle . Haettu 31. toukokuuta 2020. Arkistoitu alkuperäisestä 4. kesäkuuta 2020.

Kirjallisuus

Linkit

Luettelot