15. Clausole e vincoli proposizionali

Dopo aver introdotto nel precedente articolo le proposizioni, in questo articolo approfondiamo le clausole e i vincoli proposizionali. Avevamo introdotto il ragionamento con vincoli sin dall'articolo 10, approfondiamo i vincoli proposizionali e le formule logiche, le quali forniscono una struttura di vincoli che può essere sfruttata.

Definiamo un sotto linguaggio del calcolo proposizionale che non ammette incertezza o ambiguità, il cosiddetto linguaggio delle clausole proposizionali definite. La sintassi delle proposizioni è definita attraverso una proposizione atomica, che corrisponde a quella del calcolo proposizionale e una proposizione definita nella forma $h \leftarrow a_1 \wedge \dots \wedge a_m$. Definiamo h come la testa (head) della clausola, e ogni $a_i$ un atomo.

Se m è maggiore di 0, la clausola prende il nome di regola e la parte destra corpo della clausola. Mentre nel caso in cui m sia proprio uguale a 0, la freccia uò essere omessa e la clausola prende il nome di clausola atomica o fatto. Una base di conoscenza è un insieme di queste clausole. Dopo che al computer è stata fornita una base di conoscenza su un particolare dominio, un utente potrebbe voler porre al computer domande su quel dominio. Il computer può rispondere se una proposizione è o meno una conseguenza logica della base di conoscenza. Se l'utente conosce il significato degli atomi, l'utente può interpretare la risposta in termini di dominio.

Una query è un modo per chiedere se una proposizione è una conseguenza logica di una base di conoscenza. Una volta che il sistema è stato dotato di una base di conoscenza, viene utilizzata una query per chiedere se una formula è una conseguenza logica della base di conoscenza. Una query è una domanda che ha come risposta “sì” se il corpo è una conseguenza logica della base di conoscenza, o la risposta “no” se il corpo non è una conseguenza della base di conoscenza.

All'interno della base di conoscenza vi è il problema della deduzione, ovvero il problema di determinare se una proposizione è una conseguenza logica di una base di conoscenza. Questa deduzione è una forma specifica di inferenza. Diciamo che una dimostrazione è una dimostrazione derivabile meccanicamente se una proposizione segue logicamente da una base di conoscenza. Un teorema è una proposizione dimostrabile. L'algoritmo per derivare le conseguenze di una base di conoscenza prende il nome di procedura di dimostrazione.

Data una procedura, $KB \vdash g$ significa che g può essere dimostrato o derivato dalla knowledge base KB. La qualità di una procedura di dimostrazione può essere giudicata dal fatto che calcoli ciò che si intende calcolare. Una procedura di dimostrazione è corretta rispetto a una semantica se tutto ciò che può essere derivato da una base di conoscenza è una conseguenza logica della base di conoscenza. Una procedura di dimostrazione è completa rispetto a una semantica se esiste una dimostrazione di ogni conseguenza logica della base di conoscenza.

Vi sono due procedure per dimostrare le proposizioni definite: una procedura bottom-up e una procedura top-down. Nella procedura bottom-up si parte dimostrando atomi che sono stati già stabiliti, al contrario dell'approccio top-down il quale parte da una query e cerca di trovare le clausole che la supportano. L'approccio bottom-up consiste in una procedura forward chaining sulle clausole definite. L'idea generale si basa sulla regola di derivazione.

La procedura di dimostrazione bottom-up, ha una serie di caratteristiche. E' solida, ha una complessità lineare nella dimensione della base di conoscenza ed è un algoritmo completo.

Nella procedura di dimostrazione top-down si parte dalla query per determinare se questa è una conseguenza logica delle clausole definite nella KB. Generalmente questo processo prende il nome di risoluzione SLD. Data una clausola di risposta, l'algoritmo top-down seleziona un atomo nel corpo della clausola di risposta, definito sotto obiettivo.