Cтраница 1
Общезначимость формул ( М) - ( М4) в произвольной топологической булевой алгебре легко следует из III. [1]
Установить общезначимость формул 34, 35 и 36 теоремы 2.12, рассматривая все составляющие их формулы как простые. [2]
Доказательство общезначимости формулы или, что все равно, противоречивости ее отрицания с иелыо сокращения числа анализируемых вариантов выполняется так называемым методом резолюций или резольвенций. [3]
Алгоритм Кузина для проверки выполнимости и общезначимости формулы ( § 1.1.7) упрощается в применении к КНФ. Прежде всего, проблема общезначимости становится тривиальной: речь идет о проверке тавтологичности каждого дизъюнкта. Проблема выполнимости более интересна. Предположим для простоты, что проверяемая КНФ - приведенная. [4]
Алгоритм редукции решает ту же задачу проверки общезначимости формулы, но используется в том случае, когда в формуле содержится достаточно много импликаций. [5]
Обратимся теперь к вопросу об общих методах доказательства общезначимости формулы и посмотрим, что мы можем здесь заимствовать из исчисления высказываний. Теорема 2.2 ( если теперь Л eq В приписать смысл, соответствующий нашей теперешней оценочной процедуре) и теорема 2.3 переходят в новое исчисление без изменения. В доказательствах используются по существу прежние рассуждения. Сущность теоремы 2.1 заключается в возможности доказать общезначимость формулы, не разделяя ее на простые компоненты. Та же техника применяется и в исчислении предикатов. Назовем формулу исчисления предикатов простой в исчислении высказываний, если в ней отсутствуют сентенциональные связки. [6]
Алгоритм редукции, о котором сейчас пойдет речь, позволяет доказывать общезначимость формул с помощью приведения к абсурду. Это особенно удобно, когда формула содержит много импликаций. [7]
Были построены исчисления, в рамках к-рых удалось полностью формализовать св-во универсальной общезначимости формул логики предикатов первого порядка - таковым является исчисление предикатов первого порядка. [8]
Поскольку метод аналитических таблиц основан на процедуре опровержения, то для доказательства общезначимости формулы X надо построить дерево ( таблицу) для ЛХ ( - Х), которое будет замкнутым. [9]
Уместно воспользоваться той же терминологией и теми же символами, что и раньше, поскольку приведенное определение общезначимости формулы представляет собой лишь расширение прежнего. Очевидно, при установлении общезначимости формулы истинностные таблицы должны уступить место процессам рассуждения. С другой стороны, для установления того, что формула не общезначима, достаточно будет одного поля D и одного приписывания, основанного на этом поле. Например, четвертая строка помещенной выше таблицы показывает, что рассматриваемая формула не является общезначимой. Легкость, с которой устанавливается, что некоторая формула не является общезначимой, может показаться читателю неожиданной. [10]
Так как в этой формуле заключение теоремы G опровергается, то и процедуры поиска доказательства называются процедурами поиска опровержения, т.е. вместо доказательства общезначимости формулы доказывается, что отрицание формулы противоречиво, и потери общности нет. [11]
Это продолжалось до тех пор, пока Черч [1] и Тьюринг [1] независимо не доказали, что не существует никакой общей разрешающей процедуры, никакого алгоритма, проверяющего общезначимость формул в логике первого порядка. [12]
Уместно воспользоваться той же терминологией и теми же символами, что и раньше, поскольку приведенное определение общезначимости формулы представляет собой лишь расширение прежнего. Очевидно, при установлении общезначимости формулы истинностные таблицы должны уступить место процессам рассуждения. С другой стороны, для установления того, что формула не общезначима, достаточно будет одного поля D и одного приписывания, основанного на этом поле. Например, четвертая строка помещенной выше таблицы показывает, что рассматриваемая формула не является общезначимой. Легкость, с которой устанавливается, что некоторая формула не является общезначимой, может показаться читателю неожиданной. [13]
Задача выяснения того, является ли некоторое выражение формулой, достаточно проста. Напротив, выявление выполнимости или общезначимости формулы может оказаться довольно нудной процедурой. В § 1.1.6 мы видели, что формула, содержащая k различных высказываний, допускает 2k интерпретаций. Заманчиво иметь более эффективный алгоритм проверки, чем последовательный просмотр всех интерпретаций. В последующих параграфах будут представлены основные результаты, полученные в этой области. [14]
Для класса HI все просто: общезначимость формулы со свободными переменными равносильна общезначимости ее замыкания ( которое получается, если навесить кванторы всеобщности по всем переменным), поэтому формулы класса Щ по существу ничем не отличаются от бескванторных. [15]