IT/Description/drules.tex

14 le dimostrazioni e i teoremi sono resi concreti in \HOL.
16 Il sistema deduttivo di \HOL\
20 queste famiglie d'inferenze sono rappresentate in \HOL\ attraverso
31 Infine, la logica \HOL\ primitiva � stata integrata di tre costanti
43 Come illustrazione di una dimostrazione in \HOL{}, la seguente catena di
45 \HOL{}), per i particolari termini \ml{``}$t_1$\ml{``}%''
47 entrambi del tipo \HOL\ \ml{``:bool``}:%''
59 Nella sessione di sotto, la dimostrazione � eseguita nel sistema \HOL,
80 \noindent Pi� in breve, si potrebbe valutare la seguente, e `contare'\index{contare le inferenze, nelle dimostrazioni HOL@contare le inferenze, nelle dimostrazioni \HOL{}} le
99 \index{inferenze, nella logica HOL@inferenze, nella logica \HOL{}!come applicazioni di funzioni ML@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
111 \HOL\ non permette alcuna scorciatoia circa la necessit� di eseguire
113 d'inferenza derivate\index{inferenze, nella logica HOL@inferenze, nella logica \HOL{}!nelle regole derivate}
119 \index{dimostrazioni, nella logica HOL@dimostrazioni, nella logica \HOL{}!come applicazioni di funzioni ML@come applicazioni di funzioni \ML}
120 \index{dimostrazioni, nella logica HOL@dimostrazioni, nella logica \HOL{}!cos� come generate da regole derivate}
121 \index{regole derivate, nella logica HOL@regole derivate, nella logica \HOL{}!importanza delle}
124 metodologia \HOL{}; la dimostrazione di teoremi altrimenti sarebbe impossibile.
127 mostrata nell'esempio, che possono essere condotte in \HOL: una per ogni
137 \index{regole derivate, nella logica HOL@regole derivate, nella logica \HOL{}!giustificazione delle}
141 ha richiesto lo `scaricamento' delle assunzioni. Essa � specificata per \HOL{} da
154 \noindent Questa regola generale � valida perch� da un teorema \HOL\ della
171 cio�, esegue dimostrazioni in \HOL.
175 \index{contare le inferenze, nelle dimostrazioni HOL@contare le inferenze, nelle dimostrazioni \HOL{}}%
209 vedere, essa fa affidamento sulla classe delle funzioni \ML\ che accedono alla sintassi \HOL:
220 Quando si entra nel sistema \HOL\ sono pre-definite un numero di regole
225 regole derivate pre-definite in \HOL\ generano dimostrazioni relativamente corte.
230 Tutte le regole derivate pre-definite in \HOL\ sono descritte
239 \HOL\ � incluso un gruppo di regole con delle definizioni complesse che eseguono una limitata
246 Esse appaiono in \HOL{} nella forma di Cambridge. La regola base di riscrittura
251 \index{teoremi equazionali, nella logica HOL@teoremi equazionali, nella logica \HOL{}!uso dei \ldots nella riscrittura}
252 \index{teoremi, nella logica HOL@teoremi, nella logica \HOL{}!equazionali}
259 istanziazione\index{istanziazione di tipo, nella logica HOL@istanziazione di tipo, nella logica \HOL{}!nella regola di riscrittura} definiti internamente. La validit�
267 e \HOL-oriented.
282 insieme \HOL\ standard di tautologie pre-dimostrate; e queste regole di riscrittura
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
341 \index{regole derivate, nella logica HOL@regole derivate, nella logica \HOL{}!pre-definite|(}
343 Il sistema \HOL{} fornisce tutte le regole standard d'introduzione ed
350 d'inferenza primitive della logica \HOL, e le inferenze definite in precedenza nella
355 \index{teoremi, nella logica HOL@teoremi, nella logica \HOL{}!come regole d'inferenza}%
361 l'unico esempio dato di questo, ma ce ne sono molti altri in \HOL.)
369 \index{famiglie d'inferenze, nella logica HOL@famiglie d'inferenze, nella logica \HOL{}}%
371 di teoremi. Nella logica \HOL{} non � possibile esprimere alcun teorema singolo
373 \index{teoremi, nella logica HOL@teoremi, nella logica \HOL{}!regole non esprimibili come}
374 \index{beta-conversione, nella logica HOL@beta-conversione, nella logica \HOL{}!non esprimibile come un teorema}%
381 nel sistema \HOL\ che implementa la regola derivata come una procedura in
382 \ML. L'attuale implementazione nel sistema \HOL\ differisce in qualche
388 di fatto derivate nella versione attuale del sistema \HOL. Pi� precisamente,
395 \HOL\ esistente ha un sistema deduttivo pi� comprensivo di quello
399 \index{regole derivate, nella logica HOL@regole derivate, nella logica \HOL{}!pre-definite|)}
401 A titolo informativo, nella Versione 2.0 di \HOL\ le seguenti regole che dovrebbero essere
404 \index{regole d'inferenza, della logica HOL@regole d'inferenza, della logica \HOL{}!alcune \ldots non derivate in modo appropriato|(}
405 \index{regole nella logica HOL, alcune \ldots non derivate in modo appropriato@regole nella logica \HOL{}, alcune \ldots non derivate in modo appropriato|(}
413 \index{regole derivate, nella logica HOL@regole derivate, nella logica \HOL{}!elenco di \ldots assiomatiche}
454 \index{regole d'inferenza, della logica HOL@regole d'inferenza, della logica \HOL{}!alcune \ldots non derivate in modo appropriato|(}
455 \index{regole nella logica HOL, alcune \ldots non derivate in modo appropriato@regole nella logica \HOL{}, alcune \ldots non derivate in modo appropriato|(}
457 \index{regole d'inferenza, della logica HOL@regole d'inferenza, della logica \HOL{}!derivate|(}
474 \index{regole derivate, nella logica HOL@regole derivate, nella logica \HOL{}!elenco e derivazioni di alcune|(}
502 \index{implicazione, nella logica HOL@implicazione, nella logica \HOL{}!regole d'inferenza per}
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}
578 \index{applicazione di funzione, nella logica HOL@applicazione di funzione, nella logica \HOL{}!regole d'inferenza per}
627 \index{eguaglianza, nella logica HOL@eguaglianza, nella logica \HOL{}!regola MP per@regola \ml{MP} per}
649 \index{eguaglianza, nella logica HOL@eguaglianza, nella logica \HOL{}!altre regole per|(}
650 \index{implicazione, nella logica HOL@implicazione, nella logica \HOL{}!regole d'inferenza per}
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{}}
801 \index{eguaglianza, nella logica HOL@v, nella logica \HOL{}!altre regole per|)}
806 \index{quantificatore universale, nella logica HOL@quantificatore universale, nella logica \HOL{}!regole d'inferenza per}
811 \index{regola di generalizzazione, nella logica HOL@regola di generalizzazione, nella logica \HOL{}}
863 sistema \HOL\ dal momento che � sussunta da altre funzioni.}.
905 \item Dove $x'$ non occorre libera\index{variabili libere, nella logica HOL@variabili libere, nella logica \HOL{}} in $t$ (usiamo $x'$ piuttosto che semplicemente $x$
922 \index{quantificatore universale, nella logica HOL@quantificatore universale, nella logica \HOL{}!regole d'inferenza per}
926 \index{regola di estensionalit�, nella logica HOL@regola di estensionalit�, nella logica \HOL{}}
936 \item Dove $x$ non � libera\index{variabili libere, nella logica HOL@variabili libere, nella logica \HOL{}} in $t_1$ or $t_2$.
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}
1015 \index{quantificatore esistenziale, nella logica HOL@quantificatore esistenziale, nella logica \HOL{}!regole d'inferenza per|(}
1027 \item Dove $t_1[t_2]$ denota un termine $t_1$ con qualche occorrenza libera\index{variabili libere, nella logica HOL@variabili libere, nella logica \HOL{}}
1071 \item Dove $t[v]$ denota un termine $t$ con qualche occorrenza libera\index{variabili libere, nella logica HOL@variabili libere, nella logica \HOL{}}
1100 \index{quantificatore esistenziale, nella logica HOL@quantificatore esistenziale, nella logica \HOL{}!regole d'inferenza per|)}
1173 \index{congiunzione, nella logica HOL@congiunzione, nella logica \HOL{}!regola d'inferenza per}
1247 \subsection{\texorpdfstring{$\vee$-introduzione a destra}{Disgiunzione-introduzione a destra}}\index{disgiunzione, nella logica HOL@disgiunzione, nella logica \HOL{}!regola d'inferenza per|(}
1346 \index{disgiunzione, nella logica HOL@disgiunzione, nella logica \HOL{}!regola d'inferenza per|)}
1352 \index{F (falsit�), la costante HOL@\holtxt{F} (falsit�), la costante \HOL{}!regole d'inferenza per}
1356 \index{regola di contraddizione, nella logica HOL@regola di contraddizione, nella logica \HOL{}}
1387 \index{regole derivate, nella logica HOL@regole derivate, nella logica \HOL{}!elenco e derivazioni di alcune|)}
1388 \index{regole d'inferenza, della logica HOL@regole d'inferenza, della logica \HOL{}!derivate|)}