Paramodulacja

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

Paramodulacja z grubsza polega na tym, że:

jeśli ${\displaystyle f(\dots ,X,\dots )=g(\dots )}$ oraz ${\displaystyle X=Y,}$ to ${\displaystyle f(\dots ,Y,\dots )=g(\dots ).}$

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

Przykład

• ${\displaystyle p(p(x,y),y)=q(y,x),}$
• ${\displaystyle p(z,z)=z.}$

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

W wyniku otrzymujemy ${\displaystyle p(z,z)=q(z,z).}$

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.

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 Boole’a.