Calcolo della risoluzione con raffinamento della sussunzione
Il problema che presento si può trovare a pagina 175-6 del libro Introduzione alla Logica Formale di Lolli. Per chi non ce l'ha, ecco i dati utili, allo scopo anche di richiamare i concetti.
Calcolo della risoluzione con la restrizione della sussunzione.
$S$ indica un insieme di clausole $C$ (clausola = disgiunzione di letterali), $L$ un letterale di una clausola e $L^c$ il complementare del letterale $L$: un letterale quindi rappresenta una lettera proposizionale o la sua negazione. Le clausole sono rappresentate come insiemi di letterali; è ammessa la clausola vuota (zero letterali), denotata da $\square$.
Regola del calcolo, la Risoluzione, ovvero dalle premesse $C_1 vv L$ e $C_2 vv L^c$ (denotate rispettivamente anche con $C_1 \uu {L}$ e $C_2 \uu {L^c}$) segue la clausola cosiddetta risolvente, $C_1 vv C_2$.
Una derivazione da $S$ nel calcolo in questione è una sequenza di clausole o appartenenti a $S$, o derivanti dall'applicazione della regola di cui sopra a due clausole che precedono nella sequenza. Se una derivazione termina con la clausola vuota, la derivazione è anche detta una refutazione (per risoluzione) di $S$.
Si assume, per ogni clausola di $S$, che per ogni suo letterale $L$ esista almeno un'altra clausola di $S$ a cui appartiene il letterale $L^c$.
$S^L = {C-{L^c}:C \in S \text{ e } L \notin C}$
$S^{L^c} = {C-{L}:C \in S \text{ e } L^c \notin C}$
LEMMA 1. $S$ è insoddisfacibile se e solo se sia $S^L$ che $S^{L^c}$ sono insoddisfacibili. [Dimostrazione omessa.]
LEMMA 2. Il calcolo della risoluzione è completo [ovvero $S$ insoddisfacibile implica $\vdash \square$].
[Si dimostra per induzione sul numero di coppie di letterali $L$ e $L^c$ presenti in $S$, utilizzando il lemma 1]
Da qui in poi riporto direttamente dalle pagine del testo citato.
Un'altra restrizione che si può applicare sia all'inizio su $S$ sia nella produzione di clausole con la risoluzione è la seguente: se in $S$ occorrono due clausole $C$ e $C^{\prime}$ con $C\subeC^{\prime}$, allora $C^{\prime}$ si può eliminare, osservando che $S$ è insoddisfacibile se e solo se $S-{C^{\prime}}$ è insoddisfacibile. [Ometto la breve prova di questo fatto.]
Si dice che una clausola $C$ sussume una clausola $C'$ se $C\subeC^{\prime}$. Da un insieme $S$ si possono eliminare le clausole sussunte da altre clausole di $S$.
La restrizione della sussunzione è la restrizione che vieta di eseguire risoluzioni la cui risolvente sia una clausola sussunta da una clausola o dell'insieme originario, o prodotta dalle risoluzioni precedenti.
LEMMA 3. Il calcolo della risoluzione con la restrizione della sussunzione è completo.
Dimostrazione. Ammesso che $S^L$ e $S^{L^c}$ abbiano refutazioni che rispettano la restrizione, quando si reintroduce $L^c$ (e rispettivamente $L$) le nuove clausole $C \uu {L^c}$ potrebbero essere sussunte al massimo da un'altra $C$, indipendente, non ottenuta per cancellazione di $L^c$, visto che per ipotesi induttiva $C$ non è sussunta da altre; ma se le sussunzioni sono eliminate da $S$ e in una derivazione ogni clausola è scritta una volta sola questo non può succedere (o si può fare in modo che non succeda).
Qualcuno è in grado di spiegare il nesso col resto del discorso, della parte evidenziata in rosso nella dimostrazione? Io non riesco assolutamente a capirlo (alla luce delle definizioni fornite).
Calcolo della risoluzione con la restrizione della sussunzione.
$S$ indica un insieme di clausole $C$ (clausola = disgiunzione di letterali), $L$ un letterale di una clausola e $L^c$ il complementare del letterale $L$: un letterale quindi rappresenta una lettera proposizionale o la sua negazione. Le clausole sono rappresentate come insiemi di letterali; è ammessa la clausola vuota (zero letterali), denotata da $\square$.
Regola del calcolo, la Risoluzione, ovvero dalle premesse $C_1 vv L$ e $C_2 vv L^c$ (denotate rispettivamente anche con $C_1 \uu {L}$ e $C_2 \uu {L^c}$) segue la clausola cosiddetta risolvente, $C_1 vv C_2$.
Una derivazione da $S$ nel calcolo in questione è una sequenza di clausole o appartenenti a $S$, o derivanti dall'applicazione della regola di cui sopra a due clausole che precedono nella sequenza. Se una derivazione termina con la clausola vuota, la derivazione è anche detta una refutazione (per risoluzione) di $S$.
Si assume, per ogni clausola di $S$, che per ogni suo letterale $L$ esista almeno un'altra clausola di $S$ a cui appartiene il letterale $L^c$.
$S^L = {C-{L^c}:C \in S \text{ e } L \notin C}$
$S^{L^c} = {C-{L}:C \in S \text{ e } L^c \notin C}$
LEMMA 1. $S$ è insoddisfacibile se e solo se sia $S^L$ che $S^{L^c}$ sono insoddisfacibili. [Dimostrazione omessa.]
LEMMA 2. Il calcolo della risoluzione è completo [ovvero $S$ insoddisfacibile implica $\vdash \square$].
[Si dimostra per induzione sul numero di coppie di letterali $L$ e $L^c$ presenti in $S$, utilizzando il lemma 1]
Da qui in poi riporto direttamente dalle pagine del testo citato.
Un'altra restrizione che si può applicare sia all'inizio su $S$ sia nella produzione di clausole con la risoluzione è la seguente: se in $S$ occorrono due clausole $C$ e $C^{\prime}$ con $C\subeC^{\prime}$, allora $C^{\prime}$ si può eliminare, osservando che $S$ è insoddisfacibile se e solo se $S-{C^{\prime}}$ è insoddisfacibile. [Ometto la breve prova di questo fatto.]
Si dice che una clausola $C$ sussume una clausola $C'$ se $C\subeC^{\prime}$. Da un insieme $S$ si possono eliminare le clausole sussunte da altre clausole di $S$.
La restrizione della sussunzione è la restrizione che vieta di eseguire risoluzioni la cui risolvente sia una clausola sussunta da una clausola o dell'insieme originario, o prodotta dalle risoluzioni precedenti.
LEMMA 3. Il calcolo della risoluzione con la restrizione della sussunzione è completo.
Dimostrazione. Ammesso che $S^L$ e $S^{L^c}$ abbiano refutazioni che rispettano la restrizione, quando si reintroduce $L^c$ (e rispettivamente $L$) le nuove clausole $C \uu {L^c}$ potrebbero essere sussunte al massimo da un'altra $C$, indipendente, non ottenuta per cancellazione di $L^c$, visto che per ipotesi induttiva $C$ non è sussunta da altre; ma se le sussunzioni sono eliminate da $S$ e in una derivazione ogni clausola è scritta una volta sola questo non può succedere (o si può fare in modo che non succeda).
Qualcuno è in grado di spiegare il nesso col resto del discorso, della parte evidenziata in rosso nella dimostrazione? Io non riesco assolutamente a capirlo (alla luce delle definizioni fornite).
Risposte
Anch'io ebbi a che fare con questo libro, e questa restrizione limitata al caso proposizonale non è molto chiara. Il motivo dovrebbe essere questo, che se non venissero eliminate potrebbe accadere che in una delle refutazioni dell'ipotesi induttiva (p. es. quella in $S^L$), si sia utilizzata una clausola sussunta da un'altra (in $S$), ma qui legittimamente, perché le due clausole differiscono solo per il letterale $L^c$, per cui in $S^L$ non sussisterebbe la sussunzione (visto che verrebbero a coincidere e si ridurrebbero a una sola); reintroducendo poi il letterale, resterebbe violata la parte della definizione che stabilisce la condizione che non debba esservi sussunzione da parte di clausole dell'insieme originario (si poteva esprimere più semplicemente in altro modo dicendo che nelle refutazioni induttive ipotizzate si devono usare clausole di $S$ non strettamente sussunte da altre dell'insieme). In realtà questa spiegazione, come tu giustamente hai notato, non regge alla luce delle definizioni date nel testo, infatti la definizione di sussunzione fa riferimento solo alle clausole ottenute per risoluzione, non a quelle dell'insieme di origine. Non incoerente sarebbe stato invece il discorso se si fosse anche specificato nelle richieste della definizione "l'eliminazione di sussunzioni nell'insieme di partenza".
Accedi a tutti gli appunti
Tutor AI: studia meglio e in meno tempo