Loogiline programmeerimine on arvutiprogrammeerimise liik, mille puhul programmeerija peab andma arvutile juhised, kuidas teha matemaatilist loogikat kasutades otsuseid, näiteks kasutada matemaatilist algoritmi. Arvutiprogrammid koosnevad koodist, mis ütleb arvutile, mida teha. Lõpuks aga satub arvuti eksemplari, kus ta peab otsustama, kuidas edasi minna, ja ilma selle kohta teabeta ei saa see oma praegust funktsiooni täita. Loogiline programmeerimine tegeleb seda tüüpi otsustega ja annab arvutile juhiseid, et ta saaks teha “loogilise” otsuse, kuidas teatud olukorrale kõige paremini reageerida. Loogilise programmeerimise toimimiseks peab koodi kirjutav programmeerija tagama, et tema väited on mõistlikud ja tõesed, seega loogilised ning teoreemide tõestajana tuntud arvutiprogramm peab tegema otsuseid, mis põhinevad programmeerija avalduses esinevatel väidetel. kood.
Teoreemi tõestaja viitab arvutiprogrammile, mis on loodud teoreemidena tuntud matemaatiliste väidete lahendamiseks. Teoreemid on väited, mis osutuvad tõeseks eelnevate väidete põhjal. Loogilises programmeerimises töötab teoreemi tõestaja koos programmeerija loodud väidetega järelduste tegemiseks. Näiteks kui kood väidab, et A on võrdne B-ga ja B on võrdne C-ga, teeb teoreemi tõestaja loogilise järelduse, et A peab olema võrdne C-ga. See protsess erineb sellest, kui programmeerija lihtsalt ütleb arvutile koodi, et A on võrdne C-ga, sest arvutiprogramm peab selle järelduse tegema, kasutades teoreemi tõestajat ja programmeerija algseid lauseid koodis.
Teoreetiliselt peab loogilise programmeerimise toimimiseks programmeerija ainult veenduma, et tema väited on õiged, ja teoreemi tõestaja looja peaks tagama, et programm suudab lugeda väiteid ja teha nende põhjal kõige tõhusamaid otsuseid. Võimalust teha tõhusaid otsuseid nimetatakse “loogiliselt toimivaks” arvutiks. Tegelikkuses need kaks töövaldkonda kattuvad ning loogilise programmeerimisega tegelejad peavad sageli soovitud tulemuste saavutamiseks koodi muutma ja manipuleerima teoreemi tõestaja tööpõhimõtte järgi. Lihtsalt täpsete avalduste esitamisest selle kohta, kuidas teatud otsus teha, ei pruugi arvuti õiget funktsiooni täitmiseks piisata ning programmeerija peab oma koodi testima ja vastavalt muudatusi tegema.
Loogilise programmeerimise toimimiseks tugineb see ka tagurpidisele mõtlemisele. Tagurpidi arutledes teeb programm järeldusi, vaadeldes andmete kogumit ja töötades välja üldiste teadaolevate väidete põhjal, et jõuda täpsemate järeldusteni. Programm võib teada, et kaks teavet on tõesed, ja järeldab, et kuna need kaks teavet on tõesed, tähendab see, et ka kolmas teave on tõene. See jätkab seda protsessi, kuni jõuab antud teabe põhjal loogilise järelduseni. Selle toimimisviisi tõttu on loogiline programmeerimine üles ehitatud deklaratiivsele esituskeelele, mis tähendab, et programm ütleb arvutile, mida ta peaks tegema, kuid jätab teoreemi tõestaja otsustada, milline on kõige loogilisem või tõhusam viis soovitud protseduuri sooritamiseks.