Inhoudsopgave:
Definitie - Wat betekent Unification?
In de informatica en logica is unificatie de algoritmische procedure die wordt gebruikt bij het oplossen van vergelijkingen met symbolische uitdrukkingen. Met andere woorden, door bepaalde variabelen van sub-expressies te vervangen door andere expressies, probeert unificatie twee symbolische expressies te identificeren. Unificatie wordt gebruikt in geautomatiseerde redeneertechnologie, die een van de belangrijkste toepassingsgebieden van unificatie blijft.
Unificatie wordt gebruikt in implementaties zoals:
- Implementatie van het programmeertaal-type systeem
- Logisch programmeren
- SMT-oplossers
- Cryptografische protocolanalyse
- Algoritmen voor termherschrijven
Eenmaking is een van de fundamentele technieken waarop methoden voor geautomatiseerde aftrek zijn gebaseerd.
Techopedia verklaart Unification
De term "eenwording" en zijn begrip kunnen worden toegeschreven aan John Alan Robinson. Hij gebruikte unificatie als de basiswerking van zijn resolutieprincipe en toonde ook aan dat niet-identificeerbare termen maximaal één algemene unifier hebben. Verschillende kaders voor eenwording worden gedifferentieerd op basis van de uitdrukkingen die in het eenwordingprobleem voorkomen. Eerste orde unificatie is er een waarin hogere orde variabelen (variabelen die functies vertegenwoordigen) zijn toegestaan in de uitdrukkingen. Gratis unificatie of syntactische unificatie is er een waarbij een oplossing nodig is om beide zijden van de vergelijking gelijk te maken.
De oplossing van een unificatieprobleem wordt weergegeven door substitutie, wat het in kaart brengen is van een symbolische waarde voor elke variabele die betrokken is bij de uitdrukkingen van het probleem. Met andere woorden, de essentiële focus van eenwording is het zoeken naar een vervanging om twee gegeven termen te verenigen. Een hoger uniform algoritme zal naar verwachting een minimale en volledige substitutieset bieden (een set met alle relevante oplossingen zonder overbodige leden) voor een bepaald probleem. Met andere woorden, unificatie is niet alleen geïnteresseerd in oplosbaarheid van een gegeven unificatie als probleem, maar ook indien oplosbaar, in het berekenen van de meest algemene unifier.
Eenwording wordt beschouwd als de kern van:
- Prolog implementaties
- Expertsystemen op basis van kunstmatige intelligentie
- Patroonovereenkomst in functionele talen
- Bepaalde parsing-benaderingen
- Deductieve databases
- Natuurlijke taalverwerking
- Stelling bewijst
- Type inferentie-algoritmen
