Matemaattiset todistusohjelmat ja niiden sovellukset
avoin
Julkaisu on tekijänoikeussäännösten alainen. Teosta voi lukea ja tulostaa henkilökohtaista käyttöä varten. Käyttö kaupallisiin tarkoituksiin on kielletty.
Lataukset59
Pysyvä osoite
Verkkojulkaisu
DOI
Tiivistelmä
Työssä tutkitaan, mitä erilaisia matemaattisten todistusten generointi- ja käsittelyohjelmia ja -menetelmiä on. Tutkimus on toteutettu kirjallisuukatsauksena. Ensin esitellään ATP-menetelmiä (Automated Theorem Prover), eli automaattisia matemaattisia todistusmenetelmiä. Käsitellään SAT- ja SMT-ratkaisualgoritmeja, resoluutiota, uudelleenkirjoitusta sekä superpositiokalkyyliä, luonnollista päättelyä, induktiota, korkeamman kertaluvun todistusmenetelmiä ja tekoälymenetelmiä. Perehdytään interaktiivisiin todistusohjelmiin eli todistusassistentteihin. Lisäksi tutustutaan todistusohjelmien sovelluksiin. Tutkimuksessa yritetään kartoittaa, mitä ohjelmallisia todistusmenetelmiä on olemassa. Matemaattisilla todistuohjelmilla ei ole ollut vielä melkein yhtään vaikutusta matematiikkaan. Sen sijaan formaalit menetelmät (engl. Formal methods), joka tarkoittaa ohjelmistojen ja laitteistojen toiminnan matemaattista varmistamista, on suosittu tieteenala.