La logica del primo ordine (FOL) e i suoi metodi d’inferenza

• Costanti: nomi, numeri, città, oggetti, ecc.
• Predicati: per esempio \texttt{Brother}, \texttt{Mother}, \texttt{>}, ecc. che esprimono delle relazioni. Le utilizziamo in maniera simile alle funzioni. Ad esempio indicando
  \texttt{Brother}(x, \, y)
  stiamo indicando che x è fratello di y.
• Funzioni: per esempio \texttt{sqrt}, \texttt{LeftLegOf}, ecc. utilizzate per indicare concetti più complicati a cui non vogliamo associare un predicato. Tramite una funzione possiamo indicare dunque le gambe sinistre di tutte le persone come
  \texttt{LeftLegOf}(x)
  evitando di dover memorizzare un nome specifico per ogni istanza d’interesse.
• Variabili: per esempio x, y, ecc. possono essere anche delle costanti o dei predicati. Ci servono per indicare i dati del problema che stiamo trattando
• Connettivi: \wedge,\,\vee,\,\neg,\,\Rightarrow,\,\iff
• Uguaglianza: =
• Quantificatori: \forall,\,\exist (sono la cosa più importante introdotta dalla FOL)

\text{There is no one who doesn't like icecream}\\
\Downarrow\\
\forall\,\,x\,\,\texttt{Likes($x$, iceCream)}\,\,\equiv\,\,\textcolor{00ffa1}{\neg}\exists\,\,x\,\,\textcolor{00ffa1}{\neg}\texttt{Likes($x$, iceCream)}\\[30pt]

\text{Not everybody dislikes broccoli}\\
\Downarrow\\
\exists\,\,x\,\,\texttt{Likes($x$, broccoli)}\,\,\equiv\,\,\textcolor{00ffa1}{\neg}\forall\,\,x\,\,\textcolor{00ffa1}{\neg}\texttt{Likes($x$, broccoli)}

\text{Everyone at Oxford is smart}\\
\Downarrow\\
\forall\,\,x\,\,\texttt{At($x$, Oxford)}\Rightarrow \texttt{Smart($x$)}

\text{Someone who is not at Oxford is smart}\\
\Downarrow\\
\exists\,\,x\,\,\neg\texttt{At($x$, Oxford)}\,\,\wedge\,\,\texttt{Smart($x$)}

\forall\,\,x,\,y\,\,\texttt{Sibling}(x,\,y)\iff\neg(x=y)\wedge\exists \,\,m,\,f\,\,\neg(m=f)\wedge\texttt{Parent($m$, $x$)}\wedge\texttt{Parent($f$, $x$)}\wedge\texttt{Parent($m$, $y$)}\wedge\texttt{Parent($f$, $y$)}

• \forall\,\,x,\,y\,\,\texttt{Mother}(x,\,y)\iff\texttt{Parent}(x,\,y)\wedge\texttt{Female}(x)
  A parole: se x è madre di y, allora x è genitore di y ed è donna.
• \forall\,\,x,\,y\,\,\texttt{FirstCousin}(x,\,y)\iff\exist\,\,p,\,s\,\,\texttt{Parent}(p,\,x)\wedge\texttt{parent}(s,\,y)\wedge\texttt{Sibling}(s,\,p)
  A parole: perché x e y siano cugini di primo grado devono esistere due persone p ed s tali per cui p sia il genitore di x e s sia il genitore di y. Poiché x e y devono essere dei cugini di primo grado serve inoltre che p ed s siano fratelli (siblings) tra loro.

\begin{aligned}
&S=\texttt{Smarter($x$, $y$)}\rightarrow\text{frase originale}\\[10pt]

&\sigma=\{x/\texttt{Hilary},\,y/\texttt{Bill}\}\rightarrow\text{sostituzione}\\[10pt]

&S_{\sigma}=\texttt{Smarter(Hilary, Bill)}
\end{aligned}

• Universal instantiation: esprimiamo una frase universale inserendo all’interno dell’espressione un qualunque valore. Indichiamo tale valore qualsiasi con una variabile. Per esempio, nell’espressione
  \forall\,\,x\,\,\texttt{King}(x)\wedge\texttt{Greedy}(x)\Rightarrow\texttt{Evil}(x)
  possiamo sostituire al posto di x un qualunque valore per esprimere ciò che vogliamo. Inoltre, ponendo ad esempio x=\texttt{Father}(\texttt{John}) siamo anche in grado di comporre delle espressioni ben più complesse del tipo
  \dfrac{\forall\,\,x\,\,\boldsymbol{\alpha}}{\texttt{Substitute}(\{x/g\},\,\boldsymbol{\alpha})}
  A parole: per ogni possibile valore di x, data una frase \boldsymbol{\alpha}, possiamo sostituire g ad x per ottenere una frase \boldsymbol{\alpha} valida a sua volta. Il valore g viene chiamato ground-truth.
• Existential instantiation: per una frase \alpha nella variabile x possiamo sostituire il valore della variabile con una costante k (costante di Skolem), che non appare in altri luoghi della knowledge base. Tramite tale costante possiamo poi rappresentare ciò che vogliamo. Per esempio, partendo dall’espressione
  \exist\,\,x\,\,\texttt{Crown}(x)\wedge\texttt{OnHead}(x,\,\texttt{John})
  può essere ottenuta la frase
  \texttt{Crown}(c_1)\wedge\texttt{OnHead}(c_1,\,\texttt{John})
  dove abbiamo fissato un valore per x.
  Usando l’existential instantiation avremo delle espressioni del tipo
  \dfrac{\exist\,\,x\,\,\boldsymbol{\alpha}}{\texttt{Substitute}(\{x/k\},\,\boldsymbol{\alpha})}
  A parole: esiste almeno un valore di x per il quale, data una frase \boldsymbol{\alpha}, possiamo sostituire la costante k ad x per ottenere una frase \boldsymbol{\alpha} valida a sua volta.

\texttt{Knows}(\texttt{John},\,x)\qquad\texttt{Knows}(y,\,\texttt{Mary})

\{x/\texttt{Mary},\,y/\texttt{John}\}

\dfrac{p_1',\,p_2',\,\dots,\,p_n',\quad (p_i\wedge p_2\wedge\dots\wedge p_n\Rightarrow q)}{\text{Subst($\theta,\,q$)}}

\begin{matrix}
p_1'=\texttt{King}(\texttt{John}) & p_1=\texttt{King}(x)\\

p_2'=\texttt{Greedy}(y) & p_2=\texttt{Greedy}(x)
\end{matrix}

q=\texttt{Evil}(x)

\theta=\{x/\texttt{John},\,y/\texttt{John}\}

\text{Subst}(\theta,\,q)=\texttt{Evil}(\texttt{John})

\text{KB}\wedge\neg\alpha

[inserire formula]