Logičko programiranje je vrsta računalnog programiranja u kojoj programer mora dati računalu upute o tome kako donijeti odluke koristeći matematičku logiku, kao što je korištenje matematičkog algoritma. Računalni programi se sastoje od koda koji računalu govori što treba učiniti. Na kraju, međutim, računalo će naići na instancu u kojoj mora donijeti odluku kako dalje i bez ikakvih informacija o tome kako to učiniti, ne može dovršiti svoju trenutnu funkciju. Logičko programiranje bavi se ovim vrstama odluka i daje upute računalu kako bi ono moglo donijeti “logičnu” odluku o tome kako najbolje reagirati na određenu situaciju. Da bi logičko programiranje funkcioniralo, programer koji piše kod mora osigurati da su njezine izjave smislene i istinite, dakle logične, a računalni program poznat kao dokazivač teorema potreban je za donošenje odluka na temelju izjava koje susreće u programerovu kodirati.
Dokazivač teorema odnosi se na računalni program koji je dizajniran za rješavanje matematičkih iskaza poznatih kao teoremi. Teoremi su tvrdnje koje se pokazuju kao istinite na temelju prethodnih tvrdnji. U logičkom programiranju, dokazivač teorema radi zajedno s izjavama koje stvara računalni programer kako bi došao do zaključaka. Na primjer, ako kod kaže da je A jednako B, a B jednako C, dokazivač teorema će donijeti logičan zaključak da A mora biti jednako C. Ovaj proces se razlikuje od toga da programer jednostavno kaže računalu u kod da je A jednako C jer računalni program mora izvesti ovaj zaključak koristeći dokazivač teorema i izvorne izjave programera u kodu.
U teoriji, da bi logičko programiranje funkcioniralo, programer samo treba osigurati da su njezini iskazi točni, a tvorac dokazivača teorema trebao bi osigurati da program može čitati izjave i donositi najučinkovitije odluke na temelju njih. Sposobnost donošenja učinkovite odluke naziva se računalom koje funkcionira “logično”. U stvarnosti se ta dva polja rada preklapaju, a oni koji izvode logičko programiranje često moraju mijenjati i manipulirati kodom na temelju načina na koji dokazivač teorema radi kako bi postigli željene rezultate. Jednostavno unošenje točnih izjava o tome kako donijeti određenu odluku možda neće biti dovoljno da računalo izvrši ispravnu funkciju, a programer će morati testirati svoj kod i u skladu s tim izvršiti prilagodbe.
Da bi logičko programiranje funkcioniralo, ono se također oslanja na rezoniranje unatrag. U rezoniranju unatrag, program dolazi do zaključaka gledajući skup podataka i radeći na opće poznatim izjavama kako bi došao do naprednijih zaključaka. Program može znati da su dvije informacije istinite i zaključit će da, budući da su te dvije informacije istinite, to znači da je i treći dio informacije istinit. Nastavlja ovaj proces sve dok ne dođe do logičnog zaključka na temelju informacija koje mu je dao. Zbog načina na koji radi, logičko programiranje je izgrađeno na jeziku deklarativnog predstavljanja, što znači da program govori računalu što treba učiniti, ali prepušta dokazivaču teorema da odredi najlogičniji ili učinkovitiji način za izvođenje tražene procedure.