Paramodulacja

Z Wikipedii

Paramodulacja to algorytm automatycznego dowodzenia twierdzeń w systemach z równością.

Paramodulacja z grubsza polega na tym, że jeśli $f(\dots,X,\dots)=g(\dots)$ oraz $X = Y$ , to $f(\dots,Y,\dots)=g(\dots)$ .

Mówiąc zaś bardziej formalnie, jeśli $A = B$ , $C = D$ , i $C$ unifikuje się z podtermem $A$ na pozycji $p$ , to $\sigma A[p \larr D] = \sigma B$ , gdzie $σ$ to unifikator $A p$ i $C$ .

Na przykład:

$p (p (x, y), y) = q (y, x)$
$p (z, z) = z$

Unifikujemy $p (x, y)$ w $p (p (x, y), y)$ z $p (z, z)$ . Unifikator to $x = z, y = z$ . Zastępujemy więc $p (x, y)$ przez $z$ , wszystkie wystąpienia zmiennych $x$ i $y$ zastępujemy zgodnie z unifikatorem.

W wyniku otrzymujemy $p (z, z) = q (z, z)$

[edytuj] Porządek na termach

Naiwnie zaimplementowana paramodulacja może być bardzo nieefektywna - generowane równania mogą stawać się coraz większe i większe i wcale nie przybliżać nas do rozwiązania. Oczywistą heurystyką jest dobieranie do paramodulacji raczej mniejszych (które z większą szansą dokądś prowadzą) i starzych (które z większą szansą mają jakiś związek z problemem) równości.

Innym sposobem jest wprowadzenie porządku na termach, tak że używamy do paramodulacji tylko tej strony równania która jest mniejsza (lub nieporównywalna), przez co równania nie będą aż tak niekontrolowanie rosły.

[edytuj] AC-paramodulacja

Jeśli pewne symbole są łączne i przemienne, możemy dodać aksjomaty opisujące to do zbioru aksjomatów. Bardziej efektywne jest jednak często włączenie tego faktu do algorytmu paramodulacji. Zastępuje się po prostu zwykłą unifikację AC-unifikacją.

System oparty na AC-paramodulacji udowodnił że aksjomat Robbinsa w połączeniu z aksjomatami łączności i przemienności alternatywy stanowi pełną aksjomatyzację algebry Boola.