Loogika aine ja ajalugu
Predikaatarvutusest oluliselt lihtsamad
loogikasüsteemid on sageli lahenduvad. Juba enne Turingit oli teada, et näiteks klassikaline lausearvutus on lahenduv.
On olemas algoritmid, mis suudavad (kui neile piisavalt aega anda) iga lausearvutuse keeles kirjutatud väite kohta
öelda, kas see väide on õige ja tuletatav, või vale ja ei ole tuletatav.
Lahenduvuse takistuseks on väited, mis pole tuletatavad: ei saa olla olemas algoritmi, mis suudaks mittetuletatava
predikaatarvutuse väite puhul alati õigesti otsustada, et seda väidet tuletada ei saa ja otsingu võib katki jätta.
Tuletatavate väidete puhul aga suudab Turing masin tuletuse teoreetiliselt alati leida. Muidugi võib mittetriviaalsete
väidete tuletuste leidmiseks sageli rohkem aega kuluda kui universumil vanust.
1936. aastal esitas Alonzo Church minimaalsete vahenditega algoritmikirjutamise- ehk progammeerimiskeele, nn.
lambda-arvutuse
annaabi.ee 
