Logično programiranje je vrsta računalniškega programiranja, pri katerem mora programer dati računalniku navodila, kako se odločati z uporabo matematične logike, kot je uporaba matematičnega algoritma. Računalniški programi so sestavljeni iz kode, ki računalniku pove, kaj naj naredi. Sčasoma pa bo računalnik naletel na primer, ko se mora odločiti, kako naprej, in brez kakršnih koli informacij, kako to storiti, ne bi mogel dokončati svoje trenutne funkcije. Logično programiranje se ukvarja s tovrstnimi odločitvami in daje navodila računalniku, da lahko sprejme »logično« odločitev o tem, kako se najbolje odzvati na določeno situacijo. Da bi logično programiranje delovalo, mora programer, ki piše kodo, zagotoviti, da so njene izjave smiselne in resnične, torej logične, zato je potreben računalniški program, znan kot dokazovalec izrekov, da sprejema odločitve na podlagi izjav, na katere naleti v programerjevem Koda.
Dokazovalec izrekov se nanaša na računalniški program, ki je bil zasnovan za reševanje matematičnih izjav, znanih kot izreki. Teoremi so trditve, za katere se izkaže, da so resnične na podlagi prejšnjih trditev. Pri logičnem programiranju dokazovalec izrekov deluje skupaj z izjavami, ki jih ustvari računalniški programer, da doseže zaključke. Na primer, če koda navaja, da je A enako B in B enako C, bo dokazovalec izrekov logično zaključil, da mora biti A enako C. Ta postopek se razlikuje od tega, da programer preprosto pove računalniku v kodo, da je A enako C, ker mora računalniški program narediti ta sklep z uporabo dokazovalca izrekov in programerjevih izvirnih stavkov v kodi.
V teoriji mora programer, da logično programiranje deluje, le zagotoviti, da so njene izjave pravilne, ustvarjalec dokazovalca izrekov pa mora zagotoviti, da lahko program bere izjave in na podlagi njih sprejema najučinkovitejše odločitve. Sposobnost učinkovite odločitve se imenuje računalnik, ki deluje »logično«. V resnici se ti dve področji dela prekrivata in tisti, ki izvajajo logično programiranje, morajo pogosto spreminjati in manipulirati s kodo glede na to, kako deluje dokazovalec izrekov, da bi dosegli želene rezultate. Preprosto dajanje natančnih izjav o tem, kako sprejeti določeno odločitev, morda ne bo dovolj, da bi računalnik izvedel pravilno funkcijo, programer pa bo moral preizkusiti svojo kodo in ustrezno prilagoditi.
Da bi logično programiranje delovalo, se zanaša tudi na nazaj sklepanje. Pri sklepanju nazaj program pride do zaključkov tako, da pogleda nabor podatkov in dela na podlagi splošnih znanih izjav, da doseže naprednejše zaključke. Program morda ve, da sta dva podatka resnična, in sklepa, da ker sta ta dva podatka resnična, to pomeni, da je tudi tretji del informacije resničen. Ta postopek nadaljuje, dokler ne doseže logičnega zaključka na podlagi informacij, ki jih je prejel. Zaradi načina delovanja je logično programiranje zgrajeno na deklarativnem predstavitvenem jeziku, kar pomeni, da program pove računalniku, kaj naj naredi, vendar prepusti dokazovalcu izrekov, da določi najbolj logičen ali učinkovit način za izvedbo zahtevanega postopka.