Tõestusassistent
tarkvara, mis aitab luua formaalseid tõestusi läbi inimese ja arvuti koostöö / From Wikipedia, the free encyclopedia
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.
See artikkel vajab toimetamist. (Detsember 2023) |
See artikkel ootab keeletoimetamist. (Detsember 2023) |
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]