Диссертация (Автоматический логический вывод в интуиционистских логических исчислениях обратным методом Маслова), страница 9

Кроме того, обратный метод можетиспользоваться как для доказательства утверждений «от противного» (т. е.аналогично методу резолюций и некоторым табличным методам), так и дляпостроения конструктивных доказательств.Кроме указанных преимуществ, С. Ю. Маслов также отмечал [22], чтообратный метод эффективно использует информацию из доказываемой формулыпри поиске вывода (доказательство становится «направленным»), а также что наоснове обратного метода можно создать алгоритм поиска вывода, которыйодновременно является разрешающим алгоритмом для широких классов формул.Таким образом, обратный метод совмещает сильные стороны резолютивныхи табличных методов.

Во-первых, для обратного метода можно адаптироватьмощные стратегии из метода резолюций. Во-вторых, обратный метод обладаетуниверсальностью табличных методов и позволяет получать более естественные ипонятные человеку выводы.1.6. ЗаключениеВ заключение этой главы можно сказать, что современные программыавтоматического доказательства теорем успешно применяются для решения44многих научных и технических задач. Эффективные программы АЛВ могутоперировать десятками и даже сотнями тысяч промежуточных утверждений,управлять процессом поиска вывода при помощи множества эвристическихметодов [128].

Однако решение ряда интересных практических задач, таких каккомплексная, а не частичная верификация программных систем промышленногомасштаба, пока оказывается за гранью возможностей современных программАЛВ [93, 147, 134]. Актуальными задачами в области АЛВ остаютсясовершенствование используемых методов, разработка более эффективныхстратегий поиска вывода и эвристик, оптимизация программных алгоритмов, атакже совершенствование пользовательских интерфейсов для программ АЛВ.В программах АЛВ для интуиционистской логики обычно используютсятабличные методы логического вывода.

Однако существующие программныереализации пока не справляются с достаточно сложными задачами, чтоподтверждается результатами их тестирования, опубликованными на сайте ILTP[144]. В связи с указанной проблемой, особый научный и практический интереспредставляют исследования обратного метода логического вывода. В настоящейкандидатской работе исследуются особенности применения обратного метода кинтуиционистской логике первого порядка.45ГЛАВА 2. ПОСТРОЕНИЕ ИНТУИЦИОНИСТСКОГО ИСЧИСЛЕНИЯОБРАТНОГО МЕТОДА2.1.

ВведениеВ этой главе рассматривается новое многосукцедентное исчислениеобратного метода с унификацией (см. определения в следующем параграфе),которое строится индивидуально для каждой доказываемой формулы такимобразом, чтобы в доказательстве участвовали только ее подформулы.Эта глава также содержит формулировки некоторых исчислений илиотдельных правил вывода, предложенных другими авторами.

При этомиспользуемые этими авторами термины и обозначения приводятся в соответствиес принятыми в настоящей работе.В параграфе 2.2 приводятся основные определения и обозначения. Впараграфе 2.3 описывается стандартная методика, используемая для построенияисчисленийобратногометода.Впараграфе2.4приводитсяпримеринтуиционистского исчисления обратного метода с унификацией — исчислениеиз работы А. Дегтярева и А.

Воронкова [68]. В параграфе 2.5 строится новоемногосукцедентное исчисление обратного метода. В параграфе 2.6обсуждаются отличия этого исчисления от уже существующих исчисленийобратного метода. В параграфе 2.7 приводится пример доказательства формулыобратным методом. В параграфе 2.8 предлагаются некоторые модификацииисчисленийи. В параграфе 2.9 подводятся итоги главы.Основные результаты этой главы изложены в статьях [116, 44, 45].Исчисления m-G3i-inv и m-G3i-inv* из статей [116, 44] являются модификациямиисчисления36, которые имеют в основном отличия технического характера36.Стоит отметить, что сами названия исчислений m-G3i-inv и m-G3i-inv* в указанных статьях выбраны несовсем удачно. Во-первых, по сравнению с G3-системами, в этих исчислениях присутствуют правила сокращения.Во-вторых, правила вывода зависят от доказываемой формулы , но в названиях исчислений этой формулы нет.Поэтому в диссертационной работе используется другой стиль наименования исчислений.462.2.

Основные определения и обозначенияВ этом параграфе приводятся термины и соглашения, используемые в этойи в последующих главах наряду с терминами из параграфа 1.2. Большую частьданных ниже определений можно найти в работе [68] и в книгах [13, 32, 14, 50].Выражение — это терм, формула, подстановка (см. определение в пункте2.2.1), пара подстановок, мультимножество формул (см.

определение в пункте2.2.2), секвенция (см. определение в пункте 2.2.4) и т. д.Свободные и связанные переменные в формуле (выражении) и их вхожденияопределяются стандартным образом, см. [32, с. 55–56].Записьобозначает множество всех переменных выражения— множествовсехегосвободныхпеременных,а,—множество всех его связанных переменных.Замкнутая формула — формулапеременных, т.

