Dlaczego unifikacja jest tak ważna dla wnioskowania silników?

^{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?

Unifikacja jest tak fundamentalną koncepcją w informatyce, że być może czasem przyjmujemy to za pewnik. Za każdym razem, gdy mamy regułę, równanie lub wzorzec i chcemy zastosować ją do niektórych danych, ujednolicenie służy do specjalizacji reguły do ​​danych. Lub jeśli chcemy połączyć dwie ogólne, ale nakładające się reguły, unifikacja zapewnia nam najbardziej ogólną połączoną regułę. Ujednolicenie leży u podstaw

• Dowody twierdzeń i asystenci dowodowi, w tym niektóre oparte na unifikacji wyższego rzędu.
• Implementacje Prolog (jako Rozdzielczość).
• Algorytmy wnioskowania typu.
• Językoznawstwo komputerowe / przetwarzanie języka naturalnego.
• Systemy przepisywania terminów, takie jak Maude, które mogą być wykorzystane jako podstawa semantyki języka programowania.
• Dedukcyjne bazy danych.
• Systemy eksperckie lub bardziej ogólnie Sztuczna inteligencja.
• Komputerowe systemy algebry.
• Dopasowywanie wzorców w językach funkcjonalnych (przynajmniej częściowo ... tylko dopasowywanie).
• Niektóre podejścia do analizy.
• Niektóre języki zapytań, szczególnie w sieci semantycznej.

Proof asystenci, tacy jak Isabelle / HOL, pracują na poziomie syntaktycznym na rachunku logicznym. Wyobraź sobie, że masz zasadę modus ponens (MP)

$\qquad \displaystyle P\to Q, P\ \Longrightarrow\ Q$

i cel dowodowy

$\qquad \displaystyle (a \lor b) \to (c \land d), a \lor b \ \overset{!}{\Longrightarrow} c\land d$

apply rule mpapply simp$\varphi$$\varphi(P) = a\lor b$$\varphi(Q) = c \land d$

Zaletą metod asystentów, takich jak simpteraz, jest to, że jeśli Twoim celem jest

$\qquad \displaystyle (a \lor b) \to (c \land d), a \ \overset{!}{\Longrightarrow} d$

$P \land Q \Longrightarrow P$$P \Longrightarrow P \lor Q$

$\Gamma = \{\varphi_1, \dots, \varphi_n\}$

$\qquad \Gamma \Longrightarrow \psi$

oznacza:

$\Gamma$$\psi$

$\Gamma \Longrightarrow \psi$$\psi$

$P$$Q$$\varphi$

$\models$$\Longrightarrow$

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).