1 \chapter{Strumenti di dimostrazione: Logica Proposizionale}
6 Gli utenti di \HOL{} possono creare i loro propri strumenti di dimostrazione
9 di tipo \ml{thm}. In questo capitolo, � descritto un esempio reale.
12 di programmazione della dimostrazione. La prima implementazione � quella ovvia, ma
13 � inefficiente a causa del metodo di `forza bruta' utilizzato. La seconda
14 implementazione tenta di essere molto pi� intelligente.
18 Il problema da risolvere � quello di decidere la verit� di una formula
29 dove le variabili $v$ sono tutte di tipo booleano, e dove il
33 \section{Metodo 1: Tabelle di verit�}
37 Il primo metodo che deve essere implementato � il metodo di forza bruta di tentare
38 tutte le combinazioni booleane possibili. L'unico vero vantaggio di questo approccio
58 di fatto gi� dimostrato nella teoria \theoryimp{bool}.)
60 Il prossimo, e ultimo passo, � di riscrivere con questo teorema:
96 \ml{tautLib.TAUT\_CONV} incorporata nel sistema risolve il problema di sopra
98 reale in questa soluzione � che richiede di scrivere una sola riga. Questa �
99 un'illustrazione generale del fatto che gli strumenti di alto livello di \HOL{},
101 di compiti di dimostrazione.
106 decidere la soddisfacibilit� di formule proposizionali in CNF
109 dalle nostre formule di input, il nostro compito pu� essere visto come determinare
110 la validit� di una formula proposizionale. Testare la negazione di una tale
124 arbitrarie in CNF{}, e per poi decidere la soddisfacibilit� di queste
140 (Il teorema restituito da \ml{toCNF} uguaglier� il termine di input a
145 Prima di guardare all'implementazione di queste funzioni, dovremo
156 originaria. Entrambe la manipolazioni di termini richieste si possono fare
160 forme di termini associate con quella teoria.)
169 La funzione \ml{strip\_forall} spoglia un termine di tutte le sue quantificazioni
172 termine di tipo \holtxt{bool} e restituisce il termine corrispondente alla sua
175 Usando queste funzioni, � facile vedere come saremo in grado di prendere
178 usare i risultati di queste chiamate. La chiamata a \ml{toCNF}  restituir� un
186 un'applicazione di \ml{TRANS} a questo e al teorema mostrato di sopra
187 deriver� la formula $\vdash \neg\varphi = F$. Al fine di derivare il
188 risultato finale, avremo bisogno di trasformare questo in $\vdash\varphi$. Questo
220 $\phi\vdash \holtxt{F}$ in $\vdash \phi = \holtxt{F}$ � questione di
221 richiamare \ml{DISCH} e poi di riscrivere con il teorema incorporato
226 Mettendo tutto ci� che sta di sopra insieme, possiamo scrivere la nostra funzione wrapper,
258 Quando l'argomento di \ml{spec} non � quantificato universalmente, questo significa
266 livello principale di un termine. Questi usi di \ml{REWR\_CONV} sono fatti con
275 Una formula in Forma Normale Congiuntiva � una congiunzione di disgiunzioni
276 di letterali (cio� o variabili, o variabili negate). E' possibile
290 incremento esponenziale nella dimensione di una formula. (Si consideri di usarli
292 di congiunzioni di letterali, in CNF{}.)
294 Un approccio migliore � di convertire in ci� che � conosciuta come una ``CNF
307 formula in CNF{}. Con esempio piccolo come questo, la formula � di fatto
308 pi� grande di quella prodotto dalla traduzione ingenua, ma con esempi
311 ingenuamente di quando usando \ml{defCNF}, e la traduzione richiede 150
314 Ma cosa facciamo di queste variabili quantificate esistenzialmente extra? Di fatto,
317 verdetto di insoddisfacibilit� della forma $\vdash \varphi' = \holtxt{F}$, o una
339 \ml{DEF\_CNF\_VECTOR\_CONV}. Al posto di un output della forma
351 dimostrazione abbozzata di sopra. E fino a quando non richiediamo che i letterali siano
356 Sfortunatamente per uniformit�, in casi semplici, le funzioni di conversione
358 esistenziale del tutto. Questo rende la nostra implementazione di \ml{DPLL}
361 funzione \ml{transform} che trasformer� un risultato di insoddisfacibilit�
364 di sopra. Altrimenti, la trasformazione pu� essere la funzione identit�,
389 \ml{CoreDPLL} di sopra). Il codice di sopra usa \ml{REWR\_CONV} con il
392 le uguaglianza di primo livello di un teorema. Infine,
410 di base ``tabelle di verit�'' che abbiamo gi� visto. Come con quella
415 bisogno di controllare anche cosa accade se alla stessa variabile � dato il
416 valore di verit� opposto. In secondo luogo, DPLL fa una certa attenzione a selezionare delle variabili
419 spazio di ricerca.
424 forma di una funzione da termini a termini). Mentre la ricerca DPLL per
427 avr� bisogno di prendere un termine (la formula corrente) e un contesto (l'assegnazione
429 naturale come un insieme di equazioni, dove ciascuna equazione � o either $v =
441 risultato di semplificare $\phi$ sotto l'assunzione aggiuntiva
448 $\psi\vdash\psi$, dove $\psi$ � la nuova assunzione. L'azione di
470 di lookup per quella map finita.
487 La funzione \ml{foldthis} di sopra aggiunge le equazioni che sono archiviate come
504 che uguaglia l'input a falso, c'� bisogno di fare di pi�. Se questa � la
530 di alto livello, nella Figura~\ref{fig:coredpll}.
584 senza accrescere la dimensione del problema. Il processo di
585 eliminare clausole unitarie � di solito chiamato ``unit propagation''.
586 La unit propagation di solito non � pensata come un'operazione
587 di case splitting, ma eseguirla in questo modo render� il nostro codice pi� semplice.
590 variabile su cui eseguire lo split � molto pi� di una magia nera. Qui
592 pi� di frequente. La nostra funzione \ml{find\_splitting\_var} prende una formula
610 Questa funzione lavora passando una lista di clausole alla funzione
633 L'uso di un albero binario per archiviare dati variabili rende efficiente
652 migliori rispetto all'implementazione con le tavole di verit�. Per esempio, la
679 (Se si desidera la velocit� reale, la funzione incorporata \ml{tautLib.TAUT\_PROVE} esegue ci� che sta sopra in meno di un centesimo di secondo, usando uno strumento esterno per generare la dimostrazione di insoddisfacibilit�, e per poi tradurre quella dimostrazione indietro in HOL.)
686 una variabile o la negazione di una variabile. Questo rende \ml{DPLL\_UNIV}
687 poco facile da usare quando viene ad essere usata come parte della dimostrazione di
692 \paragraph{Mitigare il Requisito di Quantificazione}  Il primo passo �
693 permettere formule che non sono chiuse. Al fine di trasmettere una formula
698 falsa, allora non possiamo concludere niente di pi� e dovremo sollevare
701 Il codice che implementa questo � mostrato di sotto:
721 Possiamo fare meglio di \ml{nonuniv\_wrap}: piuttosto che quantificare solamente
724 variabile o la negazione di una variabile in una nuova variabile. Prima
744 Si noti che non abbiamo tentato esplicitamente di separare le negazioni
781 un teorema che uguaglia l'input originale a vero. (Se il termine di input non
782 � un'istanza di una formula proposizionale valida, la chiamata a
789 	(entrambi i rami dei termini devono essere di tipo booleano).

Indexes created Tue Sep 03 12:52:19 MDT 2024