Cтраница 2
Единственная допустимая стратегия удаления состоит в вычеркивании примеров тех m - дизъюнктов, которые уже были выведены на этой же глубине, запоминая при этом, как именно данные примеры были получены. Другими словами, если ЛП, Л / 2, A / 3eRes ( lO, label ( Л / 3) - пример label ( Л /) и N3 и N расположены на одной глубине в I /, то мы можем всюду в Res ( У) заменить N3 на N. Таким образом, АЧ М2, W, jV2 Nl Ny и, возможно, некоторые резолюции с N в качестве первой или второй компоненты будут добавлены к Res ( I /), a все вхождения N3 будут устранены. В исходном пространстве, однако, может использоваться любая полная стратегия доказательства теорем в том случае, когда абстрактное пространство порождается полностью. Например, мы можем так ограничить процедуру ridfindm в proofsearch2, чтобы она порождала резольвенты из S только согласно некоторой полной m - резолюционной стратегии. [16]
Затем обсуждаются некоторые новые правила вывода, связанные с резолюцией. Для m - дизъюнктов определяется вариант резолюции, называемый m - резолюцией, а также определяются m - абстракции. Они отображают множество m - дизъюнктов А на более простое множество В, такое что шфезолюционные доказательства из А отображаются на имеющие подобные структуры m - резолюционные доказательства из В. Преимущество т-аб-стракций состоит в том, что они сохраняют гораздо больше информации о структуре доказательства, чем обычные абстракции. И как следствие имеются простые полные стратегии доказательства теорем, основанные на m - абстракциях. Имеются также стратегии, использующие несколько m - абстракций одновременно, что соответствует одновременному применению нескольких аналогий. Таким образом, мы получаем сильно ограничивающую поиск стратегию, которая не имеет известных аналогов для обычной резолюции и обычных абстракций. Все предлагаемые стратегии, основанные на m - абстракциях, полны. [17]
Th, строится отрицание Ри добавляется к Th, при этом получают новую теорию ТЫ. При этом существует возможность выводить из исходных дизъюнктов дизъюнкты-следствия. Это противоречие свидетельствует о том, что Р выводимо из аксиом Th. Вообще говоря, существует множество стратегий доказательства, нами рассмотрена лишь одна из возможных - нисходящая. [18]
Th, строится отрицание Р и добавляется к Th, при этом получают новую теорию ТЫ. При этом существует возможность выводить из исходных дизъюнктов дизъюнкты-следствия. Если Р выводимо из аксиом теории Th, то в процессе вывода можно получить некоторый дизъюнкт Q, состоящий из одной литеры, и противоположный ему дизъюнкт - Q. Это противоречие свидетельствует о том, что Р выводимо из аксиом Th. Вообще говоря, существует множество стратегий доказательства, нами рассмотрена лишь одна из возможных - нисходящая. [19]
Предположим, что мы ищем доказательство m - дизъюнкта С из S. Если существует доказательство Т m - дизъюнкта С из 5, имеющее глубину d, то существуют доказательства Т1 - ш-дизъюнктов В, из ft ( S) ( l / &), такие что T - ftTi и Tt является начальным поддоказательсгвом Vi. Более точно, W будет начальным поддоказательством доказательства, порожденного процедурой match. С этой целью необходимо модифицировать ndfindm так, чтобы она могла обращаться с векторными m - резолюционными доказательствами. В результате получается стратегия доказательства теорем proofsearch4, полностью аналогичная proofsearch 2, за исключением того лишь, что proofsearch 4 использует одновременно несколько абстракций. [20]
Данный подход представляется достаточно общим для того, чтобы применяться и к другим системам правил вывода, а также к логикам более высокого порядка. Мы определяем класс отображений, называемых функциями абстракции, которые удовлетворяют некоторым условиям. Эти отображения преобразуют множество дизъюнктов Л в более простое множество дизъюнктов В, причем доказательства из Л соответствуют доказательствам из В, имеющим подобную структуру. Абстракции обсуждаются также в [9], но данные там стратегии отличаются от тех, которые представлены ниже. Рассматриваются как синтаксические, так и семантические отображения Один полезный класс нетривиальных семантических абстракций может быть порожден полностью автоматически. Далее мы предлагаем неполную стратегию доказательства теорем, основанную на абстракциях. [21]