Programmeerimiskeel
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
solved using his automated theorem prover EQP.
.Programm otsis lahendust ca üks nädal, kuni lõpuks leidis
.Ülesanne oli matemaatikute poolt lahendamata, kuigi püstitati aastal
1933:
.Meil on antud Robbinsi algebra:
x + y = y + x. [commutativity]
(x + y) + z = x + (y + z). [associativity]
n(n(x + y) + n(x + n(y))) = x. [Robbins equation]
.Kas järgmised võrdused annava selle algebra jaoks vastuolu:
x+y != x.
annaabi.ee 
