Диссертация (1149226), страница 15

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 15)

Тогда если подстановки, тоитакже унифицируемы иявляется их унификатором.. Рассмотрим три частных случая..85Так как— правильные –формулы, тоиивыполняются равенства:(3.1)(3.2)Таккаки(и— правильные–формулы), то также выполняется следующее равенство:(3.3)Из равенств (3.1), (3.2) и (3.3) следует, чтоСлучай 2...Тогдаи выполняется цепочка равенств:,(3.4)Второе равенство в цепочке выполняется, так каки. Третье равенство в цепочке (3.4) выполняется, так как.

Действительно,,а.Равенства (3.1) и (3.3) в этом случае также выполняются, поэтому имеетместо.Случай 3..Рассматривается аналогично предыдущему случаю.Таким образом,является унификатором подстановоки.В статье [157] А. Воронков сформулировал определение отношенияпоглощения55 для произвольной дедуктивной системы и доказал теорему ополноте стратегии поглощения, соответствующей такому отношению. Внастоящей работе не требуется использовать настолько общие результаты,поэтому для упрощения изложения и самого доказательства мы сформулируемопределениеисчисления55отношенияпоглощения,адаптированноедляконкретного(в том числе добавлено условие транзитивности отношения).В оригинале используется термин «subsumption ordering».86Пусть–секвенций.

Это отношение— отношение на множественазывается отношением поглощения для исчисления, если выполняютсяследующие условия:1. Пусть— применение правила вывода исчисления)и(— правильные –секвенции,, гдене имеющие друг с другом общих свободных переменных. Тогдавыполняется хотя бы одно из условий:а):б) найдется;–секвенциятакаяиявляетсянепосредственным следствием некоторых –секвенций(гдеичто) по какому-либо из правил выводаисчисления2.

Если,, т. е.:и,— правильная.–секвенция,то.3. Еслии, то(свойство транзитивности).Докажем, что сформулированное в начале этого параграфа отношениеявляется отношением поглощения в смысле предыдущего определения.Лемма 3.2. Отношениеявляется отношением поглощения для исчисления.Доказательство леммы вынесено в приложение Б.В частности, из леммы 3.2 следует транзитивность отношения.

Такжеотметим, что заключение любого применения правила переименованияилиправила нормализациипоглощает посылку.Вообще говоря, полнота стратегии поглощения зависит от того, как именноона применяется [50]. В работе [68] в связи с этим вводится понятие допустимойпроцедуры поиска вывода: если начиная с некоторого шага секвенциивсегда остаются в пространстве поиска вывода (т. е. не поглощаются другими87секвенциями) и к этим секвенциям применимо правило вывода,то на некотором шаге процедуры это правило будет обязательно применено.Такое определение подходит для пропозициональных исчислений, где несуществует бесконечной последовательности таких секвенцийвыполняетсяине совпадает с, что для.

Для исчислениямыбудем использовать более сильное условие допустимости. Будем называтьпроцедуру поиска вывода допустимой, если для любых –секвенций,входящих в пространство поиска вывода на некоторых шагах процедуры, и длялюбого правила вывода, применимого к, на некоторомшаге процедуры будет обязательно выведена такая правильная –секвенциячтои,не имеет общих свободных переменных с выведенными ранее–секвенциями (такое же требование должно выполняться, еслиявляетсяаксиомой). Это определение можно формализовать с помощью тех же понятий,что используются в работе [68].Можно убедиться, что алгоритм поиска вывода из параграфа 2.5.4 будетудовлетворять условию допустимости, если использовать его совместно состратегией поглощения следующим образом: перед применением шага 3 удалятьиз множества T все такие секвенции, которые поглощаются секвенциями измножества S.

При этом можно рассматривать такую модификацию алгоритма, вкоторой отсутствует шаг 4, а на шаге 2 возвращаемый алгоритмом результат (вслучае пустого множества T) определяется наличием целевой секвенции в S56.Полноту стратегии поглощения будем доказывать в предположении, чтоиспользуетсядопустимаяпроцедурапоискавывода.Сначаладокажемвспомогательную лемму 3.3, которая может рассматриваться как аналог теоремы2 из статьи А.

