Matemaattiset todistusohjelmat ja niiden sovellukset

Tietueen suppeat tiedot
dc.contributor.authorSyrén, Aapeli
dc.contributor.departmentfi=Tietotekniikan laitos|en=Department of Computing|
dc.contributor.facultyfi=Teknillinen tiedekunta|en=Faculty of Technology|
dc.contributor.studysubjectfi=Tietojenkäsittelytieteet|en=Computer Science|
dc.date.accessioned2026-01-22T22:30:43Z
dc.date.available2026-01-22T22:30:43Z
dc.date.issued2026-01-15
dc.description.abstractTyö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.
dc.format.extent35
dc.identifier.olddbid214254
dc.identifier.oldhandle10024/197272
dc.identifier.urihttps://www.utupub.fi/handle/11111/1166
dc.identifier.urnURN:NBN:fi-fe202601227803
dc.language.isofin
dc.rightsfi=Julkaisu on tekijänoikeussäännösten alainen. Teosta voi lukea ja tulostaa henkilökohtaista käyttöä varten. Käyttö kaupallisiin tarkoituksiin on kielletty.|en=This publication is copyrighted. You may download, display and print it for Your own personal use. Commercial use is prohibited.|
dc.rights.accessrightsavoin
dc.source.identifierhttps://www.utupub.fi/handle/10024/197272
dc.subjectutomaattinen todistusohjelma, Interaktiivinen todistusohjelma, Todis- tusassistentti, Formaalit menetelmät
dc.titleMatemaattiset todistusohjelmat ja niiden sovellukset
dc.type.ontasotfi=Kandidaatintutkielma|en=Bachelor's thesis|

Tiedostot

Näytetään 1 - 1 / 1
Name:
Syren_Aapeli_matemaattiset_todistusohjelmat_ja_niiden_sovellukset.pdf
Size:
466.2 KB
Format:
Adobe Portable Document Format
Lataa

Kokoelmat

Kandidaatin tutkielmat (kokotekstit)