04. Logica proposizionale e del primo ordine

Logica proposizionale

(vedi Linguaggi formali)
Composta da lettere $A = \left \{ a_1, \ldots , a_n \right \}$ che descrivono qualcosa nel mondo da rappresentare. Queste lettere sono connesse tra loro tramite connettivi logici $\left \{ \wedge, \vee , \neg , \rightarrow , \leftrightarrow \right \}$.

Teoria logica proposizionale

Un insieme di clausole (connessione di lettere, anche dette regole se scritte con una certa convenzione) che coinvolgono le lettere dell'insieme A. Può essere vista anche come una formula unica espressa in logica proposizionale.

Semantica di una teoria logica in forma proposizionale

E' data da un modello. Un modello è un sottoinsieme delle lettere presenti nella formula logica, quindi $M \subseteq A$. Se T è una teoria composta dalla connessione di lettere A, allora M è un modello per T se M soddifa (rende vere) tutte le clausole di T. In notazione compatta:

M è un modello di T se $M \models T$ (Cioè i modelli che soddisfano M, ovvero M stesso, permettono di dedurre o in altri termini soddisfano anche T)

Entailment o implicazione "semantica" o deduzione a partire da una teoria logica proposizionale

Una teoria proposizionale G implica una certa formula logica f se e solo se:

$\forall \ \mbox{modello} \ M \ \mbox{di G, ovvero:} \ \left ( M \models G \right ) \Rightarrow \left ( M \models f \right )$. Ovvero ogni modello di G (che quindi rende vera G) rende vera anche f.

Si può anche dire (è più scorrevole nel discorso) che f è deducibile da G.

Logica del primo ordine

Definizione elementi base: costanti, variabili, funtori, predicati, etc…

La logica proposizionale è un caso particolare della logica del primo ordine, dunque gli enunciati prima visti (semantica, modello, etc..) valgono anche per la logica del primo ordine.
Sostanzialmente nella logica del primo ordine le lettere della logica proposizionale non sono altro che predicati. In particolare le lettere della logica proposizionale sono predicati di arità1 0. Tuttavia spieghiamo il tutto per passi.
Gli elementi per costruire formule della logica del primo ordine sono i seguenti:

  • costanti : valori costanti, tipo '5'.
  • variabili : simboli che fanno le veci delle costanti, una variabile sarà sostituita con una particolare costante ma, finchè non viene sostituità, può assumere potenzialmente qualsiasi valore del dominio delle costanti. Di solito per indicare le variabili si usano $x_1, \ldots, x_n$
  • funtori o simboli di funzione: sono relazioni tra elementi del dominio delle costanti (e quindi delle variabili) e dei funtori stessi. Un funtore che non ha variabili nei suoi parametri indica una relazione fissa e quindi costante. Un funtore f coinvolge, come abbiam detto, gli elementi, quindi può avere un'arità diversa da zero. In generale la formula di un funtore è:
    $f \left ( e_1, \ldots, e_n \right )$ dove $e_i, \forall \ i \in \left \{ 1, \ldots, n \right \}$ è una variabile o una costante o un funtore a sua volta.
    nota: un funtore di arità 0 è come se fosse una costante (si ricollega al discorso sopra esposto).
    esempio: dog(mario()) è un funtore che esprime "il cane di mario" dove mario è una costante ed anche dog lo è poichè non compaiono variabili nei suoi argomenti.
  • termini: sono gli elementi che compaiono nei parametri dei funtori e dei predicati. Come abbiam già detto per i funtori, possono essere costanti, variabili, e funtori. Un termine dove non compaiono variabili è detto termine ground.
  • predicati: descrivono qualcosa nel mondo da rappresentare. Tipo "piove" traducibile con piove() (predicato di arità 0). I predicati hanno un'arità maggiore o uguale di 0 e gli argomenti dei predicati sono i termini.
    esempio: piace(sister(mario()), dog(friend(mario())) ) alla sorella di Mario piace il cane dell'amico di Mario (notare che la virgola indica l'and tra i predicati).
  • quantificatori: si applicano alle variabili e stabiliscono se un pezzo di formula logica deve essere vero per tutte (il "per ogni") le istanze di una variabile o per almeno una (lo "esiste") istanza. In notazione $\forall \ , \exists$.
  • Connettivi logici: uguali a quelli della logica proposizionale e si applicano solo ai predicati (anche perchè, lo ricordiamo, i predicati con arità 0 sono pari alle lettere della logica proposizionale).

Formule, teorie, programmi logici ground: sono formule, teorie, programmi logici (cioè composizione di predicati) "espanse" in tutte le istanze necessarie (a seconda delle variabili e delle variabili quantificate) dove non ci sono variabili. Ad esempio:
p(cost1) and p(cost2) and p(cost3) è una teoria (o formula o programma logico) ground poichè non ci sono costanti.
Altro esempio: forall x p(x) dove il dominio delle costanti è {1,2} , allora l'equivalente ground sarà insieme di {p(1), p(2)} .

