Définition - Que signifie l'unification?
En informatique et en logique, l'unification est la procédure algorithmique utilisée pour résoudre des équations impliquant des expressions symboliques. En d'autres termes, en remplaçant certaines variables de sous-expression par d'autres expressions, l'unification tente d'identifier deux expressions symboliques. L'unification est utilisée dans la technologie de raisonnement automatisé, qui reste l'un des principaux domaines d'application de l'unification.
L'unification est utilisée dans les implémentations telles que:
- Implémentation de système de type langage de programmation
- Programmation logique
- Solveurs SMT
- Analyse du protocole cryptographique
- Algorithmes de réécriture de termes
L'unification est l'une des techniques fondamentales sur lesquelles reposent les méthodes de déduction automatisée.
Definir Tech explique l'unification
Le terme «unification» et sa notion peuvent être attribués à John Alan Robinson. Il a utilisé l'unification comme opération de base de son principe de résolution et a également montré que les termes unifiables ont au plus un unificateur général. Plusieurs cadres d'unification sont différenciés en fonction des expressions qui se produisent dans le problème d'unification. L'unification du premier ordre est celle dans laquelle des variables d'ordre supérieur (variables représentant des fonctions) sont autorisées dans les expressions. L'unification libre ou l'unification syntaxique est celle dans laquelle une solution est nécessaire pour rendre les deux côtés de l'équation égaux.
La solution d'un problème d'unification est représentée par la substitution, qui est le mappage d'une valeur symbolique à chaque variable impliquée dans les expressions du problème. En d'autres termes, l'objectif essentiel de l'unification est de rechercher une substitution afin d'unifier deux termes donnés. On s'attend à ce qu'un algorithme uniforme supérieur fournisse un ensemble de substitution minimal et complet (un ensemble ayant toutes les solutions pertinentes sans membres redondants) pour un problème donné. En d'autres termes, l'unification ne s'intéresse pas seulement à la solvabilité d'une unification donnée en cas de problème, mais aussi si elle peut être résolue, au calcul de l'unificateur le plus général.
L'unification est considérée comme le cœur de:
- Implémentations Prolog
- Systèmes experts basés sur l'intelligence artificielle
- Correspondance de modèles dans les langages fonctionnels
- Certaines approches d'analyse
- Bases de données déductives
- Traitement du langage naturel
- Prouveurs de théorème
- Algorithmes d'inférence de type