Tõestusassistent

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.

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

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

• 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:
  • HOL4 – HOL-i "peamine järeltulija", pidevalt arenduses. Toetab Moscow ML ja Poly/ML keeli. BSD-stiilis litsents.
  • HOL Light – minimalistlik haru. Põhineb OCaml-il.
  • ProofPower – oli ajutiselt omanduslik tarkvara, siis tehti uuesti vabavaraks. Põhineb Standard ML-il.
• 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

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

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