Paramodulacja

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

Paramodulacja z grubsza polega na tym, że:

jeśli oraz to

Mówiąc zaś bardziej formalnie, jeśli i unifikuje się z podtermem na pozycji to gdzie to unifikator i

Przykład

Unifikujemy w z Unifikator to Zastępujemy więc przez wszystkie wystąpienia zmiennych i zastępujemy zgodnie z unifikatorem.

W wyniku otrzymujemy

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.