Spisu treści:
Definicja - Co oznacza ujednolicenie?
W informatyce i logice unifikacja to procedura algorytmiczna stosowana w rozwiązywaniu równań zawierających wyrażenia symboliczne. Innymi słowy, zastępując niektóre zmienne podwyrażeniowe innymi wyrażeniami, unifikacja próbuje zidentyfikować dwa wyrażenia symboliczne. Unifikacja jest stosowana w zautomatyzowanej technologii wnioskowania, która pozostaje jednym z głównych obszarów zastosowań unifikacji.
Ujednolicenie jest stosowane w implementacjach takich jak:
- Implementacja systemu w języku programowania
- Programowanie logiki
- Solvery SMT
- Analiza protokołu kryptograficznego
- Algorytmy przepisywania terminów
Ujednolicenie jest jedną z podstawowych technik, na których oparte są metody zautomatyzowanej dedukcji.
Techopedia wyjaśnia Unifikację
Termin „zjednoczenie” i jego pojęcie można przypisać Johnowi Alanowi Robinsonowi. Użył unifikacji jako podstawowej operacji swojej zasady rozwiązywania, a także pokazał, że terminy jednoznaczne mają co najwyżej jeden ogólny unifikator. Kilka ram unifikacji jest zróżnicowanych w zależności od wyrażeń występujących w problemie unifikacji. Ujednolicenie pierwszego rzędu to takie, w którym zmienne wyższego rzędu (zmienne reprezentujące funkcje) są dozwolone w wyrażeniach. Bezpłatne zjednoczenie lub zjednoczenie syntaktyczne to takie, w którym potrzebne jest rozwiązanie, aby wyrównać obie strony równania.
Rozwiązanie problemu unifikacji jest przedstawione przez podstawienie, które jest odwzorowaniem wartości symbolicznej na każdą zmienną związaną z wyrażeniami problemu. Innymi słowy, Zasadniczym celem unifikacji jest poszukiwanie podstawienia w celu ujednolicenia dwóch podanych terminów. Oczekuje się, że wyższy jednolity algorytm zapewni minimalny i kompletny zestaw podstawiania (zestaw zawierający wszystkie odpowiednie rozwiązania bez zbędnych elementów) dla danego problemu. Innymi słowy, unifikacja jest zainteresowana nie tylko rozwiązywalnością danej unifikacji, jeśli jest to problemem, ale także jeśli jest to możliwe do rozwiązania, w obliczaniu najbardziej ogólnego unifikatora.
Ujednolicenie jest uważane za rdzeń:
- Wdrożenia Prolog
- Systemy eksperckie oparte na sztucznej inteligencji
- Dopasowywanie wzorców w językach funkcjonalnych
- Niektóre podejścia do analizy
- Dedukcyjne bazy danych
- Przetwarzanie języka naturalnego
- Dowody twierdzeń
- Algorytmy wnioskowania typu
