Looginen ohjelmointi on eräänlainen tietokoneohjelmointi, jossa ohjelmoijan on annettava tietokoneelle ohjeet päätösten tekemisestä matemaattisen logiikan avulla, kuten matemaattisen algoritmin käyttö. Tietokoneohjelmat koostuvat koodista, joka kertoo tietokoneelle, mitä tehdä. Lopulta tietokone kuitenkin joutuu tilanteeseen, jossa sen on tehtävä päätös siitä, miten edetä, ja ilman tietoja siitä, miten tämä tehdään, se ei voinut suorittaa nykyistä toimintoaan. Looginen ohjelmointi käsittelee tällaisia päätöksiä ja antaa ohjeita tietokoneelle, jotta se voi tehdä “loogisen” päätöksen siitä, miten parhaiten reagoida tiettyyn tilanteeseen. Jotta looginen ohjelmointi toimisi, koodin kirjoittavan ohjelmoijan on varmistettava, että hänen lausuntonsa ovat järkeviä ja totta, joten ne ovat loogisia, ja lauseen todistajana tunnettu tietokoneohjelma edellyttää päätösten tekemistä ohjelmoijan lausunnoissa havaittujen lausuntojen perusteella koodi.
Lauseen todistaja viittaa tietokoneohjelmaan, joka on suunniteltu ratkaisemaan matemaattisia lausuntoja, joita kutsutaan lauseiksi. Lauseet ovat väitteitä, joiden on osoitettu pitävän paikkansa aiempien lausuntojen perusteella. Loogisessa ohjelmoinnissa lauseen todistaja tekee johtopäätöksiä yhdessä tietokoneohjelmoijan luomien lausuntojen kanssa. Jos esimerkiksi koodi ilmoittaa, että A on yhtä suuri kuin B ja B on yhtä suuri kuin C, lauseen todistaja tekee loogisen johtopäätöksen, että A: n on oltava yhtä suuri kuin C. Tämä prosessi on erilainen kuin ohjelmoija yksinkertaisesti kertoo tietokoneelle koodi, joka A on yhtä suuri kuin C, koska tietokoneohjelman on tehtävä tämä johtopäätös käyttämällä lauseen todistajaa ja ohjelmoijan alkuperäisiä lausekkeita koodissa.
Teoriassa, jotta looginen ohjelmointi toimisi, ohjelmoijan on vain varmistettava, että hänen lausuntonsa ovat oikeat ja lauseen todistajan on varmistettava, että ohjelma voi lukea lausuntoja ja tehdä tehokkaimmat päätökset niiden perusteella. Kykyä tehdä tehokas päätös kutsutaan “loogisesti” toimivaksi tietokoneeksi. Todellisuudessa nämä kaksi työaluetta ovat päällekkäisiä, ja loogista ohjelmointia suorittavien on usein muutettava ja käsiteltävä koodia sen perusteella, miten lauseen todistaja toimii, jotta he voivat saavuttaa haluamansa tulokset. Pelkkä tarkan lausunnon antaminen tietyn päätöksen tekemisestä ei ehkä riitä saamaan tietokonetta suorittamaan oikeaa toimintoa, ja ohjelmoijan on testattava koodinsa ja tehtävä muutokset sen mukaisesti.
Jotta looginen ohjelmointi toimisi, se perustuu myös taaksepäin. Taaksepäin päätellessään ohjelma tekee johtopäätöksiä tarkastelemalla datajoukkoa ja työskentelemällä yleisesti tunnetuista lausunnoista edistyneempien johtopäätösten tekemiseksi. Ohjelma saattaa tietää, että kaksi tietoa on totta, ja se päättelee, että koska nämä kaksi tietoa ovat totta, se tarkoittaa, että myös kolmas tieto on totta. Se jatkaa tätä prosessia, kunnes se saavuttaa loogisen johtopäätöksen antamiensa tietojen perusteella. Toimintatavansa vuoksi looginen ohjelmointi perustuu deklaratiiviseen esityskieleen, mikä tarkoittaa, että ohjelma kertoo tietokoneelle, mitä sen pitäisi tehdä, mutta jättää lauseen todistajan tehtäväksi määrittää loogisin tai tehokkain tapa suorittaa vaadittu menettely.