Esempio reale di unificazione nella logica del primo ordine?

Question

So che questa è solo una parte di una domanda di programmazione, ma al momento sto facendo un po 'di programmazione logica. Una cosa che ancora non capisco correttamente è Unificazione nella logica del primo ordine.

Ho letto il Wikipedia article ed è più o meno chiaro che lo scopo è cercare un termine che unifica due frasi ... Ci sono anche esempi in questo articolo ma non capisco perché questo dovrebbe essere utile . Qualcuno può dare un esempio con oggetti del mondo reale invece di A, B, C, ecc.? Spero che questo mi aiuti a capire. Grazie

Answer 1

Se si osservano esempi reali in cui l'unificazione è utilizzata e utile, dare un'occhiata alle grammatiche basate sull'unificazione utilizzate nella linguistica computazionale, ad esempio HPSG e LFG. In apparenza, questo assomiglia ad un altro sapore di unificazione, ma sono davvero gli stessi.

La grammatica basata sull'unificazione può essere pensata come una CFG (grammatica context-free) in cui le produzioni vengono estese con l'unificazione. Ogni termine nel CGF ottiene un AVM (matrice del valore dell'attributo), che è un grafico aciclico diretto di caratteristiche e valori. L'idea qui è in qualche modo simile a attribuire grammatiche usate nei compilatori.

Immaginate questo giocattolo grammatica:

S -> NP VP 
NP -> Kim 
NP -> The cats 
VP -> V NP 
V -> see 
V -> sees 

Abbiamo qualche lieve overgeneration qui nel contratto:

* I gatti vede Kim [S [NP I gatti] [VP [V vede] [ NP Kim]]]

al fine di risolvere questo problema abbiamo potuto affinare la CFG per includere la nozione di accordo:

S -> NP_sg VP_sg 
S -> NP_sg VP_pl 
NP_sg -> Kim 
NP_pl -> The cats 
VP_sg -> V_sg NP_sg 
VP_sg -> V_sg NP_pl 
V_sg -> sees 
V_pl -> see 
VP_pl -> V_pl NP_pl 
VP_pl -> V_pl NP_sg 

Qui respingeremo l'overgeneration di prima. Ma questo porta all'esplosione combinatoria molto rapidamente. tuttavia abbiamo potuto aumentare ogni termine con un AVM e unificare questi insieme quando analizziamo:

S -> NP VP , C = A unified with B. 
NP -> kim /[ AGR sg ]. We mark Kim as being singular 
NP -> The cats/[ AGR pl ] 
VP[ AGR #1 ] -> V [ AGR #1 ] NP 

Il # 1-annotazione sono reentrancies, che significa che il valore di questa funzione deve essere la stessa, infatti indicheranno allo stesso nodo nel grafico dopo l'unificazione, se succede. Qui in pratica diciamo che la caratteristica dell'accordo di una frase verbale è la stessa dell'accordo del verbo nella frase.

V -> See/[ AGR pl ] 
V -> Sees/[ AGR sg ] 

Con la nostra grammatica giocattolo aumentata "Kim vedere i gatti" è respinto perché il NP e VP non unificare, avendo un valore diverso per la sua caratteristica AGR. Durante l'analisi, uniamo gli AVM insieme, e quindi acquisiamo molto in espressività, rendendo facile per gli ingegneri di grammatica scrivere grammatiche. In genere un UBG a copertura ampia ha nell'ordine di un centinaio di regole, mentre il CFG equivalente, che potrebbe non esistere, CFG con unificazione è completo di Turing, avrà regole nel numero di migliaia o più.

Per ulteriori dettagli, vedere HPSG e LFG.

Answer 2

La programmazione logica è, AFAIK, praticamente tutta l'unificazione. Fornisci una dichiarazione all'interprete e l'interprete prova a unificarlo con qualcosa che sa essere "vero", cioè qualcosa che si trova nel suo database.

ad es.

cat(tom) :- true. 

Asserisce che tom è un gatto.

Poi si può interrogare

?- cat(X). 

e prologo tornerà

X = tom 

Prolog guarda nel suo database e cerca di unificare la vostra dichiarazione fornita (cat(X)) con un dato di fatto già "conosce". In questo caso, trova cat(tom) e quindi può dirti che X=tom.

Answer 3

Grazie a voi per queste risposte dettagliate. Ora capisco davvero. Comunque vorrei scrivere qui un esempio che ho trovato nel libro "Artificial Intelligence: A Modern Approach" di Stuart Russell e Peter Norvig nel caso qualcuno stia cercando di nuovo la stessa domanda. Penso che questa risposta utilizza un approccio molto pratico:

regole di inferenza Lifted richiedono trovare sostituzioni che fanno diverse espressioni logiche sembrano identici. Questo processo è chiamato unificazione e è un componente chiave di tutti gli algoritmi di inferenza del primo ordine. L'algoritmo UNIFY accetta due frasi e restituisce un unificatore per loro se esiste uno .

Vediamo alcuni esempi di come UNIFY deve comportarsi. Supponiamo di avere una query Knows (John, x): chi conosce John ? Alcune risposte a questa domanda possono essere trovate trovando tutte le frasi in la knowledge base che unifica con Knows (John, x). Ecco i risultati di unificazione con quattro diverse frasi che potrebbero essere alla base conoscenze:

UNIFY(Knows(John, x), Knows(John, Jane)) = {x/Jane} 
UNIFY(Knows(John, x), Knows(y, Bill)) = {x/Bill, y/John} 
UNIFY(Knows(John, x), Knows(y, Mother(y))) = {y/John, x/Mother(John)} 
UNIFY(Knows(John, x), Knows(x, Elisabeth)) = fail 

L'ultima unificazione fallisce perché x non può assumere i valori John e Elizabeth ai contemporaneamente.