Applicazioni di unificazione?

Question

Quali sono le (pratiche) applicazioni di dell'Unità ? Dove viene effettivamente utilizzato nel mondo reale?

Non riuscivo a capire l'intera idea di ciò che realmente è e perché è considerato come una parte di Intelligenza Artificiale.

Answer 1

Unificazione è essenzialmente un processo di sostituzione . Ho visto che ha definito "a due vie matching".

In Prolog, in altri linguaggi di programmazione logica e nelle lingue direttamente sulla base di riscrittura logica ( Maude , Elan , ecc ...) è il meccanismo attraverso il quale liberi logici) variabili (sono legano ai termini / valori. In concomitante Prolog queste variabili vengono interpretate come canali di comunicazione.

IMO, il modo migliore per capire è con alcuni esempi di matematica (unificazione era / è un meccanismo chiave di base, per esempio, nel contesto di automatizzato di ricerca provers teorema, una branca della AI, un altro uso nella ). Gli esempi che seguono sono tratti dal contesto di (CAS) :

Primo esempio:

dato un insieme Q e due operazioni binarie * e + su di esso, allora * è sinistra-distributiva oltre + se:

X * (Y + Z)   =   (X * Y) + (X * Z)   |1|

Questo è un regola di riscrittura (un insieme di regole di riscrittura è un riscrittura sistema ).

Se vogliamo applicare questa regola di riscrittura ad un caso specifico, ad esempio:

a * (1 + b)   |2|

Unify (attraverso un algoritmo di unificazione) questo termine, | 2 |, con il lato sinistro ( LHS ) di | 1 | e noi abbiamo questo (banale di proposito) sostituzione ( unificatore più generale , mgu ):

{X/a, Y/1, Z/b}   |3|

Ora, applicando | 3 | al destra ( RHS ) di 1 |, abbiamo, infine:

(a * 1) + (a * b)

Questo è stato semplice e di apprezzare ciò che può fare l'unificazione vi mostrerò un po 'esempio più complesso.

Secondo esempio:

Dato questo regola di riscrittura:

log(X,Y) + log(X,Z)   =>   log(X,Y*Z)   |4|

l'applichiamo a questa equazione:

log(e,(x+1)) + log(e,(x-1)) = k   |5|

( LHS di | 5 | unificare a LHS di | 4 |), quindi abbiamo questa mgu :

{X/e, Y/(x+1), Z/(x-1)}   |6|

Si noti che X e X sono due variabili diverse. Qui abbiamo due variabili, X e Y, che corrispondono a due termini composti , (x + 1) e (x-1), non i valori semplici o variabili.

Applichiamo questa mgu , | 6 |, per RHS di | 4 | allora e ci siamo rimessi in questo | 5 |; così abbiamo:

log(e,(x+1)*(x-1)) = k   |7|

e così via.

(sperando non ho alcun errore o questo potrebbe confondere i neofiti ancora di più.)

Answer 2

Unificazione è un meccanismo fondamentale inferenza . In pratica, l'unificazione in questo contesto ridurrà di molto l'usura sulle dita.

Answer 3

Prolog , per esempio, utilizza l'unificazione di trovare i valori per le variabili che soddisfano le norme - vedi questa spiegazione per un esempio. Mi aspetto che sia una tecnica tipica nei linguaggi di programmazione logici in generale, anche se non ho esperienza con tutti gli altri.

Answer 4

L'unificazione è come pattern-matching, in cui si strofinare insieme due strutture, in cui le variabili in uno sono autorizzati a corrispondere i valori nell'altra.

La forma più semplice di unificazione accade ogni volta che si chiama una funzione in un linguaggio normale. Il chiamante ha argomenti, e il chiamato ha parametri. I parametri sono "legati a" gli argomenti, e che produce un'istanza della funzione.

Un altro semplice forma di unificazione è quando si utilizza un'espressione regolare per la corrispondenza, per esempio a un prompt dei comandi si potrebbe dire dir x*y*.z* che corrisponderà alcuni, ma non tutti i nomi dei file.

Intelligenza Artificiale piace fare uso di motori di inferenza, per cercare di simulare il ragionamento da un corpus di conoscenze, di solito sotto forma di dichiarazioni in una logica. Per scegliere uno stupido esempio, è possibile "sapere" che "tutti gli uomini sono mortali", come in forall(x)(man(x) implies mortal(x)). Poi, se fai una domanda "è Sam mortale", come mortal(Sam)?, si potrebbe unire che con la regola per ottenere una nuova domanda "è Sam un uomo" man(Sam)?

La speranza che aiuta.