Differenza di espressività tra logica del primo ordine e logica proposizionale

Con la logica proposizionale posso esprimere i problemi entro Co-NP, quindi molte cose non riesco ad esprimerle, ad esempio molti giochi sono oltre Co-NP. Con la logica del primo ordine non ho limiti poichè riesco, in modo complesso, a modellare la macchina di Turing. Cioè posso pensare di avere un funtore "testina", un funtore "posizioneSulNastro", etc…

Tradurre predicati ground in lettere della logica proposizionale, ritornare alla logica proposizionale.

Un predicato ground p(t1, … , tn) è traducibile in lettera della logica proposizionale in molti modi, il più banale è:

p_t1_terminiDit1_t2_terminiDit2_..._tn_terminiDitn

Se il predicato non è ground ma il dominio delle costanti è finito (l'universo di Herbrand), cioè anche se ci sono funtori questi non fanno esplodere l'universo di Herbrand2, allora posso comunque passare dalla logica di 1° ordine alla logica proposizionale come segue:

x \in {1,2,3}
p(x) //predicato, normalmente si omette la quantificazione universale quindi sarebbe "forall x p(x)"
-- trasformazione --
p(1) and p(2) and p(3)
//poichè per ogni x deve valere p, quindi ho la congiunzione dei predicati ground

Regole o clausole?

Le regole sono particolari clausole riscritte con il connettivo dell'implicazione come segue:

a <- b //se b allora a
-- è equivalente a --
not b or a

si ha infatti
a | b | a <- b | not b or a |
T | F |    T   |      T     |
T | T |    T   |      T     |
F | F |    T   |      T     |
F | T |    F   |      F     |

Inferenza classica, regole d'inferenza.

Si vuol dedurre solo ciò che è vero per tutti i modelli della teoria T (ovvero l'entailment). Cioè:

$T \models a \leftrightarrow \forall \ M \ \left ( M \models T \right ) \ \mbox{(per ogni modello di T)} \Rightarrow \left ( M \models a \right )$

Però in questo modo il costo di deduzione è elevato, poichè bisogna trovare ogni modello di T e poi verificare che sia un modello anche per 'a'. Allora invece di lavorare a livello di semantica (appunto con i modelli) si cerca di lavorare a livello di sintassi3 , sfruttando la struttura clausole della teoria T per vedere se si riesce a derivare la formula 'a'.

Modus ponens

E' una regola d'inferenza solo sintattica. Ci dice che se ho il sintagma (l'elemento sintattico) 'a' ed una regola $a \rightarrow b$ allora posso derivare il sintagma 'b'. E' solo una regola sintattica, verifica solo se esistono i pezzi richiesti per derivare un altro pezzo, ovviamente ciò è costruito, come si è detto, cercando di accordarsi con la semantica. Nota: 'a' e 'b' possono essere formule a loro volta.
A livello di notazione si ha:

(1)
\begin{align} \frac{a \ ; a \rightarrow b }{b} \end{align}

Dopo questa operazione otteniamo una teoria ${T}'$ che è pari a T più la formula derivata.
In questo modo si riesce a dire se la teoria T può derivare una data formula se, applicando più volte il modus ponens, si arriva a derivare la formula che si voleva derivare. Cioè:

$T \underset{r}{\rightarrow} {T}' \underset{r}{\rightarrow} {T}'' \underset{r}{\rightarrow} {T}'''$ dove la nostra formula da derivare 'a' è inclusa nell'ultima teoria, cioè $a \in {T}'''$, e la nostra regola d'inferenza è 'r'.

Il problema, come abbiam detto, è che è possibile che qualche derivazione non sia in accordo con la semantica.

Caratteristiche di una regola d'inferenza in accordo con la semantica. Correttezza e completezza.

Una regola d'inferenza in accordo con la semantica (sottointeso: sempre) deve rispettare le seguenti caratteristiche:

  • Corretta (sound)
  • Completa (complete)

R è sound (corretta) se: $\forall \ T, \forall \ a$ (con 'a' predicato, lettera o formula) è vero che:

(2)
\begin{align} T \underset{R}\vdash a \Rightarrow \left ( T \models a \right ) \end{align}

Cioè ciò che derivo con la regola d'inferenza ( $\underset{R}\vdash$) è semanticamente deducibile. (sostanzialmente se ciò che derivo è vero, dove 'vero' è tale rispetto alla semantica della teoria T)

R è completa se $\forall \ T, \forall \ a$ è vero che:

(3)
\begin{align} \left ( T \models a \right ) \Rightarrow T \underset{R}\vdash a \end{align}

Cioè se tutto ciò che è semanticamente deducibile è derivabile. (sostanzialmente se tutto ciò che è vero lo riesco a derivare)

Modus ponens rispetto alla logica proposizionale

Il modus ponens è sound rispetto alla logica proposizionale, ovvero si derivano solo cose vere, ma non è completo. Infatti:

(4)
\begin{align} T = \left \{ \begin{matrix} a \vee b \leftarrow \mbox{true} \\ c \leftarrow a \\ c \leftarrow b \end{matrix} \right. \end{align}

T in questo caso permette di derivare semanticamente 'c', ma il modus ponens non ci riesce, poichè riesce a derivare dalla prima regola 'a or b' ma, siccome la regola d'inferenza non scompone gli elementi sintattici, nessun'altra regola contiene 'a or b' come antecedente. Ci vorrebbe il Case based reasoning ovvero un ragionamento per casi, cioè avendo un or potremmo dire che è vera 'a' o 'b'.

Se limitiamo la teoria ad avere solo regole di Horn (sotto) allora il modus ponens è corretto e completo.

Regole di Horn

Regole nella forma: $A \leftarrow B$ dove A è un singolo predicato positivo, mentre B può essere una congiunzione di predicati positivi e/o negati. Quindi la prima formula della T vista prima non è in forma di Horn.

Principio o regola di risoluzione (vedi anche Ling. Form.)

In sostituzione al modus ponens si usa la regola di risoluzione che è corretta e completa per la logica proposizionale anche per teorie con regole non di Horn. Funziona come segue.
Date due clausole:

(5)
\begin{gather} a_1 \wedge a_2 \wedge \ldots \wedge a_m \rightarrow b_1 \wedge b_2 \wedge \ldots \wedge b_k \\ c_1 \wedge c_2 \wedge \ldots \wedge c_n \rightarrow a_i \wedge d_1 \wedge d_2 \wedge \ldots \wedge d_p \end{gather}

L'atomo (o singolo predicato) $a_i$ compare in testa ad una clausola ed in coda all'altra (la testa è la conseguenza di un'implicazione la coda è la premessa dell'implicazione) quindi si possono combinare le due clausole che elidono $a_i$ ottenendo una nuova (che non sostituisce le clausole precedenti) clausola:

(6)
\begin{align} a_1 \wedge a_2 \wedge \ldots \wedge a_{i-1} \wedge a_{i+1} \wedge \ldots \wedge a_m \wedge c_1 \wedge c_2 \wedge \ldots \wedge c_n \rightarrow b_1 \wedge b_2 \wedge \ldots \wedge b_k \wedge d_1 \wedge d_2 \wedge \ldots \wedge d_p \end{align}

Costo dell'inferenza classica

Supponiamo di avere una regola R corretta e completa per la logica in uso. Il problema rimane il costo di derivazione. Vorremmo derivare la formula in esame il più velocemente possibile. Abbiamo il problema: da quale sottoinsieme di formule della teoria T partiamo per derivare? Non sapendolo, potremmo derivare in modo breadth first (pag15r nozione2): applico R a tutte le fomule di T (ed è costossissimo) ed ottengo T' (togliendo i risultati di derivazione ridondanti) e poi continuo finchè la nuova teoria derivata è uguale a quella precedente.
Se la formula da derivare è una conseguenza della teoria prima o poi la derivo, se non è una conseguenza quando me ne accorgo?

Tutti questi problemi vengono amplificati se R non è corretta e completa.

Se T ha derivabilità finita (dopo tot applicazioni di R a tutte le formule delle teorie derivate da T non derivo più nulla) allora posso accorgermi quando la formula da derivare non si può derivare, ma se T ha una derivabilità molto grande (non diciamo infinita ma davvero molto grande) quando posso presumere che la formula in questione non sia derivabile?

Discorsi simili valgono per tutti i linguaggi di rappresentazione della conoscenza che ammettono problemi indecidibili (come quello della non derivazione sopra esposto).

Cosa non permette, la logica del primo ordine, di fare agevolmente?

La logica di 1° ordine, essendo turning completa, permette di fare praticamente tutto ciò che riusciamo a fare in termini di algoritmi. Il problema è che rappresenta alcuni problemi in modo molto macchinoso:

  • i ragionamenti probabilistici diventano complessi.
  • è monotona (la conoscenza cresce e non viene ritrattata) e simulare la non monotonicità è complesso. Esempio di non monotonicità: si assume che tutti i conigli siano bianchi fino a prova contraria (al primo coniglio nero si ritratta questa conoscenza).
  • il concetto di tempo è complesso da implementare.
  • le credenze sono complesse da rappresentare (es: "io ritengo che a sia vero").
Unless otherwise stated, the content of this page is licensed under Creative Commons Attribution-ShareAlike 3.0 License