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.

Tõestusassistentidega on võimalik hõlbustada tarkvaraarendust: näiteks võivad nad aidata kinnitada arvutiprogrammide loogika täielikkust, ning mitmed tõestusassistendid toimivad ka funktsionaalsete programmeerimiskeeltena. 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.

 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.
 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.

 Märkimisväärsed formaliseeritud tõestused 
 Teoreem Tõestusassistent AastaNeljavärviprobleemCoq2005Feiti-Thompsoni teoreemCoq2012Ringi fundamentaalgruppCoq2013Polünomiaalne Freiman-Ruzsa konjuktuurLean2023

 Viited 

Kategooria:Loogika
Kategooria:Tarkvara