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]
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]
Seamless Wikipedia browsing. On steroids.
Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.
Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.