Matemaattiset todistusohjelmat ja niiden sovellukset

Abstract

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.