\relax 
\ifx\hyper@anchor\@undefined
\global \let \oldcontentsline\contentsline
\gdef \contentsline#1#2#3#4{\oldcontentsline{#1}{#2}{#3}}
\global \let \oldnewlabel\newlabel
\gdef \newlabel#1#2{\newlabelxx{#1}#2}
\gdef \newlabelxx#1#2#3#4#5#6{\oldnewlabel{#1}{{#2}{#3}}}
\AtEndDocument{\let \contentsline\oldcontentsline
\let \newlabel\oldnewlabel}
\else
\global \let \hyper@last\relax 
\fi

\@writefile{toc}{\contentsline {section}{\numberline {1}Introduzione}{1}{section.1}}
\newlabel{Introduzione}{{1}{1}{Introduzione\relax }{section.1}{}}
\@writefile{toc}{\contentsline {section}{\numberline {2}Prefazione}{1}{section.2}}
\newlabel{Prefazione}{{2}{1}{Prefazione\relax }{section.2}{}}
\newlabel{lemdikonig}{{2.2}{1}{Prefazione\relax }{thm.2.2}{}}
\@writefile{toc}{\contentsline {section}{\numberline {3}Induzione}{1}{section.3}}
\newlabel{Induzione}{{3}{1}{Induzione\relax }{section.3}{}}
\newlabel{insieme indotto}{{3.3}{2}{Induzione\relax }{thm.3.3}{}}
\newlabel{albero binario}{{3.6}{3}{Induzione\relax }{thm.3.6}{}}
\newlabel{sequenza di costruzione}{{3.7}{4}{Induzione\relax }{thm.3.7}{}}
\newlabel{equivalenzacostruzioneinduzione}{{3.9}{4}{Induzione\relax }{thm.3.9}{}}
\newlabel{insieme libero}{{3.10}{5}{Induzione\relax }{thm.3.10}{}}
\newlabel{Induzione!strutturale}{{3.11}{5}{Induzione\relax }{thm.3.11}{}}
\newlabel{propseqminimali}{{3.13}{6}{Induzione\relax }{thm.3.13}{}}
\newlabel{pp1p21212}{{3.14}{6}{Induzione\relax }{thm.3.14}{}}
\newlabel{funzione induttiva}{{3.15}{6}{Induzione\relax }{thm.3.15}{}}
\newlabel{funzioneinduttivaunica}{{3.16}{7}{Induzione\relax }{thm.3.16}{}}
\@writefile{toc}{\contentsline {section}{\numberline {4}Logica proposizionale}{7}{section.4}}
\newlabel{Logica proposizionale}{{4}{7}{Logica proposizionale\relax }{section.4}{}}
\newlabel{deflogicaprop}{{4.1}{7}{Logica proposizionale\relax }{thm.4.1}{}}
\newlabel{formule atomiche}{{4.1}{7}{Logica proposizionale\relax }{thm.4.1}{}}
\newlabel{valutazione booleana}{{4.3}{8}{Logica proposizionale\relax }{thm.4.3}{}}
\newlabel{propdatafesisteunasolavalutaz}{{4.4}{9}{Logica proposizionale\relax }{thm.4.4}{}}
\newlabel{lem1}{{4.5}{9}{Logica proposizionale\relax }{thm.4.5}{}}
\newlabel{0esttaut}{{4.10}{10}{Logica proposizionale\relax }{thm.4.10}{}}
\newlabel{thmdideduzione}{{4.12}{11}{Logica proposizionale\relax }{thm.4.12}{}}
\newlabel{thmdideduzionegeneralizzata}{{4.13}{11}{Logica proposizionale\relax }{thm.4.13}{}}
\newlabel{dualsym}{{4.15}{12}{Logica proposizionale\relax }{thm.4.15}{}}
\newlabel{connettividuali}{{4.16}{12}{Logica proposizionale\relax }{thm.4.16}{}}
\newlabel{defoperatonegazione}{{4.17}{12}{Logica proposizionale\relax }{thm.4.17}{}}
\newlabel{operatore duale}{{4.17}{12}{Logica proposizionale\relax }{thm.4.17}{}}
\newlabel{propnegtaut}{{4.18}{13}{Logica proposizionale\relax }{thm.4.18}{}}
\newlabel{propnegdd}{{4.19}{13}{Logica proposizionale\relax }{thm.4.19}{}}
\newlabel{operatoresostituzione}{{4.21}{14}{Logica proposizionale\relax }{thm.4.21}{}}
\newlabel{psost}{{4.22}{14}{Logica proposizionale\relax }{thm.4.22}{}}
\newlabel{psostII}{{4.23}{14}{Logica proposizionale\relax }{thm.4.23}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.1}Forme normali}{15}{subsection.4.1}}
\newlabel{Forme normali}{{4.1}{15}{Forme normali\relax }{subsection.4.1}{}}
\newlabel{connettivi primari}{{4.25}{15}{Forme normali\relax }{thm.4.25}{}}
\newlabel{formulealphabetadef}{{4.25}{15}{Forme normali\relax }{thm.4.25}{}}
\newlabel{tabellaalphabetaform}{{4.27}{15}{Forme normali\relax }{thm.4.27}{}}
\newlabel{thmabinduzione}{{4.29}{16}{Forme normali\relax }{thm.4.29}{}}
\newlabel{defformab}{{4.30}{17}{Forme normali\relax }{thm.4.30}{}}
\newlabel{propformabeqformI}{{4.31}{17}{Forme normali\relax }{thm.4.31}{}}
\newlabel{formablibera}{{4.32}{17}{Forme normali\relax }{thm.4.32}{}}
\newlabel{exfindformab}{{4.33}{18}{Forme normali\relax }{thm.4.33}{}}
\newlabel{rango}{{4.33}{18}{Forme normali\relax }{thm.4.33}{}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {4.1.1}CNF e DNF}{18}{subsubsection.4.1.1}}
\newlabel{CNF e DNF}{{4.1.1}{18}{CNF e DNF\relax }{subsubsection.4.1.1}{}}
\newlabel{defdisgiunzioni}{{4.34}{18}{CNF e DNF\relax }{thm.4.34}{}}
\newlabel{letterali}{{4.34}{18}{CNF e DNF\relax }{thm.4.34}{}}
\newlabel{disgiunzioni letterali}{{4.34}{19}{CNF e DNF\relax }{thm.4.34}{}}
\newlabel{congiunzioni letterali}{{4.34}{19}{CNF e DNF\relax }{thm.4.34}{}}
\newlabel{Conjunctive Normal Form}{{4.34}{19}{CNF e DNF\relax }{thm.4.34}{}}
\newlabel{Disjunctive Normal Form}{{4.34}{19}{CNF e DNF\relax }{thm.4.34}{}}
\newlabel{remCNF}{{4.1}{19}{CNF e DNF\relax }{rem.4.1}{}}
\newlabel{valutazioneclausolavuota}{{4.35}{19}{CNF e DNF\relax }{thm.4.35}{}}
\newlabel{pquaconjblabla}{{4.36}{19}{CNF e DNF\relax }{thm.4.36}{}}
\newlabel{XtoCNF}{{4.37}{19}{CNF e DNF\relax }{thm.4.37}{}}
\newlabel{invariante}{{4.1.1}{21}{CNF e DNF\relax }{thm.4.37}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.2}Tableaux}{22}{subsection.4.2}}
\newlabel{Tableaux}{{4.2}{22}{Tableaux\relax }{subsection.4.2}{}}
\newlabel{tableaux}{{4.2}{22}{Tableaux\relax }{subsection.4.2}{}}
\newlabel{deftabl}{{4.38}{22}{Tableaux\relax }{thm.4.38}{}}
\newlabel{TsoddalloraTstarsodd}{{4.41}{23}{Tableaux\relax }{thm.4.41}{}}
\newlabel{thmdicorrettezza}{{4.42}{24}{Tableaux\relax }{thm.4.42}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.3}Risoluzioni}{25}{subsection.4.3}}
\newlabel{Risoluzioni}{{4.3}{25}{Risoluzioni\relax }{subsection.4.3}{}}
\newlabel{defrisol}{{4.44}{25}{Risoluzioni\relax }{thm.4.44}{}}
\newlabel{regole di espansione}{{4.44}{26}{Risoluzioni\relax }{thm.4.44}{}}
\newlabel{regole risolutive}{{4.44}{26}{Risoluzioni\relax }{thm.4.44}{}}
\newlabel{RissoddalloraRisstarsodd}{{4.47}{27}{Risoluzioni\relax }{thm.4.47}{}}
\newlabel{thmdicorrettezzarisol}{{4.48}{28}{Risoluzioni\relax }{thm.4.48}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.4}Completezza}{28}{subsection.4.4}}
\newlabel{Completezza}{{4.4}{28}{Completezza\relax }{subsection.4.4}{}}
\newlabel{Hintikka}{{4.49}{28}{Completezza\relax }{thm.4.49}{}}
\newlabel{hintikkasoddisfacibile}{{4.50}{28}{Completezza\relax }{thm.4.50}{}}
\newlabel{proprieta' di consistenza}{{4.51}{29}{Completezza\relax }{thm.4.51}{}}
\newlabel{defpropcons}{{4.51}{29}{Completezza\relax }{thm.4.51}{}}
\newlabel{thmdicompletezzaristrettatableaux}{{4.52}{30}{Completezza\relax }{thm.4.52}{}}
\newlabel{propSinCallorasoddisf}{{4.53}{30}{Completezza\relax }{thm.4.53}{}}
\newlabel{lemthmdicompletezzarisoluzioni}{{4.57}{33}{Completezza\relax }{thm.4.57}{}}
\newlabel{thmdiesistenzamodello}{{4.59}{37}{Completezza\relax }{thm.4.59}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.5}Compattezza}{41}{subsection.4.5}}
\newlabel{Compattezza}{{4.5}{41}{Compattezza\relax }{subsection.4.5}{}}
\newlabel{compattezza}{{4.61}{41}{Compattezza\relax }{thm.4.61}{}}
\newlabel{thmdicompattezza}{{4.61}{41}{Compattezza\relax }{thm.4.61}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.6}Risoluzioni ristrette}{42}{subsection.4.6}}
\newlabel{Risoluzioni ristrette}{{4.6}{42}{Risoluzioni ristrette\relax }{subsection.4.6}{}}
\newlabel{defCsat}{{4.63}{42}{Risoluzioni ristrette\relax }{thm.4.63}{}}
\newlabel{Csaturoinsodd}{{4.64}{43}{Risoluzioni ristrette\relax }{thm.4.64}{}}
\newlabel{Robinson}{{4.65}{46}{Risoluzioni ristrette\relax }{thm.4.65}{}}
\newlabel{Rsoddisf}{{4.66}{46}{Risoluzioni ristrette\relax }{thm.4.66}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.7}Conseguenza proposizionale}{47}{subsection.4.7}}
\newlabel{Conseguenza proposizionale}{{4.7}{47}{Conseguenza proposizionale\relax }{subsection.4.7}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.8}Sistemi di Hilbert}{48}{subsection.4.8}}
\newlabel{Sistemi di Hilbert}{{4.8}{48}{Sistemi di Hilbert\relax }{subsection.4.8}{}}
\newlabel{defhilbert}{{4.70}{48}{Sistemi di Hilbert\relax }{thm.4.70}{}}
\newlabel{Modus Ponens}{{4.70}{48}{Sistemi di Hilbert\relax }{thm.4.70}{}}
\newlabel{PalloraP}{{4.71}{49}{Sistemi di Hilbert\relax }{thm.4.71}{}}
\newlabel{zeroalloratutto}{{4.72}{49}{Sistemi di Hilbert\relax }{thm.4.72}{}}
\newlabel{thmdeduzioneTarski}{{4.73}{49}{Sistemi di Hilbert\relax }{thm.4.73}{}}
\newlabel{thmdiTarski}{{4.73}{49}{Sistemi di Hilbert\relax }{thm.4.73}{}}
\newlabel{NOTXXX}{{4.74}{51}{Sistemi di Hilbert\relax }{thm.4.74}{}}
\newlabel{thmhilbert}{{4.75}{52}{Sistemi di Hilbert\relax }{thm.4.75}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.9}Sistema di deduzione naturale}{55}{subsection.4.9}}
\newlabel{Sistema di deduzione naturale}{{4.9}{55}{Sistema di deduzione naturale\relax }{subsection.4.9}{}}
\newlabel{defdednaturale}{{4.76}{55}{Sistema di deduzione naturale\relax }{thm.4.76}{}}
\newlabel{propdednatalcunecose}{{4.77}{57}{Sistema di deduzione naturale\relax }{thm.4.77}{}}
\newlabel{thmdeduzionenaturale}{{4.78}{58}{Sistema di deduzione naturale\relax }{thm.4.78}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.10}Procedura di Davis Putnam}{61}{subsection.4.10}}
\newlabel{Procedura di Davis Putnam}{{4.10}{61}{Procedura di Davis Putnam\relax }{subsection.4.10}{}}
\newlabel{defSLit}{{4.79}{61}{Procedura di Davis Putnam\relax }{thm.4.79}{}}
\newlabel{lemmaSandLeqSLandL}{{4.80}{61}{Procedura di Davis Putnam\relax }{thm.4.80}{}}
\newlabel{lemmaSSLSoveL}{{4.81}{62}{Procedura di Davis Putnam\relax }{thm.4.81}{}}
\newlabel{lemaSsoddsoloconLalloraSLsoddisf}{{4.82}{62}{Procedura di Davis Putnam\relax }{thm.4.82}{}}
\newlabel{lemletteraleunicoinSalloraSLsoddisf}{{4.83}{63}{Procedura di Davis Putnam\relax }{thm.4.83}{}}
\newlabel{lemmaSLC1inC2}{{4.84}{63}{Procedura di Davis Putnam\relax }{thm.4.84}{}}
\newlabel{sadasdadasddsfq}{{4.86}{65}{Procedura di Davis Putnam\relax }{thm.4.86}{}}
\@writefile{toc}{\contentsline {section}{\numberline {5}Logica del I ordine}{66}{section.5}}
\newlabel{Logica del I ordine}{{5}{66}{Logica del I ordine\relax }{section.5}{}}
\newlabel{costanti}{{1}{66}{Logica del I ordine\relax }{Item.34}{}}
\newlabel{termini}{{5.1}{66}{Logica del I ordine\relax }{Item.36}{}}
\newlabel{termini chiusi}{{5.1}{66}{Logica del I ordine\relax }{Item.36}{}}
\newlabel{alberosintattico}{{5.2}{66}{Logica del I ordine\relax }{thm.5.2}{}}
\newlabel{albero sintattico}{{5.2}{66}{Logica del I ordine\relax }{thm.5.2}{}}
\newlabel{variabile legata}{{5.3}{67}{Logica del I ordine\relax }{thm.5.3}{}}
\newlabel{libera}{{5.3}{67}{Logica del I ordine\relax }{thm.5.3}{}}
\newlabel{enunciati}{{5.3}{67}{Logica del I ordine\relax }{thm.5.3}{}}
\newlabel{formula chiusa}{{5.3}{67}{Logica del I ordine\relax }{thm.5.3}{}}
\newlabel{sostituzione}{{5.5}{68}{Logica del I ordine\relax }{thm.5.5}{}}
\newlabel{sostituzprop1}{{5.6}{69}{Logica del I ordine\relax }{thm.5.6}{}}
\newlabel{sostituzprop2}{{5.7}{69}{Logica del I ordine\relax }{thm.5.7}{}}
\newlabel{sostituzione libera}{{5.8}{70}{Logica del I ordine\relax }{thm.5.8}{}}
\newlabel{propsostituzioneliberaassociativa}{{5.9}{70}{Logica del I ordine\relax }{thm.5.9}{}}
\newlabel{ridenominazione}{{5.10}{71}{Logica del I ordine\relax }{thm.5.10}{}}
\newlabel{algounificazione}{{5.16}{73}{Logica del I ordine\relax }{thm.5.16}{}}
\newlabel{Unificazione concorrente}{{5.18}{74}{Logica del I ordine\relax }{thm.5.18}{}}
\newlabel{Unificazione multipla}{{5.19}{75}{Logica del I ordine\relax }{thm.5.19}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.1}Semantica}{75}{subsection.5.1}}
\newlabel{Semantica}{{5.1}{75}{Semantica\relax }{subsection.5.1}{}}
\newlabel{interpretazione}{{5.21}{75}{Semantica\relax }{thm.5.21}{}}
\newlabel{propequivalenzanelmodelloequivalenzaveritas}{{5.22}{76}{Semantica\relax }{thm.5.22}{}}
\newlabel{propveritadiperogni}{{5.23}{76}{Semantica\relax }{thm.5.23}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.2}Termini chiusi}{77}{subsection.5.2}}
\newlabel{Termini chiusi}{{5.2}{77}{Termini chiusi\relax }{subsection.5.2}{}}
\newlabel{propterminichiusipreservati}{{5.24}{77}{Termini chiusi\relax }{thm.5.24}{}}
\newlabel{lemmaterminichiusiindipendenzaA}{{5.25}{77}{Termini chiusi\relax }{thm.5.25}{}}
\newlabel{propterminichiusiindipendenzaA}{{5.26}{77}{Termini chiusi\relax }{thm.5.26}{}}
\newlabel{propveritaperfomulechiuse}{{5.27}{78}{Termini chiusi\relax }{thm.5.27}{}}
\newlabel{propinterpretazionetermineassegnamento}{{5.28}{78}{Termini chiusi\relax }{thm.5.28}{}}
\newlabel{modello di Herbrand}{{5.29}{78}{Termini chiusi\relax }{thm.5.29}{}}
\newlabel{propvarieHerbrand}{{5.30}{79}{Termini chiusi\relax }{thm.5.30}{}}
\newlabel{dim3costruttori}{{5.30}{79}{Termini chiusi\relax }{thm.5.30}{}}
\newlabel{propxvarianteinHerbrand}{{5.31}{80}{Termini chiusi\relax }{thm.5.31}{}}
\newlabel{herbrandsoddisfacibilitasostituzioni}{{5.32}{81}{Termini chiusi\relax }{thm.5.32}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.3}Notazione uniforme}{82}{subsection.5.3}}
\newlabel{Notazione uniforme}{{5.3}{82}{Notazione uniforme\relax }{subsection.5.3}{}}
\newlabel{istanza}{{5.33}{82}{Notazione uniforme\relax }{thm.5.33}{}}
\newlabel{remgammaistanzax}{{5.1}{82}{Notazione uniforme\relax }{rem.5.1}{}}
\newlabel{equivalenzagammadelta}{{5.34}{82}{Notazione uniforme\relax }{thm.5.34}{}}
\newlabel{SUgsoddisfacibilesseSuggtsoddisfacibile}{{5.35}{83}{Notazione uniforme\relax }{thm.5.35}{}}
\newlabel{thmabgdinduzioneIordine}{{5.36}{83}{Notazione uniforme\relax }{thm.5.36}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.4}Sistemi di deduzione}{84}{subsection.5.4}}
\newlabel{Sistemi di deduzione}{{5.4}{84}{Sistemi di deduzione\relax }{subsection.5.4}{}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {5.4.1}Tableaux I ordine}{89}{subsubsection.5.4.1}}
\newlabel{Tableaux I ordine}{{5.4.1}{89}{Tableaux I ordine\relax }{subsubsection.5.4.1}{}}
\newlabel{deftabIordine}{{5.39}{89}{Tableaux I ordine\relax }{thm.5.39}{}}
\newlabel{correttezzatableauxIordine}{{5.41}{90}{Tableaux I ordine\relax }{thm.5.41}{}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {5.4.2}Risoluzioni I ordine}{90}{subsubsection.5.4.2}}
\newlabel{Risoluzioni I ordine}{{5.4.2}{90}{Risoluzioni I ordine\relax }{subsubsection.5.4.2}{}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {5.4.3}Hilbert del I ordine}{91}{subsubsection.5.4.3}}
\newlabel{Hilbert del I ordine}{{5.4.3}{91}{Hilbert del I ordine\relax }{subsubsection.5.4.3}{}}
\newlabel{Generalizzazione Universale}{{5.45}{91}{Hilbert del I ordine\relax }{thm.5.45}{}}
\newlabel{propassioma10debole}{{5.46}{91}{Hilbert del I ordine\relax }{thm.5.46}{}}
\newlabel{propHilbertausiliaraperlacompletezzadelta}{{5.48}{92}{Hilbert del I ordine\relax }{thm.5.48}{}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {5.4.4}Deduzione naturale I ordine}{94}{subsubsection.5.4.4}}
\newlabel{Deduzione naturale I ordine}{{5.4.4}{94}{Deduzione naturale I ordine\relax }{subsubsection.5.4.4}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.5}Completezza semantica}{94}{subsection.5.5}}
\newlabel{Completezza semantica}{{5.5}{94}{Completezza semantica\relax }{subsection.5.5}{}}
\newlabel{Hintikka I ordine}{{5.52}{94}{Completezza semantica\relax }{thm.5.52}{}}
\newlabel{hintikkasoddisfacibileIordine}{{5.53}{95}{Completezza semantica\relax }{thm.5.53}{}}
\newlabel{proprieta' di consistenza I ordine}{{5.54}{96}{Completezza semantica\relax }{thm.5.54}{}}
\newlabel{defpropconsIordine}{{5.54}{96}{Completezza semantica\relax }{thm.5.54}{}}
\newlabel{thmdiesistenzamodelloIordine}{{5.55}{96}{Completezza semantica\relax }{thm.5.55}{}}
\newlabel{compattezza I ordine}{{5.57}{99}{Completezza semantica\relax }{thm.5.57}{}}
\newlabel{thmdicompattezzaIordine}{{5.57}{99}{Completezza semantica\relax }{thm.5.57}{}}
\newlabel{thm di Herbrand}{{5.58}{99}{Completezza semantica\relax }{thm.5.58}{}}
\newlabel{thmdiHerbrand}{{5.58}{99}{Completezza semantica\relax }{thm.5.58}{}}
\newlabel{validasseveraneimodellidiHerbrand}{{5.59}{100}{Completezza semantica\relax }{thm.5.59}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.6}Skolemizzazione}{100}{subsection.5.6}}
\newlabel{Skolemizzazione}{{5.6}{100}{Skolemizzazione\relax }{subsection.5.6}{}}
\newlabel{thmsostituzioneIordine}{{5.60}{100}{Skolemizzazione\relax }{thm.5.60}{}}
\newlabel{thmsostituzioneperimplicazioni}{{5.62}{101}{Skolemizzazione\relax }{thm.5.62}{}}
\newlabel{lemmaskolemizzazione}{{5.63}{102}{Skolemizzazione\relax }{thm.5.63}{}}
\newlabel{thmdiskolemizzazione}{{5.64}{103}{Skolemizzazione\relax }{thm.5.64}{}}
\newlabel{premessa}{{5.66}{104}{Skolemizzazione\relax }{thm.5.66}{}}
\@writefile{toc}{\contentsline {section}{\numberline {6}*}{107}{section.6}}
\newlabel{*}{{6}{107}{*\relax }{section.6}{}}