Taula de continguts:
Definició: què significa Unificació?
En informàtica i lògica, la unificació és el procediment algorítmic utilitzat per resoldre equacions que impliquen expressions simbòliques. És a dir, substituint certes variables de subexpressió per altres expressions, la unificació intenta identificar dues expressions simbòliques. La unificació s’utilitza en la tecnologia de raonament automatitzat, que continua sent un dels principals àmbits d’aplicació de la unificació.
La unificació s'utilitza en aplicacions com:
- Implementació de sistemes de llenguatge de programació
- Programació lògica
- Solucionaris SMT
- Anàlisi del protocol criptogràfic
- Algorismes de reescriptura de terminis
La unificació és una de les tècniques fonamentals sobre les quals es basen els mètodes de deducció automatitzada.
Techopedia explica Unificació
El terme unificació i la seva noció es poden atribuir a John Alan Robinson. Va utilitzar la unificació com a operació bàsica del seu principi de resolució i també va demostrar que termes unificables tenen com a màxim un unificador general. Es diferencien diversos marcs d’unificació en funció de les expressions que es produeixen en el problema d’unificació. La unificació de primer ordre és aquella en què es permeten variables d’ordre superior (variables que representen funcions) a les expressions. La unificació lliure o la unificació sintàctica és aquella en què es necessita una solució per a fer iguals els dos costats de l’equació.
La solució d’un problema d’unificació es representa mitjançant la substitució, que és el mapeig d’un valor simbòlic a totes les variables implicades en les expressions del problema. És a dir, L'objectiu essencial de la unificació és buscar una substitució per unificar dos termes donats. S’espera que un algoritme uniforme superior proporcioni un conjunt de substitució mínim i complet (un conjunt que té totes les solucions rellevants sense membres redundants) per a un problema determinat. Dit d'una altra manera, la unificació no només interessa la solvibilitat d'una unificació donada si és un problema, sinó també si es pot solucionar, a l'hora de computar unificador més general.
La unificació es considera el nucli de:
- Prologacions d’implementacions
- Sistemes experts basats en intel·ligència artificial
- Coincidència de patrons en llenguatges funcionals
- Alguns enfocaments per analitzar
- Bases de dades deductives
- Processament del llenguatge natural
- Teorema demostradors
- Algorismes d’inferència de tipus
