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

Odpowiedzi:

11

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.
Dave Clarke
źródło
8

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

P.Q,P.  Q

i cel dowodowy

(zab)(dore),zab !dore

apply rule mpapply simpφφ(P.)=zabφ(Q)=dore

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

(zab)(dore),za !re

P.QP.P.P.Q


Γ={φ1,,φn}

Γψ

oznacza:

Γψ

Γψψ

P.Qφ

Raphael
źródło
3
2

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

jmad
źródło
Nie sądzę, żeby pierwsze zdanie było ważne; zobacz moją odpowiedź.
Raphael
1
Nie zgadzam się również z pierwszym zdaniem. Rozdzielczość (specjalizacja unifikacji) jest rdzeniem Prologu, który jest jednym z najpopularniejszych języków implementacji systemów ekspertowych i innych mechanizmów wnioskowania.
Dave Clarke
@Raphael i Dave: więc mówisz, że algorytm unifikacji jest bezpośrednio używany w silnikach wnioskowania?
jmad
@jmad: Nie jestem pewien, że istnieje algorytm unifikacji, a ja nie jestem też pewien, jakiego rodzaju systemy są nazywane „silnik wnioskowanie”. Wiem, że unifikacja jest szeroko stosowana wszędzie tam, gdzie pojawia się logika i / lub formalna semantyka; zobacz odpowiedź Dave'a na listę.
Raphael
@Raphael: to właściwie problem, który chciałem rozwiązać: wydaje się, że mechanizmy wnioskowania nie dotyczą wnioskowania, które znam na temat typu i logiki.
jmad