Метод резолюции
МЕТОД РЕЗОЛЮЦИИ - один из методов доказательства, используемый в формальной логике. Его можно применять при построении ответов на вопросы, однако он требует слишком много машинного времени, когда задача сложна. Метод по существу представляет собой "доказательство от противного". Справедливость гипотезы устанавливается доказательством того, что ее отрицание, сопоставленное с аксиомами, или заведомо справедливыми утверждениями, приводит к противоречию. Сначала отрицание гипотезы и аксиомы представляется в рамках логического формализма, т.е. как предложения, являющиеся дизъюнкциями литеров. Затем в множестве аксиом отыскивается аксиома, содержащая такой литерал, который после соответствующих подстановок значений переменных входит в противоречие с каким-либо литералом в отрицании гипотезы. Когда к двум предложениям применяется резолюция, противоречащие друг другу литералы взаимно уничтожаются. Затем та же процедура применяется уже к результирующему предложению и т.д. В конце концов, если исходная гипотеза была справедливой, этот процесс приводит к явному противоречию. В качестве примера здесь рассмотрена гипотеза "Марк ненавидит Цезаря". В идеализированном случае, когда фактов, известных о "мире", очень мало (слева), только одна аксиома (5) содержит литерал, противоречащий отрицание гипотезы, и программа быстро завершает доказательство. Когда информации становится больше (аксиомы, выделенные цветом) и появляется еще одна причина для ненависти (8), программа может выбрать не ту аксиому и продолжать процесс, пока не зайдет в тупик, так и не придя к противоречию (справа). В реальных задачах количество возможных вариантов выбора является экспоненциальной функцией от числа аксиом, последнее же обычно очень велико. Поэтому отыскать решение в процессе "слепого" поиска практически невозможно. Рассмотренный здесь пример придуман Е. Рич.
