Programmeerimiskeel
mis tõlge on parem kui teine ja milline on selgelt vigane.
ITK 2007, Kalev Pihl
Sissejuhatus informaatikasse
18
Ülesannete lahendamine
loogikatõestuse abil
.Ülesanne tuleb loogika keeles formuleerida.
.Küsimus tuleb ka loogika keeles formuleerida.
.Tõestaja asub tõestust otsima.
.Kui anda lõpmatult palju aega ja mälu, siis tõestaja lõpuks ka
tõestuse leiab (kui tõestus üldse teoreetiliselt eksisteerib). Keeruliste
ülesannete puhul võtaks see lootusetult kaua aega (meenuta
keerukusklasse!)
.Kui tõestust ei ole, siis tõestaja enamasti jääbki seda otsima,
teadmata, et sellist tõestust ei saa olla.
.Tõestajate igaastased võistlused CASC:
.http://www.cs.miami.edu/~tptp/CASC/
.Gandalf:
.Tammeti tõestaja, mitmelaastalvõitnud mõne CASC kategooria
.http://www.ttu.ee/it/gandalf/
ITK 2007, Kalev Pihl
Sissejuhatus informaatikasse
19
Näide: masinaga lahendatud matemaatikaprobleem
W. McCune 1996:
.The Robbins problem---are all Robbins algebras Boolean?-has been
annaabi.ee 
