Tõestusassistent

Interaktiivne tõestussessioon CoqIDE keskkonnas, kus tõestusskript on vasakul ja tõestuse seisund on paremal.

Tõestusassistent ehk interaktiivne teoreemitõestaja on arvutiprogramm, mille eesmärk on aidata inimestel arvuti abiga arendada formaalseid tõestusi teoreemidele matemaatilises loogikas. Tõestusassistent koosneb mingit laadi interaktiivsest teoreemiredaktorist või muust kasutajaliidesest, millega on võimalik juhtida otsingut tõestuste jaoks. Selle otsingu üksikasjad ja tegevuskäik sisalduvad arvutis.

Tõestusassistentidega on võimalik hõlbustada tarkvaraarendust: näiteks võivad nad aidata kinnitada arvutiprogrammide loogika täielikkust,[1] ning mitmed tõestusassistendid toimivad ka funktsionaalsete programmeerimiskeeltena.[2] Tõestusassistentide keeli ei loeta loogilise programmeerimise keelteks, sest nende ülesehitus on erinev.

Hiljuti on üritatud varustada need tööriistad tehisintellektiga, et automaatselt formaliseerida matemaatika üldtermineid.[3]

Tõestusassistentide nimekiri

[muuda | muuda lähteteksti]
  • ACL2 – programmeerimiskeel, esimese järgu loogika teooria ning teoreemitõestaja (interaktiivse ja automaatse režiimiga) Boyeri-Moore'i traditsioonis.
  • Coq – võimaldab väljendada matemaatilisi väiteid, kontrollib nende väidete tõestusi mehaaniliselt, aitab leida formaalseid tõestusi ning eraldab sertifitseeritud programmi selle formaalse spetsifikatsiooni konstruktiivsest tõestusest. Sisaldab kasutajaliidest CoqIDE, mis põhineb OCaml/Gtk-l.
  • HOL teoreemitõestajad – tööriistade perekond, mis on tuletatud LCF-i teoreemitõestajast. Nendes süsteemides on nende loogiline tuum nende programmeerimiskeele teek. Teoreemid esindavad uusi keeleelemente ning neid saab luua ainult läbi "strateegiate". See garanteerib loogilist korrektsust ning strateegiaid on võimalik komponeerida, et toota arvestatav kogus tõestusi vähese jõupingutusega. HOL perekonda kuuluvad:
  • Isabelle – interaktiivne teoreemitõestaja, mis on HOL-i järeltulija. Põhiline kood on BSD-litsentsi all, aga Isabelle'i distributsioon annab kaasa paljusid laiendusi, millel on erinevad litsentsid. Sisaldab Isabelle/jEdit graafilist kasutajaliidest, mis põhineb jEdit tekstiredaktoril, ning Isabelle/Scala taristut dokumendipõhiste tõestuste töötlemiseks. Makarius Wenzel on arendanud laiendusi Isabelle'i jaoks koodiredaktori Visual Studio Code jaoks.[4]
  • Lean
  • Mizar – tõestusassistent, mis põhineb esimese järgu loogikal loomuliku deduktsiooni stiilis ning Tarski-Grothendiecki hulgateoorial.
  • Prototype Verification System (PVS) – tõestuskeel ja -süsteem, mis põhineb kõrgema järgu loogikal.

Formalisatsioonide ulatus

[muuda | muuda lähteteksti]

Freek Wiedijk koostas nimekirja tõestusassistentidest vastavalt nende poolt formaliseeritud teoreemide arvule 100 hästi tuntud teoreemi põhjal. 2023. aasta septembri seisuga on kõigest viies süsteemis vähemalt 70% neist teoreemidest tõestatud, nimelt süsteemides Isabelle, HOL Light, Coq, Lean ja Metamath.[5][6]

Märkimisväärsed formaliseeritud tõestused

[muuda | muuda lähteteksti]
Teoreem Tõestusassistent Aasta
Neljavärviprobleem[7] Coq 2005
Feiti-Thompsoni teoreem[8] Coq 2012
Ringi fundamentaalgrupp[9] Coq 2013
Polünomiaalne Freiman-Ruzsa konjuktuur[10] Lean 2023

Viited

[muuda | muuda lähteteksti]
  1. ↑ "Certified Programming in Coq - Ocaml Wiki". www.ocamlwiki.com. Originaali arhiivikoopia seisuga 12. detsember 2023. Vaadatud 12. detsembril 2023.
  2. ↑ "A short introduction to Coq | The Coq Proof Assistant". coq.inria.fr. Vaadatud 18. jaanuaril 2024.
  3. ↑ Ornes, Stephen (27. august 2020). "Quanta Magazine – How Close Are Computers to Automating Mathematical Reasoning?" (Ameerika inglise).
  4. ↑ Wenzel, Makarius. "Isabelle". Vaadatud 2. novembril 2019.
  5. ↑ Wiedijk, Freek (15. september 2023). "Formalizing 100 Theorems".
  6. ↑ Geuvers, Herman (veebruar 2009). "Proof assistants: History, ideas and future". Sādhanā. 34 (1): 3–25. DOI:10.1007/s12046-009-0001-5. S2CID 14827467.
  7. ↑ Gonthier, Georges (2008), "Formal Proof—The Four-Color Theorem" (PDF), Notices of the American Mathematical Society, 55 (11): 1382–1393, MR 2463991, originaali arhiivikoopia (PDF) seisuga 5. august 2011
  8. ↑ "Feit thomson proved in coq - Microsoft Research Inria Joint Centre". 19. november 2016. Originaali arhiivikoopia seisuga 19. november 2016. Vaadatud 7. detsembril 2023.
  9. ↑ Licata, Daniel R.; Shulman, Michael (2013). Calculating the Fundamental Group of the Circle in Homotopy Type Theory | IEEE Conference Publication | IEEE Xplore. Lk 223–232. arXiv:1301.3443. DOI:10.1109/lics.2013.28. ISBN 978-1-4799-0413-6. S2CID 5661377. Vaadatud 7. detsembril 2023.
  10. ↑ Sloman, Leila (6. detsember 2023). "'A-Team' of Math Proves a Critical Link Between Addition and Sets". Quanta Magazine (inglise). Vaadatud 7. detsembril 2023.