Programarea logică este un tip de programare a computerului în care programatorul trebuie să dea computerului instrucțiuni despre cum să ia decizii folosind logica matematică, cum ar fi utilizarea unui algoritm matematic. Programele de calculator sunt alcătuite din cod care îi spune computerului ce trebuie să facă. În cele din urmă, totuși, computerul va întâlni o instanță în care trebuie să ia o decizie cu privire la modul de a proceda și, fără nicio informație despre cum să facă acest lucru, nu și-ar putea îndeplini funcția actuală. Programarea logică se ocupă de aceste tipuri de decizii și oferă computerului instrucțiuni pentru ca acesta să poată lua o decizie „logică” despre cum să răspundă cel mai bine la o anumită situație. Pentru ca programarea logică să funcționeze, programatorul care scrie codul trebuie să se asigure că afirmațiile sale au sens și sunt adevărate, prin urmare sunt logice, iar un program de calculator cunoscut sub numele de demonstrator de teoreme este necesar să ia decizii pe baza afirmațiilor pe care le întâlnește în programul programatorului. cod.
Un probator de teoreme se referă la un program de calculator care a fost conceput pentru a rezolva enunțuri matematice cunoscute sub numele de teoreme. Teoremele sunt afirmații care se dovedesc a fi adevărate pe baza afirmațiilor anterioare. În programarea logică, teorema-dovatorul lucrează împreună cu afirmațiile create de programatorul de calculator pentru a ajunge la concluzii. De exemplu, dacă codul afirmă că A este egal cu B și B este egal cu C, probatorul teoremei va face concluzia logică că A trebuie să fie egal cu C. Acest proces este diferit de programatorul care spune pur și simplu computerului în codează că A este egal cu C deoarece programul de calculator trebuie să tragă această concluzie folosind teorema-dovator și declarațiile originale ale programatorului din cod.
În teorie, pentru ca programarea logică să funcționeze, programatorul trebuie doar să se asigure că afirmațiile ei sunt corecte, iar creatorul demonstratorului de teoreme ar trebui să se asigure că programul poate citi declarații și poate lua cele mai eficiente decizii pe baza acestora. Capacitatea de a lua o decizie eficientă este denumită un computer care funcționează „logic”. În realitate, cele două domenii de lucru se suprapun, iar cei care efectuează programare logică trebuie adesea să schimbe și să manipuleze codul în funcție de modul în care funcționează teorema-dovatorul pentru a obține rezultatele dorite. Pur și simplu introducerea unor declarații exacte despre cum să luați o anumită decizie poate să nu fie suficientă pentru a determina computerul să îndeplinească funcția corectă, iar programatorul va trebui să-și testeze codul și să facă ajustări în consecință.
Pentru ca programarea logică să funcționeze, se bazează și pe raționamentul înapoi. În raționamentul înapoi, programul ajunge la concluzii analizând un set de date și lucrând din afirmații generale cunoscute pentru a ajunge la concluzii mai avansate. Programul poate ști că două informații sunt adevărate și va deduce că, deoarece acele două informații sunt adevărate, asta înseamnă că o a treia informație este de asemenea adevărată. Continuă acest proces până când ajunge la o concluzie logică bazată pe informațiile pe care le oferă. Datorită modului în care funcționează, programarea logică este construită pe un limbaj de reprezentare declarativă, adică programul îi spune computerului ce ar trebui să facă, dar lasă la latitudinea dovezitorului teoremei să determine cel mai logic sau eficient mod de a efectua procedura solicitată.