Часть 2. Специальные вопросы теории интеллектуальных систем

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

Г. В. Боков


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

Ключевые слова: Метод резолюции, графовые опровержения, невыполнимость, булевы формулы.