Метод - резолюция
Cтраница 3
Чтобы доказать выполнимость или невыполнимость предложения методом резолюций, достаточно вывести пустой дизъюнкт из соответствующего множества дизъюнктов. Если мы получим пустой дизъюнкт, противоречивость будет следствием предположения - чр, следовательно, мы докажем, что предложение ( р общезначимо. [31]
Примером метода моделирования процесса рассуждений может служить метод резолюций [31 ], предназначенный для работы с логическими БЗ. [32]
Как и алгоритм Девиса и Патнема, метод резолюций непосредственно обобщается на исчисление предикатов в случае, когда эрбранова область конечна. [33]
Невыполнимость этого конечного множества действительно можно доказать методом резолюций в рамках логики высказываний. [34]
Этот пример неоднократно использовался для иллюстрации различных вариантов метода резолюций. [35]
Следующий пример показывает, как формализуются предложения и методом резолюций эффективно доказываются теоремы при переходе к соответствующим формализациям. [36]
 |
Семантический граф, отображающий процедуру метода резолюции для сложного условного прампла синода. [37] |
На рис. 13.5 представлен семантический граф, отображающий процедуру метода резолюции для указанного примера. [38]
Универсальные ( полные) методы обнаружения выводимости ( например, метод резолюций [6, 25]) при использовании в задачах с ограниченными ресурсами недостаточно эффективны и нуждаются в тех или иных дополнительных средствах независимо от разрешимости теории. Кроме того, даже при отсутствии ограничений на ресурсы в неразрешимых ( полуразрешимых) теориях возникает проблема принятия решения в случае, если доказываемая формула невыводима, а признаков этого не обнаруживается ни сразу, ни в процессе доказательства. При этом учет ресурсных ограничений оказывается полезным сам по себе для построения решающих правил, в частности, прерывающих бесконечный процесс поиска вывода. [39]
Далее изучаются аксиоматический метод доказательства, метод таблиц Бета и метод резолюций. Метод резолюций вместе с алгоритмом унификации положен в основу логического программирования. Для обоснования этих методов приводятся соответствующие теоремы корректности и полноты. [40]
Главный скачок был сделан Робинсоном [1], который ввел так называемый метод резолюций. После введения метода резолюций были предложены некоторые стратегии в целях увеличения его эффективности. В этой главе мы будем доказывать теорему Эрбрана. [41]
Мы увидим, что преимущество хорновских дизъюнктов при поиске вывода методом резолюции заключается в наличии единственного входа - положительной литеры при поиске партнера для применения резолюции к отрицательной литере. Это приводит к систематическому методу поиска в глубину слева направо при попытках применять резолюцию и производить подстановки; этот метод напоминает программирование с бектрекингом. [42]
Книга посвящена детальному изложению всего круга проблем, связанных с так называемым методом резолюций Этот метод наиболее известен и широко используется в современных работах по доказательству на ЭВМ математических теорем и вообще при построении систем искусственного интеллекта. Описываются применения метода к таким, например, актуальным для всякого системного программиста задачам, как автоматический анализ и синтез программ В приложении описаны другие методы и некоторые результаты последних лет, знакомство с которыми необходимо при изучении проблематики автоматического доказательства теорем. [43]
Первоначально он также предназначался для исчисления С, и для стандартизованных формул метода резолюций оба метода примерно эквивалентны. При этом следует отметить, что наиболее выгодные для обратного метода стандартизации по сути как раз противоположны таковым для резолюций. Более того, этот метод нетрудно распространить на произвольные секвенциальные исчисления без правил сечения. В этом смысле можно сказать, что соотношение рассматриваемых методов вполне аналогично соотношению теоремы Эрбрана для стандартных формул и всего комплекса теорем об устранении сечения. [44]
Для секвенций стандартного вида ( того самого, приведение к которому предполагается методом резолюций) не составляет труда извлечь из второй формы теоремы Эрбрана следующий частный случай теоремы Генцена. [45]
Страницы: 1 2 3 4