Istotą rozważań jest wykorzystanie odpowiedniej formalizacji logiki - formalizacji odrzuceniowej wyrażeń i automatycznego dowodzenia twierdzeń w teoriach nadbudowanych nad n-wartościowymi rachunkami predykatów. Badania nad aksjomatycznym odrzucaniem zostały zapoczątkowane przez Łukasiewicza i kontynuowane wspólnie przez Słupeckiego, Brylla, Wybraniec-Skardowską, Maducha, a ostatnio Skurę. Badania nad naturalnym odrzucaniem ściśle związanym z metodą tablic semantycznych podjął ostatnio Bryll. Zbiór tautologii rachunku predykatów jest zbiorem nierozstrzygalnym, więc mechanizacja procesów jest taka, że dla każdego opracowanego algorytmu będzie istniała formuła, dla której ten algorytm dowodu nie znajdzie. Inaczej mówiąc, jeżeli dana formuła należy do konsekwencji matrycowej, to algorytm znajdzie dowód formuły w oparciu o zbiór X jako założeń w skończonej liczbie kroków.
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.