Uniwersytet Warszawski University of Warsaw
Menu
Wyszukiwarka
 W bieżącym katalogu
next up previous
Next: Rachunki a unifikacja Up: Autoreferat pracy doktorskiej pt. Previous: Wyprowadzanie typów

Unifikacja

Drugim interesującym nas tutaj zagadnieniem jest unifikacja. W decyzyjnym problemie unifikacji danymi są zbiory par termów. Każdą taką parę nazywamy równaniem, a cały zbiór -- układem równań. W zadaniu chodzi zaś o podanie rozwiązania tego układu równań. Przez rozwiązanie rozumiemy tutaj informację, co należy wstawić na niewiadome, żeby równania stały się faktycznymi równościami.

W pewnym uproszczeniu gdy równania, które nas interesują, są między termami używanymi w logice pierwszego rzędu, a na niewiadome można wstawiać też tylko takie termy, to mówimy o unifikacji pierwszego rzędu. Gdy obiekty w równaniach są $\lambda$-termami (rachunku $\lambda$ z typami prostymi), a na niewiadome można wstawiać operatory, to mówimy o unifikacji wyższego rzędu. Jeśli operatory, które można wstawiać na niewiadome mogą operować tylko na obiektach typów atomowych (takich jak na przykład liczby naturalne, liczby rzeczywiste itp.), to mówimy o unifikacji drugiego rzędu. Owo ukonkretnienie odbywa się właśnie na zasadzie unifikacji.

Unifikacja ma główne zastosowanie w różnego rodzaju systemach automatycznego i półautomatycznego dowodzenia twierdzeń. Dotyczy to zwłaszcza systemów opartych na SLD-rezolucji, gdzie aby udowodnić klauzulę wynikową trzeba odpowiednio ukonkretnić klauzule wejściowe.


Aleksy Schubert 2001-03-15