Cтраница 2
Дэвис и Патнем доказали, что алгоритм Куайна для проверки выполнимости и общезначимости формулы упрощается в применении к конъюнктивной нормальной форме. Проблема общезначимости становится тривиальной: речь идет о проверке тавтологичности каждого дизъюнкта. [16]
В данном и следующем параграфах будут описаны алгоритмы, позволяющие эффективно распознавать выполнимость и общезначимость формул. [17]
Он доказал, что решение этой проблемы в общем случае сводится к ее решению для случая, когда логич. Вместе с тем он установил, что если формула узкого исчисления предикатов содержит лишь одноместные предикатные переменные и число их равно нек-рому натуральному и, то из общезначимости формулы в любой области, состоящей не более чем из 2 предметов, следует ее общезначимость во всякой области. Из этого утверждения следует разрешимость проблемы разрешения для узкого исчисления одноместных предикатов. [18]
На самом деле поиск общей разрешающей процедуры для проверки общезначимости формулы начат давно. Первым пытался найти такую процедуру Лейбниц ( 1646 - 1716), в дальнейшем возобновили попытки Пеано ( примерно на грани XX века) и школа Гильберта в 1920 - х годах. [19]
Легко построить примеры, для которых алгоритмы Кузина и редукции ненамного эффективнее, чем тривиальный алгоритм. Точнее, установлено, что проблема выявления общезначимости ( или выполнимости) формулы исчисления высказываний NP-полна. Не вдаваясь в рассуждения, выходящие за рамки этой книги, отметим, что указанный факт означает ничтожность вероятности существования эффективного общего алгоритма для проверки выполнимости или общезначимости формул исчисления высказываний. [20]
Обратимся теперь к вопросу об общих методах доказательства общезначимости формулы и посмотрим, что мы можем здесь заимствовать из исчисления высказываний. Теорема 2.2 ( если теперь Л eq В приписать смысл, соответствующий нашей теперешней оценочной процедуре) и теорема 2.3 переходят в новое исчисление без изменения. В доказательствах используются по существу прежние рассуждения. Сущность теоремы 2.1 заключается в возможности доказать общезначимость формулы, не разделяя ее на простые компоненты. Та же техника применяется и в исчислении предикатов. Назовем формулу исчисления предикатов простой в исчислении высказываний, если в ней отсутствуют сентенциональные связки. [21]