Процедура - доказательство
Cтраница 3
 |
К применению обобщенной теоремы для совпадения из трех потоков хотя бы двух. [31] |
Можно видеть, что отмеченное выше свойство совпадения задних фронтов результирующего потока с теми или иными задними фронтами исходных потоков сохраняется. А поэтому ко всем этим случаям полностью применима процедура доказательства, выполненная в § 1.2.2. Это позволяет нам сформулировать следующую обобщенную теорему. [32]
В основе теории резолюции лежат ранние исследования Эрбрана ( 1930) процедур доказательства в логике дизъюнктов. В книге Ченя и Ли ( 1973) дается ясное введение в теорию и приложения резолюции. [33]
Мы изложим здесь некоторые результаты о неразрешимости, показывающие, что многие из условий в теоремах предыдущего раздела не могут быть заметно ослаблены. Так как класс уравнений, рассматриваемых в этом разделе, включает уравнения, для которых этапы I и III процедуры доказательства существования, описанной в гл, 11, были обоснованы ранее, то неразрешимость задачи Дирихле в этих случаях связана с отсутствием граничной оценки градиента. В действительности несуществование такой оценки для этих уравнений может быть показано непосредственно с помощью техники, аналогичной той, которая используется далее. [34]
Наконец, словосочетание вычислительная геометрия для некоторых может означать деятельность в области доказательства геометрических теорем с помощью ЭВМ. Хотя это и увлекательное исследование, но оно дает намного больше информации о наших эвристиках, служащих для доказательства теорем и понимания процедур доказательства, чем данных о геометрии как таковой, и поэтому мы здесь этим заниматься не будем. [35]
Естественная область исследований, подсказываемая материалом этой главы - поиск практически важных задач, про которые можно доказать, что они трудно разрешимые. Работу в этом направлении проделали Фишер, Рабин [1974], исследовавшие сложность задач с элементарными арифметическими операциями, Кук, Рекхау [1974], изучившие процедуры доказательства теорем 2), Хант [1974], рассмотревший ряд задач из теории языков, и некоторые другие авторы, упомянутые в замечаниях по литературе. [36]
Для реализации естественного языка на ЭВМ требуется формализовать как его синтаксис, так и семантику. Они показали, что хорновских дизъюнктов оказывается достаточно для выражения произвольной контекстно-свободной грамматики ( КСГ), что вопросы относительно структуры предложений ЕЯ можно формулировать как целевые утверждения и что различные процедуры доказательства, применяемые к логическим представлениям ЕЯ, соответствуют различным стратегиям синтаксического анализа. [37]
В приведенных выше примерах мы показали, что заключения следуют из данных фактов. Обоснование того, как заключение следует из аксиом, называется доказательством. Процедура нахождения доказательств называется процедурой доказательства. В главах 4 - 9 мы дадим такие процедуры доказательств, которые для нахождения доказательства механически используют правила вывода. Эти процедуры доказательств очень эффективны. Читатель легко обнаружит, что три предыдущих примера чрезвычайно легко доказать, если использовать такие процедуры доказательств. [38]
Правило резолюций есть правило вывода, которое порождает резольвенты для множества дизъюнктов. Это правило было введено в 1965 г. Робинсоном. Оно более эффективно, чем предыдущие процедуры доказательств такие, как прямое применение теоремы Эрбрана, используемое Гилмором, и теоремы Девиса и Патнема. Прежде чем доказать это утверждение, рассмотрим один пример из планиметрии. [39]
Свойства адаптивности управляющего алгоритма проявляются следующим образом. Выбранная группа аксиом является исходной для алгоритма синтеза программ, осуществляющего синтез проектируемой технологии производства, а соответственно и синтез программ управления производственными единицами из программных модулей, реализующих элементарные операции и содержащихся в базе ресурсов. Ядром системы автоматизированного синтеза программ является процедура доказательства теорем. [40]
Понятия абстракции, m - абстракции и ограниченной ш-аб-стракции приводят к широкому спектру новых единообразных полных процедур доказательства для исчисления предикатов первого порядка. Вероятно, такие же стратегии с небольшими изменениями применимы и к логикам более высокого порядка. Эта техника является более общей, чем использование современных единообразных процедур доказательства. Иными словами, каждый вывод контролируется более осмысленным образом структурой задачи в целом, а не локальными свойствами участвующих в выводе дизъюнктов. К тому же при завершении поиска число абстрактных дизъюнктов более ограниченно, чем в середине, поскольку абстракция целевого дизъюнкта должна быть выведена за небольшое число шагов. [41]
В ряде следующих параграфов мы будем пользоваться конструкциями самого Гильберта; они сопряжены с довольно ограничительными предположениями, которые на протяжении нескольких десятилетий считались существенными. Однако идейная сторона гильбертовского подхода ясна из приведенной выше цитаты и не связана с такими ограничениями. Смысл этого высказывания Гильберта сводится к тому, что для теорем существования важны не столько процедуры доказательств, сколько тщательно продуманные определения. Это делает Гильберта родоначальником метода, который сейчас широко используется во всем анализе и известен под названием метода слабых решений. В результате такого подхода возникла, например, теория обобщенных функций ( распределений) Шварца. Кроме того, это высказывание Гильберта послужило толчком к возникновению ряда теорий, которые мы будем обсуждать в этой и последующих главах и которые имеют целью освободить гильбертовские построения от упомянутых ограничений. [42]
Комбинируя множество правил вывода с некоторой стратегией их применения, получаем алгоритм, называемый процедурой доказательства, который, очевидно, можно закодировать в виде программы для ЭВМ. Процесс исполнения такой программы с целью порождения логических выводов из логических предложений, выступающих в качестве входных данных, называется автоматическим доказательством теорем. Исследования в области автоматического доказательства теорем в течение трех последних десятилетий, причем очень значительные исследования, отражают давнее стремление к систематизации математических доказательств. Первые запрограммированные процедуры доказательства применялись поэтому в основном для доказательства математических теорем. К их созданию побуждала надежда, что компьютеры докажут существенные теоремы, доказательства которых окажутся слишком длинными или слишком трудными, чтобы их можно было получить немеханическими методами; можно было бы ожидать тогда, что компьютеры ускорят темпы математических открытий. [43]
Будем считать, что заданы программа Р и соответствующее множество гипотез Hyp. Процедура доказательства работает непосредственно с программой Р, которая может содержать переменные. Но цель G и сгенерированное множество А не должны содержать переменных. Вообще говоря, процедуру доказательства несложно модифицировать, чтобы она, дополнительно к возвращаемым множествам гипотез, в качестве решения возвращала бы подстановки для переменных, так что ограничение для G не является существенным. Узлы в промежуточных деревьях для процедуры доказательства - это цели, которые могут содержать переменные и атомы. Используемые при этом деревья называются целевыми. [44]
Класс встроенных MV-зависимостей был обнаружен в работах Fagin [ 1977с ] и Delobel [1978], а в работах Parker, Parsaye-Ghomi [1980], Sadiv, Walecka [1979] было показано, что для класса одних EMV-зависимостей не существует полной, конечной аксиоматизации. Процедуру доказательства вы водимости для более широкого класса зависимостей, которые определены в гл. В работах Beeri, Vardi [ 1980a, b ], а также Chandra, Lewis, Makowsky [1981] показано, что выводимость для этого класса зависимостей неразрешима. Здесь нет противоречия, поскольку процедура доказательства выводимости включает как конечные, так и бесконечные отношения. Утверждение о выводимости может иметь бесконечный контрпример и не иметь конечного. [45]
Страницы: 1 2 3 4