succ prec indice

Risoluzione Inversa

L'induzione puo' essere vista come il processo inverso alla deduzione. La deduzione permette infatti di derivare conclusioni specifiche da premesse generali, mentre l'induzione cerca di risalire alle premesse, partendo dall'osservazione di casi speciali (esempi). Questo ha condotto a tentativi di inversione del procedimento di risoluzione, alla base dei sistemi di deduzione automatica.
Un' importante contributo in questo campo e' stato fornito da Muggleton e Buntine con l'introduzione degli operatori V e W, e la realizzazione del sistema CIGOL .

Risoluzione

Introdotta nel 1965 da un fondamentale lavoro di Robinson, consiste nella
applicazione sistematica nella dimostrazione di una tesi, della regola di inferenza

    not a -> b,        b -> c                            a or b,        not b or c
_______________________    oppure    ______________________
                not a -> c                                                a or c

Rappresentando le formula in forma di clausole, ovvero come disgiungioni di letterali, la regola di risoluzione puo' venire riscritta come

W = { w₁, ... , w_k , q } , V = { v₁, ... , v_l , not q } _{_________________________________________________________________}
{ w₁, ... , w_k , v₁, ... , v_l }

Nel caso di formule del primo ordine l'ugualianza di termini e' da intendere a meno di "unificazione", ovvero per una coppia di atomi unificabili a₁, a₂, deve esistere una sostituzione theta tale che

a₁.theta = a₂.theta

La risoluzione rappresenta una generalizzazione della regola-MP (modus-ponens), derivabile da questa nel modo seguente

    a,        a -> b                                        Vero -> a,    a -> b
_______________                                ____________________
            b                                                            Vero -> b

L'inferenza con risoluzione viene applicata alla refutazione (reductio ad absurdum) per dimostrare la verita' di una tesi attraverso la ricerca della contraddorieta' della propria negazione. Se la verita' di una tesi non puo' venire dimotrata in questo modo, in un modello di Herbrand (mondo chiuso), la tesi viene dichiarata falsa.

Il processo di risoluzione considera ad ogni passo una coppia di clausole a cui applicare la regola di inferenza. Il procedimento viene detto "lineare", quando in ogni passo una delle clausole della coppia deve essere costituita dalla risolvente del passo precedente, mentre la seconda puo' essere o una premessa iniziale o una clausola gia' derivata. Se oltre a considerare la clausola ottenuta al passo precedente, la scelta della seconda clausola e' limitata alle sole premesse iniziali, il precedimento viene definito ad "input-lineare".
La risoluzione ad "input-lineare" non risulta essere un procedimento di dimostrazione completa per clausole generiche, mentre e' applicabile in modo completo a clausole di Horn (disgiunzione di predicati con al piu' un disgiunto positivo).

La selezione della clausola da considerare in un passo di risoluzione potrebbe influenzare negativamente l'esito della dimostrazione in presenza di tesi negate non ground.Un criterio "sicuro" (safe) puo' essere introdotto nel modo seguente: non selezionare per la risoluzione una sottoclausola negata non ground, trattare completamente una sottoclausola negata ground prima di considerare le rimanenti

Sostituzione Inversa

Data una "formula-ben-fomata" W, si dice sostituzione inversa theta^-1 di una sostituzione theta , una sostituzione che conduca da termini di W.theta a variabili, in modo tale che (W.theta).theta^-1= W.

Esempio:

Sia c la clausola

c = figlia( X,Y ) :- femmina( X ), genitore( Y,X ).

sia theta = { X/maria, Y/anna }, e c' la clausola ottenuta applicando theta a c (c.theta)

c' = figlia( maria, anna ) :- femmina( maria ), genitore( anna, maria ).

applicando c' la sostituzione inversa theta^-1 = { maria/X, anna/Y }, si ritrova la clausola c originale

c'.theta^-1 = c = figlia( X,Y ) :- femmina( X ), genitore( Y,X ).

Inversione

Il procedimento di risoluzione inversa, come descritto da Muggleton e Buntine, consiste nell'applicazione ripetuta degli operatori V e W in modo Bottom-up

Operatore-V

Data una coppia di clausole c e r, mediante sostituzione inversa, l'operatore-V ricerca una clausola h, tale che r sia deducibile da c e h.

op-V( c, r ) = h tale che c, h |- r ( r :- h,c )

Esempio

sia r la clausola

r = figlia( maria, anna )

la conoscenza di fondo B comprenda le clausole b₁ e b₂

b₁ = genitore( maria, anna )
b₂ = femmina( maria )

l'operatore V, applicato due volte con le sostizioni inverse theta₁^-1 = { anna/Y } e theta₂^-1 = { maria/X } produrra' la clausola h

h = figlia( X,Y ) :- femmina(X), genitore( Y,X ).

infatti

h' = op-V( b₁,r ) = r.theta₁^-1= figlia( maria,Y ) :- genitore( Y, maria ).
h = op-V( b₂,h' ) = h'.theta₂^-1= figlia( X,Y ) :- genitore( Y, Y ).

dove

r :- b₁,b₂,h

Un problema con l'operatore-V e' che date c e r la clausola h = op-V(c,r) non risulta in generale univocamente determinata, infatti op-V(c,r) effettivamente identifica l'insieme delle clausole che godono della proprieta' c, h |- r .

L'operatore-V viene anche chiamato "operatore di assorbimento".

Opeatore-W

In alcuni casi, potrebbe essere necessario introdurre nuovi predicati per ottenere una migliore descrizione degli esempi, cosa non possibile utizzando il solo operatore-V.
A questo scopo viene introdotto un nuovo operatore, denominato W per l'analogia con la struttura dell'albero di derivazione relativo.
Date due istanze r₁e r_{2 ,}espresse utilizzando un insieme di predicati { p₁,..., p_k}, l'operatore-W determina tre clausole c₁,c₂e c₃, espresse utilizzando l' insieme di predicati { p₁,..., p_k} piu' un nuovo predicato p', tali che r₁sia derivabile da { c₁,c₂}, r₂sia derivabile da { c₂,c₃ }, ed, in definitiva la coppia r₁e r₂sia derivabile da {c₁,c₂,c₃}.

Esempio

siano r₁e r₂

r₁= nonno( X,Y ) :- padre( X,Z ), padre( Z,Y ).
r₂= nonno( a,b ) :- padre( a,c ), madre( c,b ).

le clausole c₁,c₂,c₃ottenute dall'operatore-W introducendo il nuovo predicato p'=genitore(X,Y) sono

c₁= genitore( Z,Y ) :- padre( Z,Y ).
c₂= nonno( X,Y ) :- padre( X,Z ), genitore( Z,Y ).
c₃= genitore( c,b ) :- madre( c,b ).

L'operatore-W viene anche chiamato "operatore di intra-costruzione".

Minimalita'

La descriozione degli operatori V e W non affronta il problema di determinare quali clausole siano piu' indicate per i vari passi di inversione. Muggleton (1991) propone a questo scopo di unificare il concetto di "generalizzazione relativa meno generica" alla tecnica di risoluzione inversa, introducendo i cocetti di "risoluzione inversa meno generica" e di "sostituzione inversa meno generica". Rispetto a questi, il risultato dell'esempio relativo all'operatore-V sarebbe stato

h = figlia( maria,anna ) :- femmina(maria), genitore( anna,maria ).

succ prec indice