О графовом расширении метода резолюции для булевых формул

В работе описывается новое расширение метода резолюции, использующее графовое представление опровержений булевых формул в конъюнктивной нормальной форме. Доказывается, что невыполнимость булевой формулы равносильна существованию для неё графового опровержения.