Logisk programmering är en typ av datorprogrammering där programmeraren måste ge datorn instruktioner om hur man fattar beslut med hjälp av matematisk logik, till exempel användningen av en matematisk algoritm. Datorprogram består av kod som talar om för datorn vad den ska göra. Så småningom kommer dock datorn att stöta på en instans där den måste fatta ett beslut om hur den ska gå vidare och utan någon information om hur man gör detta kunde den inte slutföra sin nuvarande funktion. Logisk programmering hanterar dessa typer av beslut och ger instruktioner till datorn så att den kan fatta ett ”logiskt” beslut om hur man bäst reagerar på en viss situation. För att logisk programmering ska fungera måste programmeraren som skriver koden se till att hennes påståenden är vettiga och är sanna, alltså är logiska, och ett datorprogram som kallas en teorembevisare krävs för att fatta beslut baserat på de påståenden den möter i programmerarens program. koda.
En satsbevisare hänvisar till ett datorprogram som har designats för att lösa matematiska påståenden som kallas satser. Satser är påståenden som visats vara sanna baserat på tidigare påståenden. I logisk programmering arbetar satsbevisaren tillsammans med de påståenden som skapats av datorprogrammeraren för att nå slutsatser. Till exempel, om koden anger att A är lika med B och B är lika med C, kommer satsbevisaren att dra den logiska slutsatsen att A måste vara lika med C. Denna process är annorlunda än att programmeraren helt enkelt säger till datorn i kod att A är lika med C eftersom datorprogrammet måste dra denna slutsats med hjälp av satsbevisaren och programmerarens ursprungliga påståenden i koden.
I teorin, för att logisk programmering ska fungera behöver programmeraren bara se till att hennes påståenden är korrekta och skaparen av satsbevisaren bör se till att programmet kan läsa påståenden och fatta de mest effektiva besluten baserat på dem. Förmågan att fatta ett effektivt beslut kallas en dator som fungerar ”logiskt”. I verkligheten överlappar de två arbetsfälten varandra, och de som utför logisk programmering måste ofta ändra och manipulera koden utifrån hur satsbevisaren fungerar för att uppnå de resultat de önskar. Att bara lägga in korrekta uttalanden om hur man fattar ett visst beslut kanske inte räcker för att få datorn att utföra rätt funktion, och programmeraren måste testa sin kod och göra justeringar därefter.
För att logisk programmering ska fungera bygger den också på bakåtresonemang. I bakåtresonemang kommer programmet till slutsatser genom att titta på en uppsättning data och arbeta utifrån allmänt kända påståenden för att nå mer avancerade slutsatser. Programmet kanske vet att två delar av information är sanna, och det kommer att dra slutsatsen att eftersom dessa två delar av information är sanna, betyder det att en tredje del av information också är sann. Den fortsätter denna process tills den når en logisk slutsats baserat på informationen den har gett. På grund av hur det fungerar är logisk programmering byggd på deklarativt representationsspråk, vilket innebär att programmet talar om för datorn vad den ska göra, men överlåter det till satsbevisaren att bestämma det mest logiska eller effektiva sättet att utföra den begärda proceduren.