IT/Description/drules.tex

14 le dimostrazioni e i teoremi sono resi concreti in \HOL.
18 le otto famiglie d'inferenze primitive che compongono il
33 primitive, insieme con le costanti primitive, i quattro assiomi,
60 usando le funzioni \ML\ \ml{ASSUME}\index{ASSUME@\ml{ASSUME}} e
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
175 \index{contare le inferenze, nelle dimostrazioni HOL@contare le inferenze, nelle dimostrazioni \HOL{}}%
222 Sezione~\ref{avra_standard}, sono date le derivazioni astratte per
223 le regole pre-definite che riflettono i pattern d'inferenza pi� usuali
230 Tutte le regole derivate pre-definite in \HOL\ sono descritte
247 � \ml{REWRITE\_RULE}. Tutte le regole di riscrittura sono descritte in
253 (teoremi le cui conclusioni possono essere considerate avere la forma
256 l'istanza corrispondente di $t_2$. La regola esegue un matching ricorsivo e a tutte le profondit�,
261 in definitiva sulle regole primitive \ml{SUBST} (per eseguire le sostituzioni);
262 \ml{INST\_TYPE}\index{INST_TYPE@\ml{INST\_TYPE}}  (per istanziare i tipi); e le regole derivate per
263 la generalizzazione e la specializzazione (si vedano le Sezioni~\ref{avra_gen}
287 illustra che le sostituzioni sono eseguite a tutti i livelli della
291 le usuali relazioni `maggiore di' e `minore di', rispettivamente,
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
327 \noindent Si noti che le equazioni
331 dimostrazione passo passo, con tutte le istanziazioni,
343 Il sistema \HOL{} fornisce tutte le regole standard d'introduzione ed
345 derivate. Sono queste regole, piuttosto che le regole
347 le derivazioni di alcune delle regole standard, in sequenza.
348 Queste derivazioni usano solo gli assiomi e le definizioni nella teoria
349 \theoryimp{bool} (si veda la Sezione~\ref{boolfull}), le otto regole
350 d'inferenza primitive della logica \HOL, e le inferenze definite in precedenza nella
386 Inoltre per ragioni che sono pi� che altro storiche, non tutte le
401 A titolo informativo, nella Versione 2.0 di \HOL\ le seguenti regole che dovrebbero essere
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{}}