е., которая не содержит свободных.Очищенная формула37 — такая формула, в которой все кванторысвязывают разные переменные и ни одна связанная переменная не входитсвободно в .Вырожденный квантор — такой кванторили, что переменнаяневходит свободно в область действия этого квантора.2.2.1. Подстановки и унификацияПодстановка — этоконечное, где все переменныеот переменноймножествоупорядоченныхразличны и каждыйпарвида— терм, отличный.Для подстановкизаписьобозначает областьопределения этой подстановки, совпадающую с множеством переменных37Данный термин используется, например, в работе [34, с. 326].

В статье автора [44] ему соответствуеттермин «ректифицированная формула», а в англоязычной статье [68] — термин «rectified formula».47. Записьобозначает множество термовмножество всех переменных, входящих в термы из,а—.Пустая подстановка, обозначаемая , — это единственная подстановка спустой областью определения.Переименование38 — это подстановка, представляющая собой отображениеодин к одному из своей области определения в нее же.Термназывается свободным для переменнойникакое свободное вхождениеквантораили, гдев, еслине лежит в области действия никакого— переменная, входящая в .Подстановканазывается допустимой для выражения, если для каждоготермсвободен дляДля произвольного выражениядопустимой дляв выражении, выражениев .,и подстановкиобозначает результат одновременной заменывсех свободных вхождений переменныхвтермами.Также будем использовать следующее обозначение: если переменнаяуказывается в выраженииусловии, что подстановка, то записьобозначает выражениеявно, придопустима для .Операция композиции подстановок определяется стандартным образом, см.[50, с.

81]. Композиция подстановокиобозначаетсяили простоВдоказательствах будем пользоваться ассоциативностью операции композицииподстановок, см. [50, с. 81].Сужениепеременныхподстановкина— это подстановка, обозначаемая кактолько те парыиз , для которыхЗаписьобозначает подстановку,что..Множествоунифицируемым, если для него существует унификатор.38и содержащая те и.Унификатором для множества выраженийподстановкамножествоАналог англоязычного термина «renaming», см. [68].называется такаяназывается48Унификатордля множества выраженийназывается наиболееобщим унификатором, если для любого унификаторанайдется такая подстановка, чтомножества выраженийдля этого множества.

Наиболее общий унификатор дляобозначается как.Наиболее общий унификатор подстановоки— это наиболее общийунификатор для множества, состоящего из двух упорядоченных наборов, где.2.2.2. МультимножестваМультимножество39 — обобщение понятия множества, допускающеевключение нескольких экземпляров одного и того же элемента. Мультимножестваопределяются однозначно с точностью до порядка следования элементов.Конечное мультимножество состоит из конечного числа элементов.Для обозначения произвольных конечных мультимножеств (возможно,пустых) используются греческие буквы,и(возможно, с подстрочнымииндексами, со штрихами и т. д.).При записи мультимножеств фигурные скобки опускаются для лучшейчитаемости: вместоЕслиипишется.— мультимножества, тообозначает мультимножество,получающееся объединением их элементов. Записи видамультимножество,получающеесяприсоединениемиликобозначаютмультимножествуэлемента .ЗаписьПустьозначает, что элементивходит в мультимножество .— мультимножества.

Записьэлемент, входящий k раз в , входит не менее k раз в39В англоязычной литературе используется термин «multiset».означает, что каждый.492.2.3. Подформулы, положительные и отрицательные вхожденияПриведенные ниже определения подформул, а также их положительных иотрицательных вхождений являются вполне стандартными, см. [14] и [34].Понятиенепосредственнойподформулысложнойопределяется следующим образом.

Если F имеет видЕсли F имеет видявляетсяили,ее непосредственными подформулами являются формулыформулыиF, то, и только они., то единственной ее непосредственной подформулой. Если F имеет видилинепосредственной подформулой является, то единственной ее.Понятие подформулы определяется рекурсивно. Каждая формула Fявляется подформулой самой себя. Если формулаподформулой формулыявляется непосредственной, которая является подформулой F, тотакжеявляется подформулой F.Под вхождением подформулы G в формулу F будем пониматьфиксированную связную часть формулы F, совпадающую с G. Заметим, чтоданная формула может иметь несколько вхождений в качестве подформулы F.Например, формулаимеет два вхождения в формулуупотребляя«подформула»,терминбудемподразумевать.

В дальнейшем,фиксированноевхождение данной подформулы, если явно не указано обратное.Если G является подформулой (непосредственной подформулой) F, тобудем говорить, что F является надформулой (соответственно непосредственнойнадформулой) G.Будем говорить, что вхождение подформулывхождению подформулыв F и писатьсвязной частью вхождения.в формулу F принадлежит, если вхождениеявляетсяПолярность вхождений подформул определяется следующим образом40.Пустьобозначает вхождение подформулы G в формулу F.