Воронкова [157]57.56Таким образом, модифицированный алгоритм продолжает работу даже после порождения целевойсеквенции. При этом если стратегия поглощения полна при использовании такой модификации алгоритма, то онабудет полна и при использовании исходного алгоритма.57Полноту стратегии поглощения при использовании допустимой процедуры поиска вывода можно былобы обосновать и другим способом, по аналогии с доказательством теоремы 7.19 из [68].88Лемма 3.3. Пустьи) — наборы –секвенций,(обладающие следующим свойством: для каждой –секвенции–секвенция, что. Тогда если формулабез применения схемы аксиом–секвенцийнайдется такаявыводима из–секвенций, то она также выводима избез применения схемы аксиом.Доказательство леммы вынесено в приложение Б.Теорема 3.1.

Полнота стратегии поглощения. Стратегия поглощенияявляется полной для исчисления.выводима из –секвенцийИз леммы 3.3 следует, что если формулабез применения аксиом и–секвенций(где –секвенция, то она также выводима извычеркнута) без применения аксиом.Действительно, наборыилеммы 3.3, так каки для каждойвыполняетсяудовлетворяют условиям–секвенции,.3.4. Стратегия упрощения секвенцийВ этом параграфе мы рассмотрим некоторые возможности перестановкиприменений логических правил в исчисленияхи. Перестановочностьприменений правил в логических исчислениях исследуется в статье С. К. Клини[16], а также в учебнике А.

С. Трулстра и Г. Швихтенберга [149]. Как и в пункте2.5.1, мы будем использовать терминологию из статьи С. К. Клини [16]. Нотеперь, в отличие от пункта 2.5.1, применение логического правила (или схемыаксиом)непосредственно предшествует применению логического правила, если между ними расположены только применения структурных правил58.Такие применения правил58иНапомним, что в исчисленииисчисленииназываются смежными.структурными правилами являются правила сокращения, а в— правила сокращения, переименования и нормализации.89Пусть списоквывода:,для исчисления,,в случае, если формуласостоит из следующих правил,,,и,, а такжене содержит отрицательных вхождений символа .При фиксированной формулесписокдля исчисленияопределяетсяаналогично: он содержит одноименные правила вывода исчисления.Далее мы докажем ряд лемм о перестановочности применений правил висчислении, а затем с их помощью докажем основную теорему оперестановочности применений правил в исчисленииЛемма 3.4.

Пусть  — вывод формулы.в исчислении, обладающийсвойством чистоты переменных. Рассмотрим в этом выводе два смежныхприменения логических правили(расположено надразличным вхождениям формул в заключениесписокдля исчисления), принадлежащие. Тогда если правиловходит в, то эти два применения можно переставить (ссохранением свойства чистоты переменных), за исключением трех случаев,которые задаются выписыванием слева от черты вида правила дляот черты — для:и,и справа.В указанных трех случаях перестановку все же можно выполнить приусловии, что собственная переменнаятермприменения правилаприменения правилане входит в.Доказательство леммы вынесено в приложение Б.Лемма 3.5. Произвольный вывод  формулыв исчисленииможноперестроить (без нарушения свойства чистоты переменных, если оно имелось),поднимая наверх любое применение правилаиз спискадля исчислениятаким образом, чтобы оно входило в новый вывод только в следующих случаях: применению правиланепосредственно предшествует применениеаксиомы; боковая формула применения правилавводится непосредственнопредшествующим ему применением логического правила вывода;90 пара, где применение логического правилапредшествует применению правилаили, совпадает с, причем собственная переменнаявходит в термнепосредственноприменения правила,применения правила.В соответствии с соглашением 2.1, формулаявляется очищенной.Поэтому без ограничения общности будем считать, что вывод  обладаетсвойством чистоты переменных.

В противном случае заменим в этом выводесвободные и связанные вхождения переменных таким образом, чтобы этосвойство выполнялось (см. леммы 37 и 38 в § 78 книги [13]). Тогда можноприменятьлемму3.4.Доказательствонезначительноотличаетсяотдоказательства теоремы 2 из статьи С. К. Клини [16] и выполняется индукцией постепени вывода (т. е. по числу применений правил из списка, которыетребуется поднимать наверх), а при фиксированном числе таких применений —индукцией по рангу вывода.

Ранг вывода — это число применений логическихправил, которые находятся выше самого высокого применения правила из списка, но должны находиться ниже этого применения в преобразованном выводе.Теорема 3.2. Произвольный выводформулыв исчисленииперестроить, поднимая наверх любое применение правилаисчисленияможноиз спискадлятаким образом, чтобы оно входило в новый вывод только вследующих случаях: применению правиланепосредственно предшествует применениеаксиомы; боковая формула применения правилавводится непосредственнопредшествующим ему применением логического правила вывода; пара, где применение логического правилапредшествует применению правилаиливходит в терм, совпадает с, причем собственная переменнаяприменения правила.непосредственно,применения правила91Из леммы 2.16 следует, что существует выводисчисленииформулыв, в котором логические правила вывода применяются точно втаком же порядке, что и одноименные правила в выводеобщности будем считать, что вывод.

Без ограниченияобладает свойством чистоты переменных(иначе переименуем переменные этого вывода, как в лемме 3.5). Тогда мы можемприменить лемму 3.5 и переставить желаемым образом применения правил изспискав выводе. По лемме 2.15 новому выводу в исчислениисоответствует вывод формулыправил из спискав исчислении, в который применениявходят требуемым образом.Пользуясь теоремой 3.2, можно обосновать следующую стратегию дляисчисления, которую назовем стратегией упрощения. Если в процессепоиска вывода в исчислениикакое-либо правилоприменения правилаполучена секвенция , к которой применимоиз спискадля, то(будем говорить, чтозаменяется заключениемупрощается), за исключениемслучая, когда боковой формулой этого применения является формула видаи59является одним из правил,,,.

Характеристики

Список файлов диссертации