Ricerca di dimostrazioni
La ricerca dimostrazioni è una tecnica di ricerca alternativa all'enumerazione completa dei modelli di un problema. A partire da una base di conoscenza e da alcune informazioni sullo stato della realtà, l'algoritmo di ricerca verifica se un'affermazione è vera o falsa. Ad esempio, date tre proposizioni logiche ( A, B, C ), la seguente formula consente di realizzare una semplice base di conoscenza
B ∨ C ⇒ A
L'agente razionale osserva la realtà circostante rilevando che la proposizione A non è vera. L'agente razionale si domanda, adesso, se la proposizione C è falsa. Per rispondere a questa domanda l'agente razionale può analizzare tutte le possibili combinazioni di A, B, C tramite l'enumerazione completa dei modelli ( model checking ).
Questo processo può diventare enormemente lungo. L'enumerazione completa delle combinazioni espone l'algoritmo alla complessità temporale in quanto il tempo di esecuzione necessario cresce in modo esponenziale rispetto al numero delle variabili. La ricerca di dimostrazioni consente, invece, di stabilire la verità o meno di un'asserzione analizzando le conseguenze logiche del modello e avvalendosi delle regole di inferenza logica. Ad esempio, sapendo che la proposizione A è falsa, possiamo riscrivere la formula nella seguente equivalenza logica:
¬ ( B ∨ C ) ⇒ ¬ ( A )
In base alle leggi di De Morgan l'espressione logica ¬ ( B ∨ C ) può essere riscritta nell'equivalenza logica ( ¬ B ∧ ¬ C ). È quindi possibile riscrivere la formula nella seguente forma equivalente:
( ¬ B ∧ ¬ C ) ⇒ ¬ ( A )
E', quindi, possibile affermare che quando la proposizione logica A è falsa ( ¬ A ) anche le proposizioni logiche B e C sono false. In conclusione, la proposizione logica C è falsa ( non verificata ) poiché la proposizione logica A è falsa. L'algoritmo di ricerca delle dimostrazioni può, pertanto, rispondere alla domanda senza aver analizzato tutte le possibili combinazioni di valori alle variabili e tutti i casi possibili.
Eliminazione variabili irrilevanti. La ricerca di dimostrazioni consente di evitare di prendere in considerazione le variabili logicamente ininfluenti. Ad esempio, per rispondere alla domanda iniziale ( C è falso o vero? ) la tecnica di ricerca basata sul model checking analizza tutte le combinazioni possibili, prendendo in considerazione tutte le variabili logiche del sistema. Viceversa, l'algoritmo di ricerca di dimostrazione prende in considerazione soltanto le variabili e le formule della base di conoscenza coinvolte nella conseguenza logica del problema.
Minore complessità temporale. La ricerca di dimostrazioni è particolarmente utile per analizzare le basi di conoscenza e i sistemi complessi, laddove vi sono molte proposizioni logiche e molte regole da prendere in considerazione. Mentre nella tecnica di ricerca classica ( model checking ) ogni ulteriore variabile da analizzare aumenta in modo esponenziale la durata del processo di ricerca, ossia il tempo di esecuzione dell'algoritmo, nel caso della ricerca di dimostrazioni ciò non accade.
