La programmazione logica è un tipo di programmazione informatica in cui il programmatore deve fornire al computer istruzioni su come prendere decisioni utilizzando la logica matematica, come l’uso di un algoritmo matematico. I programmi per computer sono costituiti da codice che dice al computer cosa fare. Alla fine, tuttavia, il computer si imbatterà in un’istanza in cui deve prendere una decisione su come procedere e senza alcuna informazione su come farlo, non potrebbe completare la sua funzione attuale. La programmazione logica si occupa di questi tipi di decisioni e fornisce istruzioni al computer in modo che possa prendere una decisione “logica” su come rispondere al meglio a una determinata situazione. Perché la programmazione logica funzioni, il programmatore che scrive il codice deve assicurarsi che le sue affermazioni abbiano senso e siano vere, quindi siano logiche, e un programma per computer noto come dimostratore di teoremi è necessario per prendere decisioni basate sulle affermazioni che incontra nel programmatore. codice.
Un dimostratore di teoremi si riferisce a un programma per computer che è stato progettato per risolvere affermazioni matematiche note come teoremi. I teoremi sono affermazioni che si dimostrano vere sulla base di affermazioni precedenti. Nella programmazione logica, il dimostratore di teoremi lavora insieme alle affermazioni create dal programmatore di computer per giungere a conclusioni. Ad esempio, se il codice afferma che A è uguale a B e B è uguale a C, il dimostratore di teoremi trarrà la logica conclusione che A deve essere uguale a C. Questo processo è diverso dal programmatore che semplicemente dice al computer nel codice che A è uguale a C perché il programma per computer deve trarre questa conclusione utilizzando il dimostratore di teoremi e le dichiarazioni originali del programmatore nel codice.
In teoria, affinché la programmazione logica funzioni, il programmatore deve solo assicurarsi che le sue affermazioni siano corrette e il creatore del dimostratore di teoremi dovrebbe garantire che il programma possa leggere le affermazioni e prendere le decisioni più efficienti basate su di esse. La capacità di prendere una decisione efficiente è indicata come un computer che funziona “logicamente”. In realtà, i due campi di lavoro si sovrappongono e chi esegue la programmazione logica spesso deve modificare e manipolare il codice in base a come funziona il dimostratore di teoremi per ottenere i risultati desiderati. La semplice immissione di affermazioni accurate su come prendere una determinata decisione potrebbe non essere sufficiente per consentire al computer di eseguire la funzione corretta e il programmatore dovrà testare il proprio codice e apportare modifiche di conseguenza.
Perché la programmazione logica funzioni, si basa anche sul ragionamento all’indietro. Nel ragionamento a ritroso, il programma giunge alle conclusioni esaminando una serie di dati e lavorando da affermazioni generalmente note per raggiungere conclusioni più avanzate. Il programma può sapere che due informazioni sono vere e ne dedurrà che, poiché queste due informazioni sono vere, ciò significa che anche una terza informazione è vera. Continua questo processo fino a raggiungere una conclusione logica basata sulle informazioni fornite. A causa del modo in cui funziona, la programmazione logica è basata su un linguaggio di rappresentazione dichiarativa, il che significa che il programma dice al computer cosa dovrebbe fare, ma lascia al dimostratore di teoremi il compito di determinare il modo più logico o efficiente per eseguire la procedura richiesta.