xref: /seL4-l4v-master/HOL4/Manual/Translations/IT/Tutorial/proof-tools.tex

\chapter{Strumenti di dimostrazione: Logica Proposizionale}
\label{chap:proof-tools}

\newcommand{\naive}{na\"\i{}ve}

Gli utenti di \HOL{} possono creare i loro propri strumenti di dimostrazione
combinando le regole e le tattiche predefinite. La disciplina dei tipi \ML{}
assicura che solo metodi logicamente validi possono essere usati per creare valori
di tipo \ml{thm}. In questo capitolo, � descritto un esempio reale.

Sono date due implementazioni dello strumento per illustrare vari stili
di programmazione della dimostrazione. La prima implementazione � quella ovvia, ma
� inefficiente a causa del metodo di `forza bruta' utilizzato. La seconda
implementazione tenta di essere molto pi� intelligente.
Sono anche discusse estensioni agli strumenti per permettere un'applicabilit�
pi� generale.

Il problema da risolvere � quello di decidere la verit� di una formula
chiusa della logica proposizionale. Una tale formula ha la forma generale
\[
\begin{array}{ccl}
\varphi & ::= & v \;|\;\neg\varphi\;|\;\varphi
\land \varphi \;|\; \varphi \lor \varphi \;|\; \varphi \Rightarrow
\varphi\;|\;\varphi = \varphi
\\[1ex]
\mathit{formula} &::= & \forall \vec{v}. \;\varphi
\end{array}
\]
dove le variabili $v$ sono tutte di tipo booleano, e dove il
quantificatore universale al livello pi� esterno cattura tutte le
variabili libere.

\section{Metodo 1: Tabelle di verit�}

\setcounter{sessioncount}{0}

Il primo metodo che deve essere implementato � il metodo di forza bruta di tentare
tutte le combinazioni booleane possibili. L'unico vero vantaggio di questo approccio
� che � eccezionalmente semplice da implementare. Prima dimostreremo
il teorema motivante:
\begin{hol}
\begin{verbatim}
   val FORALL_BOOL = prove(
     ``(!v. P v) = P T /\ P F``,
     SRW_TAC [][EQ_IMP_THM] THEN Cases_on `v` THEN SRW_TAC [][]);
\end{verbatim}
\end{hol}
La dimostrazione procede dividendo il goal in due met�, mostrando
\[
(\forall v. \;P(v))\Rightarrow P(\top) \land P(\bot)
\]
(Goal che � automaticamente mostrato dal semplificatore), e
\[
P(\top) \land P(\bot) \Rightarrow P(v)
\]
per una variabile booleana arbitraria $v$. Dopo lo splitting dei casi su $v$,
le assunzioni sono poi sufficienti a mostrare il goal. (Questo teorema �
di fatto gi� dimostrato nella teoria \theoryimp{bool}.)

Il prossimo, e ultimo passo, � di riscrivere con questo teorema:
\begin{hol}
\begin{verbatim}
   val tautDP = SIMP_CONV bool_ss [FORALL_BOOL]
\end{verbatim}
\end{hol}

Questo permette il seguente

\begin{session}
\begin{verbatim}
- tautDP ``!p q. p /\ q /\ ~p``;
> val it = |- (!p q. p /\ q /\ ~p) = F : thm

- tautDP ``!p. p \/ ~p``
> val it = |- (!p. p \/ ~p) = T : thm
\end{verbatim}
\end{session}
e anche il pi� leggermente intimidatorio
\begin{session}
\begin{verbatim}
- time tautDP
     ``!p q c a. ~(((~a \/ p /\ ~q \/ ~p /\ q) /\
                    (~(p /\ ~q \/ ~p /\ q) \/ a)) /\
                   (~c \/ p /\ q) /\ (~(p /\ q) \/ c)) \/
                 ~(p /\ q) \/ c /\ ~a``;
runtime: 0.147s,    gctime: 0.012s,     systime: 0.000s.
> val it =
    |- (!p q c a.
          ~(((~a \/ p /\ ~q \/ ~p /\ q) /\ (~(p /\ ~q \/ ~p /\ q) \/ a)) /\
            (~c \/ p /\ q) /\ (~(p /\ q) \/ c)) \/ ~(p /\ q) \/ c /\ ~a) =
       T : thm
\end{verbatim}
\end{session}

Questo � un algoritmo terribile per risolvere questo problema. La funzione\linebreak
\ml{tautLib.TAUT\_CONV} incorporata nel sistema risolve il problema di sopra
molto pi� velocemente. L'unico merito
reale in questa soluzione � che richiede di scrivere una sola riga. Questa �
un'illustrazione generale del fatto che gli strumenti di alto livello di \HOL{},
in particolare il semplificatore, possono fornire prototipi veloci per una variet�
di compiti di dimostrazione.

\section{Metodo 2: l'Algoritmo DPLL}

Il metodo Davis-Putnam-Loveland-Logemann~\cite{DPLL-paper} per
decidere la soddisfacibilit� di formule proposizionali in CNF
(Conjunctive Normal form) � una tecnica potente, ancora oggi usata nei
risolutori dell'ultima generazione. Se eliminiamo i quantificatori universali
dalle nostre formule di input, il nostro compito pu� essere visto come determinare
la validit� di una formula proposizionale. Testare la negazione di una tale
formula per la soddisfacibilit� � un test per la validit�: se la negazione
della formula � soddisfacibile, allora non � valida (l'assegnazione
che soddisfa render� l'originale falsa): se la negazione della formula �
insoddisfacibile, allora la formula � valida (nessuna assegnazione la pu� rendere
falsa).

\smallskip
\noindent
(Il codice sorgente per questo esempio � disponibile nel file \texttt{examples/dpll.sml}.)

\subsection*{Preliminari}

Per iniziare, assumiamo che abbiamo gi� del codice per convertire formule
arbitrarie in CNF{}, e per poi decidere la soddisfacibilit� di queste
formule. Assumiamo inoltre che se l'input all'ultima procedura �
insoddisfacibile, allora restituir� un teorema della forma
\[ \vdash \varphi = \holtxt{F}
\]
o se � soddisfacibile, allora restituir� un'assegnazione che soddisfa,
un mapping da variabili a booleani. Questo mapping sar� una funzione da
variabili \HOL{} a uno dei termini \HOL{} \holtxt{T} o \holtxt{F}.
Cos�, assumeremo
\begin{hol}
\begin{verbatim}
   datatype result = Unsat of thm | Sat of term -> term
   val toCNF : term -> thm
   val DPLL : term -> result
\end{verbatim}
\end{hol}
(Il teorema restituito da \ml{toCNF} uguaglier� il termine di input a
un altro in CNF{}.)

\smallskip
\noindent
Prima di guardare all'implementazione di queste funzioni, dovremo
considerare
\begin{itemize}
\item come trasformare i nostri input per adattarsi alla funzione; e
\item come usare gli output dalle funzioni per produrre i nostri risultati
	desiderati
\end{itemize}

Stiamo assumendo che il nostro input sia una formula quantificata universalmente.
Entrambe le procedure CNF e DPLL si aspettano formule senza quantificatori.
Vogliamo anche passare a queste procedure la negazione della formula
originaria. Entrambe la manipolazioni di termini richieste si possono fare
con le funzioni che si trovano nella struttura \ml{boolSyntax}. (in generale,
le teorie importanti (come \theoryimp{bool}) sono accompangnate da
moduli \ml{Syntax} che contengono funzioni per manipolare le
forme di termini associate con quella teoria.)

In questo caso abbiamo bisogno delle funzioni
\begin{hol}
\begin{verbatim}
   strip_forall : term -> term list * term
   mk_neg       : term -> term
\end{verbatim}
\end{hol}
La funzione \ml{strip\_forall} spoglia un termine di tutte le sue quantificazioni
universali pi� esterne, restituendo la lista delle variabili spogliate
e il corpo della quantificazione. La funzione \ml{mk\_neg} prende un
termine di tipo \holtxt{bool} e restituisce il termine corrispondente alla sua
negazione.

Usando queste funzioni, � facile vedere come saremo in grado di prendere
$\forall\vec{v}.\;\varphi$ come input, e passare il termine $\neg\varphi$
alla funzione \ml{toCNF}. Una domanda pi� significativa � come
usare i risultati di queste chiamate. La chiamata a \ml{toCNF}  restituir� un
teorema
\[
\vdash \neg\varphi = \varphi'
\]
La formula $\varphi'$ � ci� che passeremo poi a \ml{DPLL}. (Possiamo
estrarla usando le funzioni \ml{concl} e \ml{rhs}.) Se
\ml{DPLL} restituisce il teorema $\vdash \varphi' = \holtxt{F}$,
un'applicazione di \ml{TRANS} a questo e al teorema mostrato di sopra
deriver� la formula $\vdash \neg\varphi = F$. Al fine di derivare il
risultato finale, avremo bisogno di trasformare questo in $\vdash\varphi$. Questo
si ottiene meglio fornendo un teorema fatto su misura che incorpora l'uguaglianza (non
ce n'� gi� uno simile nel sistema):
\begin{hol}
\begin{verbatim}
   val NEG_EQ_F = prove(``(~p = F) = p``, REWRITE_TAC []);
\end{verbatim}
\end{hol}
Per trasformare $\vdash \varphi$ in $\vdash (\forall
\vec{v}.\;\varphi) = \holtxt{T}$, eseguiremo la seguente dimostrazione:
\[
\infer[\texttt{\scriptsize EQT\_INTRO}]{
  \vdash (\forall \vec{v}.\;\varphi) = \holtxt{T}}{
  \infer[\texttt{\scriptsize GENL}(\vec{v})]{\vdash \forall \vec{v}.\;\varphi}{
    \vdash \varphi
  }
}
\]
L'altra possibilit� � che \ml{DPLL}  restituir� un'assegnazione che soddisfa
dimostrando che $\varphi'$. Se questo �
il caso, vogliamo mostrare che $\forall\vec{v}.\;\varphi$ � falsa.
Possiamo fare questo assumendo questa formula, e specializzando le
variabili quantificate universalmente in linea con il mapping fornito. In
questo modo, sar� possibile produrre il teorema
\[
\forall \vec{v}.\;\varphi \vdash \varphi[\vec{v} := \mbox{\emph{satisfying
  assignment}}]
\]
Poich� non ci sono variabili libere in $\forall\vec{v}.\;\varphi$, la
sostituzione produrr� una formula booleana completamente ground. Questa
si riscriver� direttamente a \holtxt{F} (se l'assegnazione
rende $\neg\varphi$ vero, deve rendere $\varphi$ falso). Trasformare
$\phi\vdash \holtxt{F}$ in $\vdash \phi = \holtxt{F}$ � questione di
richiamare \ml{DISCH} e poi di riscrivere con il teorema incorporato
\ml{IMP\_F\_EQ\_F}:
\[
\vdash \forall t.\;t \Rightarrow \holtxt{F} = (t = \holtxt{F})
\]
Mettendo tutto ci� che sta di sopra insieme, possiamo scrivere la nostra funzione wrapper,
che chiameremo \ml{DPLL\_UNIV}, con il suffisso \ml{UNIV}
che ci ricorda che l'input deve essere quantificato universalmente.
\begin{hol}
\begin{verbatim}
   fun DPLL_UNIV t = let
     val (vs, phi) = strip_forall t
     val cnf_eqn = toCNF (mk_neg phi)
     val phi' = rhs (concl cnf_eqn)
   in
     case DPLL phi' of
       Unsat phi'_eq_F => let
         val negphi_eq_F = TRANS cnf_eqn phi'_eq_F
         val phi_thm = CONV_RULE (REWR_CONV NEG_EQ_F) negphi_eq_F
       in
         EQT_INTRO (GENL vs phi_thm)
       end
     | Sat f => let
         val t_assumed = ASSUME t
         fun spec th =
             spec (SPEC (f (#1 (dest_forall (concl th)))) th)
             handle HOL_ERR _ => REWRITE_RULE [] th
       in
         CONV_RULE (REWR_CONV IMP_F_EQ_F) (DISCH t (spec t_assumed))
       end
   end
\end{verbatim}
\end{hol}

La funzione ausiliaria \ml{spec} che � usata nel secondo caso
si basa sul fatto che \ml{dest\_forall} sollever� un'eccezione
\ml{HOL\_ERR} se il termine a cui � applicata non � quantificato universalmente.
Quando l'argomento di \ml{spec} non � quantificato universalmente, questo significa
che la ricorsione � conclusa, e tutte le variabili universali della
formula originaria sono state specializzate. Quindi la formula risultante
pu� essere riscritta a falso (le riscritture incorporate in \ml{REWRITE\_RULE}
gestiscono tutti i casi necessari).

Anche la funzione \ml{DPLL\_UNIV} usa \ml{REWR\_CONV} in due posti.
La funzione \ml{REWR\_CONV} applica una singola riscrittura (al primo ordine) al
livello principale di un termine. Questi usi di \ml{REWR\_CONV} sono fatti con
chiamate alla funzione \ml{CONV\_RULE}. Questa esegue [lifts ndt] un conversione $c$ (una
funzione che prende un termine $t$ e che produce un teorema $\vdash t = t'$),
cos� che $\ml{CONV\_RULE}\;c$ porta il teorema $\vdash t$ a $\vdash t'$.


\subsection{Conversione in Forma Normale Congiuntiva}
\label{sec:conv-conj-norm}

Una formula in Forma Normale Congiuntiva � una congiunzione di disgiunzioni
di letterali (cio� o variabili, o variabili negate). E' possibile
convertire formule della forma che ci attendiamo in CNF semplicemente
riscrivendo con il seguenti teoremi
\begin{eqnarray*}
\neg (\phi \land \psi) &=& \neg\phi \lor \neg\psi\\
\neg (\phi \lor \psi) &=& \neg\phi \land \neg\psi\\
\phi \lor (\psi \land \xi) &=& (\phi \lor \psi) \land (\phi \lor \xi)\\
(\psi \land \xi)\lor\phi \ &=& (\phi \lor \psi) \land (\phi \lor
\xi)\\[1ex]
\phi \Rightarrow\psi &=& \neg\phi \lor \psi\\
(\phi = \psi) &=& (\phi \Rightarrow \psi) \land (\psi \Rightarrow
\phi)
\end{eqnarray*}
Sfortunatamente, usare questi teoremi come riscritture pu� risultare in un
incremento esponenziale nella dimensione di una formula. (Si consideri di usarli
per convertire un input in Forma Normale Disgiuntiva, una disgiunzione
di congiunzioni di letterali, in CNF{}.)

Un approccio migliore � di convertire in ci� che � conosciuta come una ``CNF
definizionale''. \HOL{} include funzioni per fare questo nella structure
\ml{defCNF}. Sfortunatamente, questo approccio aggiunge quantificatori, esistenziali,
extra alla formula. Per esempio
\begin{session}
\begin{verbatim}
- defCNF.DEF_CNF_CONV ``p \/ (q /\ r)``;
> val it =
    |- p \/ q /\ r =
       ?x. (x \/ ~q \/ ~r) /\ (r \/ ~x) /\ (q \/ ~x) /\ (p \/ x) : thm
\end{verbatim}
\end{session}
Sotto la \holtxt{x} legata esistenzialmente, il codice ha prodotto una
formula in CNF{}. Con esempio piccolo come questo, la formula � di fatto
pi� grande di quella prodotto dalla traduzione ingenua, ma con esempi
pi� realistici, la differenza diventa velocemente significativa. L'ultimo
esempio usato con \ml{tautDP} � 20 volte pi� grande quando tradotto
ingenuamente di quando usando \ml{defCNF}, e la traduzione richiede 150
volte pi� tempo per essere eseguita.

Ma cosa facciamo di queste variabili quantificate esistenzialmente extra? Di fatto,
possiamo ignorare la quantificazione quando chiamiamo la procedura core DPLL.
Se passiamo il corpo non quantificato a DPLL, otteniamo indietro o un
verdetto di insoddisfacibilit� della forma $\vdash \varphi' = \holtxt{F}$, o una
assegnazione per tutte le variabili libere che soddisfa. Se capita la
seconda, la stessa assegnazione soddisfer� anche
l'originale. Se capita la prima, eseguiremo la seguente dimostrazione
\[
\infer{\vdash (\exists \vec{x}.\;\varphi') = \holtxt{F}}{
  \infer{\vdash (\exists \vec{x}.\;\varphi') \Rightarrow \holtxt{F}}{
    \infer{\vdash\forall \vec{x}.\;\varphi' \Rightarrow \holtxt{F}}{
      \infer{\vdash\varphi' \Rightarrow \holtxt{F}}{
        \vdash \varphi' = \holtxt{F}
      }
    }
  }
}
\]
producendo un teorema della forma attesa dalla nostra funzione
\ml{wrapper}.

Di fatto, c'� una funzione alternativa nell'API \ml{defCNF} che
useremo preferendola a \ml{DEF\_CNF\_CONV}. Il problema con
\ml{DEF\_CNF\_CONV} � che pu� produrre una grande quantificazione,
che coinvolge molte variabili. Useremo piuttosto
\ml{DEF\_CNF\_VECTOR\_CONV}. Al posto di un output della forma
\[
\vdash \varphi = (\exists \vec{x}.\; \varphi')
\]
questa seconda funzione produce
\[
\vdash \varphi = (\exists (v : \textsf{num} \rightarrow
\textsf{bool}).\; \varphi')
\]
dove le variabili individuali $x_i$ della prima formula sono sostituite
da chiamate alla funzione $v$ $v(i)$, e c'� una sola variabile
quantificata, $v$. Questa variabile non influenzer� l'operazione della
dimostrazione abbozzata di sopra. E fino a quando non richiediamo che i letterali siano
variabili o le loro negazioni, ma permettiamo anche che siano termini della
forma $v(i)$ e $\neg v(i)$, allora anche l'azione della procedura
DPLL sulla formula $\varphi'$ non sar� influenzata.

Sfortunatamente per uniformit�, in casi semplici, le funzioni di conversione
a una CNF definizionale possono risultate in nessuna quantificazione
esistenziale del tutto. Questo rende la nostra implementazione di \ml{DPLL}
in qualche modo pi� complicata. Calcoliamo una variabile \ml{body} che
sar� passata in cima alla funzione \ml{CoreDPLL}, esattamente come una
funzione \ml{transform} che trasformer� un risultato di insoddisfacibilit�
in qualcosa della forma desiderata. Se il risultato della conversione a
CNF produce una quantificazione esistenziale, usiamo la dimostrazione abbozzata
di sopra. Altrimenti, la trasformazione pu� essere la funzione identit�,
\ml{I}:
\begin{hol}
\begin{verbatim}
   fun DPLL t = let
     val (transform, body) = let
       val (vector, body) = dest_exists t
       fun transform body_eq_F = let
         val body_imp_F = CONV_RULE (REWR_CONV (GSYM IMP_F_EQ_F)) body_eq_F
         val fa_body_imp_F = GEN vector body_imp_F
         val ex_body_imp_F = CONV_RULE FORALL_IMP_CONV fa_body_imp_F
       in
         CONV_RULE (REWR_CONV IMP_F_EQ_F) ex_body_imp_F
       end
     in
       (transform, body)
     end handle HOL_ERR _ => (I, t)
   in
     case CoreDPLL body of
       Unsat body_eq_F => Unsat (transform body_eq_F)
     | x => x
   end
\end{verbatim}
\end{hol}
dove dobbiamo ancora implementare la procedura DPLL core (chiamata
\ml{CoreDPLL} di sopra). Il codice di sopra usa \ml{REWR\_CONV} con il
teorema \ml{IMP\_F\_EQ\_F} per influenzare due delle trasformazioni
della dimostrazione. La funzione \ml{GSYM} � usata per invertire
le uguaglianza di primo livello di un teorema. Infine,
la conversione \ml{FORALL\_IMP\_CONV} prende un termine della forma
\[
\forall x.\;P(x) \Rightarrow Q
\]
e restituisce il teorema
\[
\vdash (\forall x.\;P(x) \Rightarrow Q) = ((\exists
x.\;P(x))\Rightarrow Q)
\]




\subsection{La Procedura DPLL Core}
\label{sec:dpll-procedure}

La procedura pu� essere vista come una piccola variazione sulla tecnica
di base ``tabelle di verit�'' che abbiamo gi� visto. Come con quella
procedura, l'operazione core � un case-split su una variabile booleana.
Ci sono tuttavia due differenze significative: DPLL pu� essere vista come
una ricerca per un'assegnazione soddisfacente, cos� che se selezionando una variabile
in modo da avere un particolare valore risulta in un'assegnazione soddisfacente, non abbiamo
bisogno di controllare anche cosa accade se alla stessa variabile � dato il
valore di verit� opposto. In secondo luogo, DPLL fa una certa attenzione a selezionare delle variabili
opportune su cui fare lo split. In particolare � usata la \emph{unit propagation}
per eliminare variabili che non causeranno ramificazioni nello
spazio di ricerca.

La nostra implementazione della procedura DPLL core � una funzione che prende
un termine e restituisce un valore del tipo \ml{result}: o un teorema
che uguaglia il termine originario a falso, o un'assegnazione soddisfacente (nella
forma di una funzione da termini a termini). Mentre la ricerca DPLL per
un'assegnazione soddisfacente procede, � costruita in modo incrementale
un'assegnazione. Questo suggerisce che il nucleo ricorsivo della nostra funzione
avr� bisogno di prendere un termine (la formula corrente) e un contesto (l'assegnazione
corrente) come parametri. L'assegnazione pu� essere rappresentata in modo
naturale come un insieme di equazioni, dove ciascuna equazione � o either $v =
\holtxt{T}$ o $v = \holtxt{F}$.

Questo suggerisce che una rappresentazione per la dichiarazione del nostro programma �
un teorema: le ipotesi rappresenteranno l'assegnazione, e la conclusione
pu� essere la formula corrente. Naturalmente, i teoremi \HOL{}
non possono semplicemente essere desiderati esistere. In questo caso, possiamo rendere
ogni cosa valida assumendo anche la formula iniziale. Cos�, quando
iniziamo la nostra dichiarazione iniziale sar� $\phi\vdash\phi$. Dopo aver effettuato lo splitting sulla
$v$, genereremo due nuove dichiarazioni
$\phi,(v\!=\!\holtxt{T})\vdash \phi_1$, e
$\phi,(v\!=\!\holtxt{F})\vdash \phi_2$, dove i $\phi_i$ sono il
risultato di semplificare $\phi$ sotto l'assunzione aggiuntiva
che vincola $v$.

Il modo pi� semplice per aggiungere un'assunzione a un teorema � usare la
regola \ml{ADD\_ASSUM}. Ma in questa situazione, vogliamo anche
semplificare la conclusione del teorema con la stessa assunzione. Questo
significa che sar� sufficiente riscrivere con il teorema
$\psi\vdash\psi$, dove $\psi$ � la nuova assunzione. L'azione di
riscrivere con un tale teorema far� apparire la nuova assunzione
tra le assunzioni del risultato.

La funzione \ml{casesplit} � cos�:
\begin{hol}
\begin{verbatim}
   fun casesplit v th = let
     val eqT = ASSUME (mk_eq(v, boolSyntax.T))
     val eqF = ASSUME (mk_eq(v, boolSyntax.F))
   in
     (REWRITE_RULE [eqT] th, REWRITE_RULE [eqF] th)
   end
\end{verbatim}
\end{hol}

Un case split pu� risultare in una formula che � stata riscritta fino al
vero o al falso. Questi sono i casi base della ricorsione. Se la
formula � stata riscritta a vero, allora abbiamo trovato un'assegnazione
soddisfacente, una che � ora archiviata per noi nelle ipotesi del
teorema stesso. La seguente funzione \ml{mk\_satmap}, estrae
quelle ipotesi in una map finita, e poi restituisce la funzione
di lookup per quella map finita.
\begin{hol}
\begin{verbatim}
   fun mk_satmap th = let
     val hyps = hypset th
     fun foldthis (t,acc) = let
       val (l,r) = dest_eq t
     in
       Binarymap.insert(acc,l,r)
     end handle HOL_ERR _ => acc
     val fmap = HOLset.foldl foldthis (Binarymap.mkDict Term.compare) hyps
   in
     Sat (fn v => Binarymap.find(fmap,v)
                  handle Binarymap.NotFound => boolSyntax.T)
   end
\end{verbatim}
\end{hol}
La funzione \ml{foldthis} di sopra aggiunge le equazioni che sono archiviate come
ipotesi nella map finita. La gestione delle eccezione in
\ml{foldthis} � necessario perch� una delle ipotesi sar� la
formula originaria. La gestione delle eccezioni nella funzione che cerca
i binding delle variabili � necessaria perch� una formula pu� essere ridotta a
vero senza che tutte le variabili siano state assegnate a un valore qualsiasi, cos�
mappiamo in modo arbitrario tali variabili a \holtxt{T}.

Se la formula � stata riscritta a falso, allora possiamo semplicemente restituire
questo teorema direttamente. Un tale teorema non � del tutto nella forma giusta
per il chiamante esterno, che si aspetta un'equazione, cos� se il
risultato finale � della forma $\phi\vdash \holtxt{F}$, dovremo
trasformare questo in $\vdash \phi = \holtxt{F}$.

La domanda successiva da affrontare � cosa fare con i risultati delle
chiamate ricorsive. Se un case split restituisce un'assegnazione soddisfacente questa
pu� essere restituita senza modifiche. Ma se una chiamata ricorsiva restituisce un teorema
che uguaglia l'input a falso, c'� bisogno di fare di pi�. Se questa � la
prima chiamata, allora � necessario controllare l'altro ramo. Se anche questo
restituisce che il teorema � insoddisfacibile, allora abbiamo due teoremi.
\[
\phi_0,\Delta,(v\!=\!\holtxt{T})\vdash \holtxt{F} \qquad
\phi_0,\Delta,(v\!=\!\holtxt{F})\vdash \holtxt{F}
\] dove $\phi_0$ � la formula originaria, $\Delta$ � il resto
dell'assegnazione corrente, e $v$ � la variabile su cui � stato appena eseguito
uno split. Per trasformare questi due teoremi nel desiderato
\[
\phi_0,\Delta\vdash \holtxt{F}
\]
useremo la regola d'inferenza \ml{DISJ\_CASES}:
\[
\infer{\Gamma \cup \Delta_1 \cup \Delta_2 \vdash \phi}{
  \Gamma \vdash \psi \lor \xi &
  \Delta_1 \cup \{\psi\}\vdash \phi &
  \Delta_2 \cup \{\xi\} \vdash \phi
}
\]
e il teorema \ml{BOOL\_CASES\_AX}:
\[
\vdash \forall t.\;(t = \holtxt{T}) \lor (t = \holtxt{F})
\]

Possiamo mettere insieme questi frammenti e scrivere la funzione \ml{CoreDPLL}
di alto livello, nella Figura~\ref{fig:coredpll}.
\begin{figure}[htbp]
\begin{holboxed}
\begin{verbatim}
fun CoreDPLL form = let
  val initial_th = ASSUME form
  fun recurse th = let
    val c = concl th
  in
    if c = boolSyntax.T then
      mk_satmap th
    else if c = boolSyntax.F then
      Unsat th
    else let
        val v = find_splitting_var c
        val (l,r) = casesplit v th
      in
        case recurse l of
          Unsat l_false => let
          in
            case recurse r of
              Unsat r_false =>
                Unsat (DISJ_CASES (SPEC v BOOL_CASES_AX) l_false r_false)
            | x => x
          end
        | x => x
      end
  end
in
  case (recurse initial_th) of
    Unsat th => Unsat (CONV_RULE (REWR_CONV IMP_F_EQ_F) (DISCH form th))
  | x => x
end
\end{verbatim}
\end{holboxed}
\caption{Il nucleo della funzione DPLL}
\label{fig:coredpll}
\end{figure}


Tutto ci� che rimane da fare � capire su quale variabile effettuare
il case split. Le variabili pi� importanti su cui effettuare lo split sono quelle
che appaiono in quelle che sono chiamate ``unit clauses'', clausole che contengono
solo un letterale. Se c'� una unit clause in una formula allora �
della forma
\[
\phi \land v \land \phi'
\]
o
\[
\phi \land \neg v \land \phi'
\]
In entrambe le situazioni, effettuare lo split su $v$ risulter� sempre in un ramo
che valuta direttamente a falso. Cos� eliminiamo una variabile
senza accrescere la dimensione del problema. Il processo di
eliminare clausole unitarie � di solito chiamato ``unit propagation''.
La unit propagation di solito non � pensata come un'operazione
di case splitting, ma eseguirla in questo modo render� il nostro codice pi� semplice.

Se una formula non include una clausola unitaria, allora la scelta della prossima
variabile su cui eseguire lo split � molto pi� di una magia nera. Qui
implementeremo una scelta molto semplice: per eseguire lo split sulla variabile che occorre
pi� di frequente. La nostra funzione \ml{find\_splitting\_var} prende una formula
e restituisce la variabile su cui eseguire lo split.
\begin{hol}
\begin{verbatim}
   fun find_splitting_var phi = let
     fun recurse acc [] = getBiggest acc
       | recurse acc (c::cs) = let
           val ds = strip_disj c
         in
           case ds of
             [lit] => (dest_neg lit handle HOL_ERR _ => lit)
           | _ => recurse (count_vars ds acc) cs
         end
   in
     recurse (Binarymap.mkDict Term.compare) (strip_conj phi)
   end
\end{verbatim}
\end{hol}
Questa funzione lavora passando una lista di clausole alla funzione
pi� interna \ml{recurse}. Questa spoglia ciascuna clausola una alla volta. Se una
clausola ha un solo disgiunto � una clausola unitaria e la variabile pu�
essere restituita direttamente. Altrimenti, le variabili nelle clausole sono
contate e aggiunte da \ml{count\_vars} alla map che si accumula, e la
ricorsione pu� continuare.

La funzione \ml{count\_vars} ha la seguente implementazione:
\begin{hol}
\begin{verbatim}
   fun count_vars ds acc =
     case ds of
       [] => acc
     | lit::lits => let
         val v = dest_neg lit handle HOL_ERR _ => lit
       in
         case Binarymap.peek (acc, v) of
           NONE => count_vars lits (Binarymap.insert(acc,v,1))
         | SOME n => count_vars lits (Binarymap.insert(acc,v,n + 1))
       end
\end{verbatim}
\end{hol}

L'uso di un albero binario per archiviare dati variabili rende efficiente
aggiornare i dati mentre sono raccolti. Estrarre la variabile
con il conteggio pi� grande � poi una scansione lineare dell'albero, che possiamo
fare con la funzione \ml{foldl}:
\begin{hol}
\begin{verbatim}
   fun getBiggest acc =
     #1 (Binarymap.foldl(fn (v,cnt,a as (bestv,bestcnt)) =>
                            if cnt > bestcnt then (v,cnt) else a)
                        (boolSyntax.T, 0)
                        acc
\end{verbatim}
\end{hol}

\subsection{Performance}
\label{sec:dpll-performance}

Quando vengono dati input un p� oltre quelli chiaramente banali, la funzione
che abbiamo scritto (al livello alto, \ml{DPLL\_UNIV}) ha delle performance considerevolmente
migliori rispetto all'implementazione con le tavole di verit�. Per esempio, la
generalizzazione del seguente termine, con 29 variabili, richiede a
\ml{wrapper} tre secondi e mezzo per essere dimostrata come tautologia:
\begin{hol}
\begin{verbatim}
   (s0_0 = (x_0 = ~y_0)) /\ (c0_1 = x_0 /\ y_0) /\
   (s0_1 = ((x_1 = ~y_1) = ~c0_1)) /\
   (c0_2 = x_1 /\ y_1 \/ (x_1 \/ y_1) /\ c0_1) /\
   (s0_2 = ((x_2 = ~y_2) = ~c0_2)) /\
   (c0_3 = x_2 /\ y_2 \/ (x_2 \/ y_2) /\ c0_2) /\
   (s1_0 = ~(x_0 = ~y_0)) /\ (c1_1 = x_0 /\ y_0 \/ x_0 \/ y_0) /\
   (s1_1 = ((x_1 = ~y_1) = ~c1_1)) /\
   (c1_2 = x_1 /\ y_1 \/ (x_1 \/ y_1) /\ c1_1) /\
   (s1_2 = ((x_2 = ~y_2) = ~c1_2)) /\
   (c1_3 = x_2 /\ y_2 \/ (x_2 \/ y_2) /\ c1_2) /\
   (c_3 = ~c_0 /\ c0_3 \/ c_0 /\ c1_3) /\
   (s_0 = ~c_0 /\ s0_0 \/ c_0 /\ s1_0) /\
   (s_1 = ~c_0 /\ s0_1 \/ c_0 /\ s1_1) /\
   (s_2 = ~c_0 /\ s0_2 \/ c_0 /\ s1_2) /\ ~c_0 /\
   (s2_0 = (x_0 = ~y_0)) /\ (c2_1 = x_0 /\ y_0) /\
   (s2_1 = ((x_1 = ~y_1) = ~c2_1)) /\
   (c2_2 = x_1 /\ y_1 \/ (x_1 \/ y_1) /\ c2_1) /\
   (s2_2 = ((x_2 = ~y_2) = ~c2_2)) /\
   (c2_3 = x_2 /\ y_2 \/ (x_2 \/ y_2) /\ c2_2) ==>
   (c_3 = c2_3) /\ (s_0 = s2_0) /\ (s_1 = s2_1) /\ (s_2 = s2_2)
\end{verbatim}
\end{hol}
(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.)

\section{Estendere l'Applicabilit� della nostra Procedura}
\label{sec:dpll-applicability-extension}

La funzione \ml{DPLL\_UNIV} richiede che il suo input sia quantificato
universalmente, con tutte le variabili libere legate, e che ciascun letterale sia
una variabile o la negazione di una variabile. Questo rende \ml{DPLL\_UNIV}
poco facile da usare quando viene ad essere usata come parte della dimostrazione di
un goal. In questa sezione, scriveremo un ulteriore livello
``wrapper'' per avvolgere \ml{DPLL\_UNIV}, producendo uno strumento che pu�
essere applicato a molti pi� goal.

\paragraph{Mitigare il Requisito di Quantificazione}  Il primo passo �
permettere formule che non sono chiuse. Al fine di trasmettere una formula
che \emph{�} chiusa a \ml{DPLL\_UNIV}, possiamo semplicemente generalizzare
sulle variabili libere della formula. Se \ml{DPLL\_UNIV} dice poi che
la nuova, formula ground � vera, allora lo sar� anche l'originale. Dall'altro
lato, se \ml{DPLL\_UNIV} dice che la formula ground �
falsa, allora non possiamo concludere niente di pi� e dovremo sollevare
un'eccezione.

Il codice che implementa questo � mostrato di sotto:
\begin{hol}
\begin{verbatim}
   fun nonuniv_wrap t = let
     val fvs = free_vars t
     val gen_t = list_mk_forall(fvs, t)
     val gen_t_eq = DPLL_UNIV gen_t
   in
     if rhs (concl gen_t_eq) = boolSyntax.T then let
         val gen_th = EQT_ELIM gen_t_eq
       in
         EQT_INTRO (SPECL fvs gen_th)
       end
     else
       raise mk_HOL_ERR "dpll" "nonuniv_wrap" "No conclusion"
   end
\end{verbatim}
\end{hol}

\paragraph{Permettere Foglie Non Letterali}
Possiamo fare meglio di \ml{nonuniv\_wrap}: piuttosto che quantificare solamente
solo sulle variabili libere (che abbiamo convenientemente assunto che saranno solo
booleane), possiamo trasformare ogni parte foglia del termine che non � una
variabile o la negazione di una variabile in una nuova variabile. Prima
estraiamo quelle foglie con valore booleano che non sono le costanti vero o
falso.
\begin{hol}
\begin{verbatim}
   fun var_leaves acc t = let
     val (l,r) = dest_conj t handle HOL_ERR _ =>
                 dest_disj t handle HOL_ERR _ =>
                 dest_imp t handle HOL_ERR _ =>
                 dest_bool_eq t
   in
     var_leaves (var_leaves acc l) r
   end handle HOL_ERR _ =>
     if type_of t <> bool then
       raise mk_HOL_ERR "dpll" "var_leaves" "Term not boolean"
     else if t = boolSyntax.T then acc
     else if t = boolSyntax.F then acc
     else HOLset.add(acc, t)
\end{verbatim}
\end{hol}
Si noti che non abbiamo tentato esplicitamente di separare le negazioni
booleane (il che si potrebbe fare con \ml{dest\_neg}). Questo perch�
anche \ml{dest\_imp} distrugge termini \holtxt{\~{}p}, restituendo
\holtxt{p} e \holtxt{F} come l'antecedente e la conclusione. Abbiamo
anche usato una funzione \ml{dest\_bool\_eq} progettata per dividere solo
quelle uguaglianze che sono su valori booleani. La sua definizione �
\begin{hol}
\begin{verbatim}
   fun dest_bool_eq t = let
     val (l,r) = dest_eq t
     val _ = type_of l = bool orelse
             raise mk_HOL_ERR "dpll" "dest_bool_eq" "Eq not on bools"
   in
     (l,r)
   end
\end{verbatim}
\end{hol}

Ora possiamo scrivere la nostra funzione finale \ml{DPLL\_TAUT}:
\begin{hol}
\begin{verbatim}
   fun DPLL_TAUT tm =
     let val (univs,tm') = strip_forall tm
         val insts = HOLset.listItems (var_leaves empty_tmset tm')
         val vars = map (fn t => genvar bool) insts
         val theta = map2 (curry (op |->)) insts vars
         val tm'' = list_mk_forall (vars,subst theta tm')
     in
         EQT_INTRO (GENL univs
                      (SPECL insts (EQT_ELIM (DPLL_UNIV tm''))))
     end
\end{verbatim}
\end{hol}
Si noti come questo codice prima tira fuori tutte le quantificazioni universali
esterne (con \ml{strip\_forall}), e poi ri-generalizza
(con \ml{list\_mk\_forall}). Le chiamate a \ml{GENL} e \ml{SPECL}
annullano queste manipolazioni, ma al livello dei teoremi. Questo produce
un teorema che uguaglia l'input originale a vero. (Se il termine di input non
� un'istanza di una formula proposizionale valida, la chiamata a
\ml{EQT\_ELIM} sollever� un'eccezione.)

\section*{Esercizi}

\begin{enumerate}
\item Estendere la procedura cos� che gestisca le espressioni condizionali
	(entrambi i rami dei termini devono essere di tipo booleano).
\end{enumerate}


%%% Local Variables:
%%% mode: latex
%%% TeX-master: "tutorial"
%%% End: