IT/Description/drules.tex

4 La nozione di {\it dimostrazione\/} � stata definita in modo astratto nel manuale
5 \LOGIC:\linebreak una dimostrazione di un sequente $(\Gamma,t)$ da un insieme di sequenti
7 una catena di sequenti culminanti in $(\Gamma,t)$, tale che ogni
10 di {\it teorema\/} � stata definita in \LOGIC: un teorema di un
11 sistema deduttivo � un sequente che segue dall'insieme vuoto di
12 sequenti per deduzione; cio�, � l'ultimo elemento di una dimostrazione
13 dall'insieme vuoto di sequenti, nel sistema deduttivo. In questa sezione,
16 Il sistema deduttivo di \HOL\
25 restituisce un valore di tipo \ml{thm}. E' stato spiegato che il
28 la possibilit� di computare teoremi se non per mezzo di funzioni che rappresentano
31 Infine, la logica \HOL\ primitiva � stata integrata di tre costanti
34 e una collezione di definizioni, forniscono un punto iniziale per
35 costruire dimostrazioni, e di conseguenza computare teoremi. Tuttavia, dimostrare
43 Come illustrazione di una dimostrazione in \HOL{}, la seguente catena di
59 Nella sessione di sotto, la dimostrazione � eseguita nel sistema \HOL,
99 \index{inferenze, nella logica HOL@inferenze, nella logica \HOL{}!come applicazioni di funzioni ML@come applicazioni di funzioni \ML}%
100 \index{passi di dimostrazione, come applicazioni di funzioni ML@passi di dimostrazione, come applicazioni di funzioni \ML}%
101 \index{dimostrazione!la nozione di, nel sistema HOL@la nozione
102   di, nel sistema \HOL}%
104 di una funzione \ML\ nell'esecuzione della dimostrazione in \HOL; e ciascuna
109 inferenza primitiva nella catena di dimostrazione, nel senso
111 \HOL\ non permette alcuna scorciatoia circa la necessit� di eseguire
114 (come implementate in \ML) riguarda la necessit� di
116 una dimostrazione di qualsiasi lunghezza. Si pu� vedere da questo che la regola
119 \index{dimostrazioni, nella logica HOL@dimostrazioni, nella logica \HOL{}!come applicazioni di funzioni ML@come applicazioni di funzioni \ML}
124 metodologia \HOL{}; la dimostrazione di teoremi altrimenti sarebbe impossibile.
126 Ci sono, naturalmente, un numero infinito di dimostrazioni, della `forma'
128 coppia di termini tipizzati \ml{``:bool``}. %''
157 come nell'esempio specifico di sopra.
161 primitive. La definizione \ML\ di \ml{UNDISCH} � semplicemente
177 ) Assumiamo che la stampa dei teoremi sia stata aggiustata come di sopra e che
178 \ml{th} sia legato come mostrato di sotto:
203 \noindent Ogni applicazione di successo di {\small\verb%UNDISCH%}
205 di {\small\verb%ASSUME%}, seguita da un'applicazione di {\small\verb%MP%};
207 dimostrazione di due passi per qualsiasi teorema dato (della forma appropriata).
215 pu� eseguire dimostrazioni di lunghezza arbitraria. Essa pu� fare anche uso di
220 Quando si entra nel sistema \HOL\ sono pre-definite un numero di regole
221 d'inferenza derivate (di cui \ml{UNDISCH} � una delle prime). Nella
227 grande quantit� di sforzo. Inoltre, possono essere definite dall'utente regole per
239 \HOL\ � incluso un gruppo di regole con delle definizioni complesse che eseguono una limitata
240 quantit� di dimostrazione `automatica' di teoremi in forma di riscrittura. L'idea
243 l'\LCF\ di Edimburgo\index{LCF@\LCF!Edinburgh}, e furono successivamente implementate
245 Huet\index{Huet, G.} per l'\LCF\ di Cambridge\index{LCF@\LCF!Cambridge}.
246 Esse appaiono in \HOL{} nella forma di Cambridge. La regola base di riscrittura
247 � \ml{REWRITE\_RULE}. Tutte le regole di riscrittura sono descritte in
250 \ml{REWRITE\_RULE} usa una lista di teoremi equazionali
255 qualsiasi sottotermine di un teorema oggetto che `matcha' $t_1$ con
256 l'istanza corrispondente di $t_2$. La regola esegue un matching ricorsivo e a tutte le profondit�,
258 usando algoritmi di ricerca, matching e
259 istanziazione\index{istanziazione di tipo, nella logica HOL@istanziazione di tipo, nella logica \HOL{}!nella regola di riscrittura} definiti internamente. La validit�
260  di \ml{REWRITE\_RULE} si appoggia
265 di \ml{REWRITE\_RULE} in \ML\
266 si basa anche su un grande numero di funzioni \ML\ generali
271 nelle dimostrazioni, perch� prende il posto di un grande numero d'inferenze
274 di inferenze che genera\footnote{Il numero di inferenze eseguite
278 	durante la fase di ricerca che non necessariamente sostiene delle
279 	sostituzioni di successo.}; e secondo perch� il suo risultato � spesso
281 equazionale esistente pu� essere fornito come una `regola di riscrittura', incluso un
282 insieme \HOL\ standard di tautologie pre-dimostrate; e queste regole di riscrittura
283 possono interagire l'una con l'altra nel processo di riscrittura per trasformare il
286 L'applicazione di \ml{REWRITE\_RULE}, nella sessione di sotto,
288 struttura di un termine.
291 le usuali relazioni `maggiore di' e `minore di', rispettivamente,
294 Si usa la definizione pre-esistente di {\small\verb%"$>"%}:
296 Si usa di nuovo la funzionalit� di timinig\index{contare le inferenze, nelle dimostrazioni HOL@contare le inferenze, nelle dimostrazioni \HOL{}}, a titolo informativo, e la stampa
297 di teoremi � aggiustata come sopra.
328 di riscrittura possono essere estratte da
333 sarebbe un processo lungo. Le regole di riscrittura lo rendono facile,
347 le derivazioni di alcune delle regole standard, in sequenza.
357 in accordo con la definizione data all'inizio di questo
359 di un teorema assomiglia alla derivazione di una regola eccetto per il fatto che non
360 ha ipotesi. (La derivazione di \ml{TRUTH}, Sezione~\ref{avra_T}, �
361 l'unico esempio dato di questo, ma ce ne sono molti altri in \HOL.)
366 coppia di termini $t_1$ e $t_2$, ed � quindi equivalente a una
371 di teoremi. Nella logica \HOL{} non � possibile esprimere alcun teorema singolo
377 (\ml{UNDISCH} non � una regola di questo tipo, dal momento che pu�, di fatto, essere
380 Per ogni derivazione data di sotto, c'� la definizione di una funzione \ML\
388 di fatto derivate nella versione attuale del sistema \HOL. Pi� precisamente,
391 esplicita. Bench� lo stato attuale di queste regole non sia
392 soddisfacente, ed � pianificato, con priorit� alta, di derivarle
393 in modo appropriato in una versione futura, il loro stato attuale di fatto
395 \HOL\ esistente ha un sistema deduttivo pi� comprensivo di quello
401 A titolo informativo, nella Versione 2.0 di \HOL\ le seguenti regole che dovrebbero essere
407 non sono derivate, ma (per questioni di efficienza) sono implementate come
409 di conversioni. % (conversions are discussed in Chapter~\ref{avra_conv}).
413 \index{regole derivate, nella logica HOL@regole derivate, nella logica \HOL{}!elenco di \ldots assiomatiche}
458 Le derivazioni che seguono consistono di sequenze di passi numerati ciascuno dei
473 \subsection{Aggiunta di un'assunzione}
474 \index{regole derivate, nella logica HOL@regole derivate, nella logica \HOL{}!elenco e derivazioni di alcune|(}
529 \index{regola di simmetria dell'eguaglianza, nella logica HOL@regola di simmetria dell'eguaglianza, nella logica \HOL{}}
530 \index{eguaglianza, nella logica HOL@eguaglianza, nella logica \HOL{}!regola di simmetria per}
555 \index{regola di transitivit� dell'eguaglianza, nella logica HOL@regola di transitivit� dell'eguaglianza, nella logica \HOL{}}
556 \index{eguaglianza, nella logica HOL@eguaglianza, nella logica \HOL{}!regola di transitivit� per}
577 \subsection{Applicazione di un termine a un teorema}%
578 \index{applicazione di funzione, nella logica HOL@applicazione di funzione, nella logica \HOL{}!regole d'inferenza per}
600 \subsection{Applicazione di un teorema a un termine}
695 \item $\turn \T = ((\lquant{x}x)=(\lquant{x}x))$\hfill [Definizione di \T]
731 \index{regola di specializzazione, nella logica HOL@regola di specializzazione, nella logica \HOL{}}
743 \item $t[t'/x]$ denota il risultato della sostituzione di $t'$ per le occorrenze libere\index{variabili libere, nella logica HOL@variabili libere, nella logica \HOL{}}
744 di $x$ in $t$, con la restrizione che nessuna variabile libera in $t'$
752 [\rul{INST\_TYPE} applicata alla definizione di $\forall$]
811 \index{regola di generalizzazione, nella logica HOL@regola di generalizzazione, nella logica \HOL{}}
834 [\rul{INST\_TYPE} applicata alla definizione di $\forall$]
862 usata in una derivazione successiva, ma di fatto non � nel
906 per motivare l'uso di \rul{SIMPLE\_ALPHA} nella derivazione di sotto).
926 \index{regola di estensionalit�, nella logica HOL@regola di estensionalit�, nella logica \HOL{}}
959 \index{operatore di scelta, nella logica HOL@operatore di scelta, nella logica \HOL{}!regole d'inferenza per}
985 \index{operatore di scelta, nella logica HOL@operatore di scelta, nella logica \HOL{}!regole d'inferenza per}
1028 di $t_2$
1029 scelta, e $t_1[x]$ denota il risultato di sostituire queste
1030 occorrenze di $t_1$ con $x$, con la restrizione che $x$
1044 [\rul{INST\_TYPE} applicata alla definizione di $\exists$]
1073 selezionata, e $t[x]$ denota il risultato di sostituire queste
1074 occorrenze di $v$ con $x$, con la restrizione che $x$ non divenga
1082 [\rul{INST\_TYPE} applicata alla definizione di $\exists$]
1102 \subsection{Uso di una definizione}
1133 \subsection{Uso di una definizione}
1225 \hfill [Definizione di $\conj$]
1264 \hfill [Definizione di $\disj$]
1299 \hfill [Definizione di $\disj$]
1332 \hfill [Definizione di $\disj$]
1351 \subsection{Regola classica di contraddizione}
1356 \index{regola di contraddizione, nella logica HOL@regola di contraddizione, nella logica \HOL{}}
1368 \item $\turn \neg = \lquant{b}b\imp\F$\hfill [Definizione di $\neg$]
1378 \item $\turn \F = \uquant{b}b$\hfill [Definizione di $\F$]
1387 \index{regole derivate, nella logica HOL@regole derivate, nella logica \HOL{}!elenco e derivazioni di alcune|)}