Inferenza nella logica dei predicati del
primo ordine
Ingegneria della conoscenza e sistemi esperti
Dario Bianchi , 1999
Inferenza nella logica del primo ordine
Sostituzioni e quantificatori
Sost( ,  ) applica la sostituzio ne  alla formula 
Sost({ x / Sam, y / Pam}, Piace( x, y )})  Piace ( Sam, Pam)
Eliminazio ne degli universali
da x Piace(x,Gelato) sostituend o {x/Ben} si ha Piace(Ben, Gelato)
Eliminazio ne degli esistenzia li
da x Uccide(x,Vittima) possiamo inferire Uccide (Assa sin o,Vittima)
(Assassino è una qualsisasi costante che non compare nella formula)
Introduzio ne degli esistenzia li
da Piace(Gerry,Gelato) possiamo inferire xPiace( x, Gelato)
Ingegneria della conoscenza e sistemi esperti
Dario Bianchi , 1999
Inferenza nella logica del primo ordine
Dalle formule :
Buffalo ( Bob )
Pig ( Pat )
x, y Buffalo ( x)  Pig ( y )  Faster ( x, y )
si inferisce la nuova formula : Buffalo ( Bob )  Pig ( Pat )
e col Modus Ponens : Faster(Bob , Pat)
MODUS PONENS
se c' è una sostituzio ne  tale che Sost (,pi )  Sost (,pi' ) i
p1' , p'2 ,..., p'n , ( p1  p2  ...  pn  q )
Sost (,q)
p1  p2  ...  pn  q è una formula di Horn (un solo letterale positivo
in una disgiunzio ne)
cioè : p1  p2   ...  pn  q
Ingegneria della conoscenza e sistemi esperti
Dario Bianchi , 1999
Inferenza nella logica del primo ordine
UNIFICAZIONE
La funzione UNIFICA prende due formule atomiche p e q e
restitusce una sostituzione che renda p e q uguali.
UNIFICA( p, q)   dove Sost ( , p )  Sost ( , q)
esempi :
UNIFICA(Conosce(John,x),Conosce(John, Jane))  {x/Jane}
UNIFICA(Conosce(John,x),Conosce(y,Leo nid))  {x/Leonid , y / John}
UNIFICA(Conosce(John,x),Conosce(y,Mad re( y ) ))  {y/John , x / Madre ( John) }
UNIFICA(Conosce(John,x),Conosce(x,Jane))  fail
Ingegneria della conoscenza e sistemi esperti
Dario Bianchi , 1999
Inferenza nella logica del primo ordine
Ingegneria della conoscenza e sistemi esperti
Dario Bianchi , 1999
Inferenza nella logica del primo ordine
Ingegneria della conoscenza e sistemi esperti
Dario Bianchi , 1999
Inferenza nella logica del primo ordine
Ingegneria della conoscenza e sistemi esperti
Dario Bianchi , 1999
Inferenza nella logica del primo ordine
Ingegneria della conoscenza e sistemi esperti
Dario Bianchi , 1999
Inferenza nella logica del primo ordine
Ingegneria della conoscenza e sistemi esperti
Dario Bianchi , 1999
Inferenza nella logica del primo ordine
Ingegneria della conoscenza e sistemi esperti
Dario Bianchi , 1999
Inferenza nella logica del primo ordine
Ingegneria della conoscenza e sistemi esperti
Dario Bianchi , 1999
Inferenza nella logica del primo ordine
Ingegneria della conoscenza e sistemi esperti
Dario Bianchi , 1999
Inferenza nella logica del primo ordine
Ingegneria della conoscenza e sistemi esperti
Dario Bianchi , 1999
Inferenza nella logica del primo ordine
Ingegneria della conoscenza e sistemi esperti
Dario Bianchi , 1999
Inferenza nella logica del primo ordine
Ingegneria della conoscenza e sistemi esperti
Dario Bianchi , 1999
Inferenza nella logica del primo ordine
Refutazion e (dimostraz ione per assurdo)
( KB  P  False )  ( KB  P)
Ingegneria della conoscenza e sistemi esperti
Dario Bianchi , 1999
Inferenza nella logica del primo ordine
Ingegneria della conoscenza e sistemi esperti
Dario Bianchi , 1999
Inferenza nella logica del primo ordine
Si consideri il problema “se Marcia va ovunque vada John, e John
è a scuola, dovè Marcia?”
Assiomi :
(y ) AT ( John, y )  AT ( Marcia , y )
AT ( John, school )
Domanda " Dov' è Marcia ?" (x) AT ( Marcia , x)
Negazione della domanda : (x) AT ( Marcia , x)
Che si può scrivere come : (x)AT ( Marcia , x)
In forma a clausole :
AT ( John, y )  AT ( Marcia , y )
AT ( John, school )
AT ( Marcia , x)
Ingegneria della conoscenza e sistemi esperti
Dario Bianchi , 1999
Inferenza nella logica del primo ordine
AT ( Marcia , x)
AT ( John, y )  AT ( Marcia , y )
{ y / x}
AT ( John, x)
AT ( John, school )
{x / school}
Sostituzione di risposta: {x / school}
Sostituendo nella domanda:
Ingegneria della conoscenza e sistemi esperti
AT ( Marcia , x)
Dario Bianchi , 1999