Алгоритм логического вывода по методу Дэвиса и Патнема

1.исключение тавтологий

S’=c S’¹ c

S выполнимо

2.однолитерные дизъюнкты L

да нет

исключение 3.исключение дизъюнктов

S’=S’\L,(LÚS) с чистой литерой L

L=”И” S’=S’\(LÚS’)

S’=c S’¹ c S’=c S’¹ c

S выполнимо вычеркиваются ùL S выполнимо 4. правило

В (ùLÚS) расщепления и