Uczę się samodzielnie Automated Theorem Proving / Solver SMT / Proof Assistants i zamieszczam serię pytań na temat tego procesu, zaczynając tutaj .
Ciągle czytam o algorytmie unifikacji .
- Co to jest i dlaczego jest tak ważne dla silników wnioskowania ?
- Dlaczego jest tak ważny dla informatyki?
Nie sądzę, aby wnioskowanie o silnikach było ważne . Algorytm unifikacji jest jednak bardzo pomocny przy wnioskowaniu typu . Są to dwa bardzo różne rodzaje wnioskowania.
Wnioskowanie o typach jest ważne dla informatyki, ponieważ typy są ważne w teorii języków programowania, która jest znaczącą częścią informatyki. Typy są również zbliżone do logiki i są intensywnie wykorzystywane w automatycznym dowodzeniu twierdzeń. Istnieją implementacje algorytmów unifikacyjnych w wielu, jeśli nie we wszystkich, asystentach dowodzenia i rozwiązaniach SMT.
Silniki wnioskowania są powiązane ze sztuczną inteligencją, która jest również ważna, ale bardzo odmienna. (Widziałem powiązania między uczeniem się a logiką, ale wydaje się to ściągnięte).
źródło