Paramodulacja
Z Wikipedii
Paramodulacja to algorytm automatycznego dowodzenia twierdzeń w systemach z równością.
Paramodulacja z grubsza polega na tym, że jeśli 
oraz X = Y, to 
.
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](../../../math/6/e/9/6e923e1b0fb0aa1c7028d567f672874e.png)
, gdzie σ to unifikator Ap 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.
