Главная >> Диссертации - все темы

Pages: |

| 2 |

«АВТОМАТИЧЕСКИЙ ПОИСК НАТУРАЛЬНОГО ВЫВОДА В КЛАССИЧЕСКОЙ ЛОГИКЕ ПРЕДИКАТОВ Диссертация на соискание ученой степени кандидата философских наук ...»

-- [ Страница 1 ] --

Московский государственный университет им. М.В. Ломоносова

Философский факультет

Кафедра логики

На правах рукописи

ШАНГИН ВАСИЛИЙ ОЛЕГОВИЧ

АВТОМАТИЧЕСКИЙ ПОИСК НАТУРАЛЬНОГО ВЫВОДА

В КЛАССИЧЕСКОЙ ЛОГИКЕ ПРЕДИКАТОВ

Диссертация на соискание ученой степени кандидата философских наук

Специальность 09.00.07 – Логика

Научный руководитель:

проф. Бочаров В.А.

Москва 2004

Введение Актуальность темы исследования. Проблема поиска логического вывода традиционно считается одной из центральной тем логики. Бурное развитие данной проблематики в XX веке стимулировали, с одной стороны, фундаментальные работы Г. Генцена и Ж. Эрбрана и, с другой, появление ЭВМ. Возможность использования ЭВМ в процессе поиска логического вывода привела к появлению проблематики автоматического (машинного) поиска логического вывода.

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

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

В диссертационном исследовании тема автоматического поиска логического вывода ограничивается поиском вывода в натуральном исчислении типа Куайна в классической логике предикатов.

Натуральные системы типа Куайна, в отличие от натуральных исчислений типа Генцена, содержат прямое правило удаления квантора существования. Как следствие, в натуральных системах типа Куайна между посылками и заключением не всегда имеет место отношение логического следования.

Основное внимание авторы программ автоматического поиска натурального вывода обычно уделяют исчислениям типа Генцена. Непрямое правило удаления квантора существования в таких исчислениях предполагает построение дополнительного подвывода, гарантирующего наличие отношение логического следования между посылками и заключением. Поскольку построение дополнительного подвывода приводит к усложнению вывода, удобнее, по нашему мнению, пользоваться прямым правилом удаления квантора существования, т.е. искать вывод в исчислениях типа Куайна.

Степень разработанности проблемы. Долгое время исследования в области автоматического поиска логического вывода были сосредоточены на поиске вывода с помощью метода резолюции, секвенциальных и аналитико-табличных типов логического вывода.

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

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

Исчисления последнего вида особенно интенсивно исследуются на предмет автоматического поиска в них вывода в конце 80-х – начале 90-х гг. ХХ века.

Так, Дж. Поллок [Pollock] предложил программу поиска натурального вывода OSCAR в классической логике предикатов (а также в некоторых неклассических логиках) с использованием сколемовских термов. Он показал, что OSCAR работает в раз эффективнее программы OTTER [Pollock], основанной на методе резолюций. С другой стороны, круг логических проблем, которые решает OSCAR, шире, чем аналогичный круг для OTTER. Дж. Поллоком была выдвинута также гипотеза, что OSCAR обладает свойством семантической полноты, т.е. что OSCAR может найти вывод любой общезначимой формулы классической логики предикатов.

Д. Пеллетье [Pelletier] предложил программу поиска натурального вывода Thinker в классической логике предикатов (а также в некоторых неклассических логиках) с предикатом равенства. Показывается, что Thinker решает 75 тестовых проблем для произвольного алгоритма поиска вывода в классической логике предикатов с предикатом равенства. Thinker не обладает свойством семантической полноты, поскольку количество переменных, которые используются в выводе, заранее ограничено.

У. Сиг вместе с Дж. Бернсом [Sieg], [Sieg & Byrnes] предложили программу автоматического поиска натурального вывода CMU PT в классической логике (авторы также рассматривают возможность обобщения программы на неклассические логики).

Специфика данного алгоритма состоит в том, что натуральный вывод строится не прямым, а косвенным образом. Сначала строится вывод в т.н. промежуточном исчислении, а затем показывается, каким образом можно преобразовать вывод в промежуточном исчислении в натуральный вывод. Авторы показывают, что CMU PT обладает свойством семантической полноты.

Д. Ли [Li] предложил программу поиска натурального вывода ANDP в классической логике. Особенно подчеркивая прикладное значение ANDP, Д. Ли дает машинные доказательства некоторых известных проблем математической логики:

проблемы остановки машины Тьюринга, проблемы зависимости некоторых аксиом в формализации проективной геометрии и др. Вопрос, обладает ли ANDP свойством семантической полноты, остается открытым.

В.А. Бочаров, А.Е. Болотов и А.Е. Горчаков [Болотов и др.] предложили алгоритм поиска натурального вывода Prover для классической логики предикатов.

Спецификой Prover является поиск вывода в натуральных исчислениях типа Куайна с использованием абсолютно и относительно ограниченных переменных. В процессе поиска вывода Prover использует также сколемовские термы. Касаясь вопроса о семантической полноте для Prover, авторы предлагают пути решения данной проблемы.

Однако доказательства данного факта для Prover предложено не было.

Группа исследователей под руководством Н.А. Шанина [Шанин и др.] предложила процедуру поиска натурального вывода типа Генцена в классической логике высказываний. Отличительной особенностью данной процедуры является поиск вывода в секвенциальном исчислении. Затем полученный вывод в секвенциальном исчислении перестраивается в натуральный вывод типа Генцена. Отмечая пионерский характер данной работы (она вышла в 1964 году), подчеркнем, что вопрос о семантической полноте процедуры авторами не ставился, поскольку в формулах, для которых требуется найти натуральный вывод, разрешается использовать не более трех пропозициональных переменных. В значительной степени на работы группы под руководством Н.А. Шанина опирается У. Сиг.

Цель и задачи исследования.

Целью диссертационного исследования является пересмотр алгоритма поиска натурального вывода типа Куайна в классической логике предикатов первого порядка, предложенного В.А. Бочаровым, А.Е. Болотовым и А.Е. Горчаковым, и доказательство для этого алгоритма теорем о семантической непротиворечивости и семантической полноте.

Для достижения данной цели ставятся и решаются следующие задачи:

Предложить доказательство теоремы о семантической непротиворечивости для натурального исчисления типа Куайна с механизмом использования в выводе абсолютно и относительно ограниченных переменных.

Представить содержательное описание алгоритма поиска вывода в виде формальных правил поиска вывода.

Опираясь на вышеупомянутый результат, доказать теорему о семантической непротиворечивости алгоритма поиска вывода в данном исчислении.

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

Показать с помощью представления алгоритмического вывода в виде древовидной структуры конечность ветвления в произвольном блоке.

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

Методологические основы и источники исследования.

При решении поставленных задач автор опирался на современный аппарат символической логики. В диссертационной работе использовались формулировки систем натурального вывода, предложенные В.А. Бочаровым, Е.К. Войшвилло, Г. Генценом, Ф. Пеллетье, Дж. Поллоком, В.А. Смирновым и др.

В основе описанного в диссертационном исследовании алгоритма поиска вывода лежит алгоритм поиска вывода в классической логике предикатов, предложенный А.Е. Болотовым, В.А. Бочаровым и А.Е. Горчаковым. В процессе использования написанной этими авторами программы возникла необходимость модифицировать данный алгоритм, определенным образом упростить процедуру поиска натурального вывода и четко сформулировать процедуру унификации.

Научная новизна исследования.

В диссертационном исследовании предложен метод доказательства теоремы о семантической непротиворечивости для натурального исчисления типа Куайна.

Показана гибкость данного метода, позволяющая применять его и к другим натуральным исчислениям этого типа, отличительными свойствами которых являются наличие прямого правила удаления квантора существования и использование в выводе абсолютно и относительно ограниченных переменных.

В процессе исследования получены следующие новые результаты, выносимые на защиту:

Предложено оригинальное доказательство теоремы о семантической непротиворечивости для натурального исчисления типа Куайна с абсолютно и относительно ограниченными переменными.

Модифицирован стандартный алгоритм унификации для временных переменных и сколемовских функций с целью работы с абсолютно и относительно ограниченными переменными.

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

Обоснован прямой метод доказательства теоремы о семантической полноте алгоритма поиска натурального вывода. С помощью данного метода предлагается оригинальное доказательство теоремы о семантической полноте для алгоритма поиска натурального вывода в исчислениях типа Куайна.

Предложено оригинальное доказательство теоремы о семантической полноте для системы натурального вывода типа Куайна, следующее из теоремы о семантической полноте для алгоритма поиска вывода в данной системе.

Практическая значимость. Разработанный алгоритм поиска натурального вывода в исчислениях типа Куайна может служить основой для создания компьютерных реализаций, которые, в свою очередь, могут использоваться в педагогической практике, облегчая усвоение основ дедукции.

Содержание диссертационного исследования может быть использован для разработки специального курса по автоматическому поиску логического вывода.

Апробация работы. Основные положения и результаты диссертационного исследования докладывались на VI и VII Международных научных конференциях «Современная логика: проблемы теории, истории и применения в науке» (СанктПетербург, 2000 и 2002), IV Международной конференции «Смирновские чтения»

(Москва, 2003) и XII Международном конгрессе по логике, философии и методологии науки (Овьедо, 2003).

Структура диссертации. Диссертация состоит из Введения, 4-х глав:

«Автоматический поиск натурального вывода: история вопроса», «Анализ системы натурального вывода BMV», «Алгоритм поиска вывода в системе BMV» и «Анализ алгоритма поиска вывода в системе BMV», Заключения и Литературы.

Глава 1. Автоматический поиск натурального вывода: история вопроса § 1.1. Натуральный вывод как тип логического вывода Моментом появления натурального вывода (НВ) как одного из типов логического вывода традиционно считается выход в 1934 году статьи Г. Генцена «Исследования логических выводов» [Генцен] и статьи С. Яськовского «Правила введения посылок в формальной логике» [Jaskowski].

В англоязычной литературе системы НВ называются «natural deduction». В отечественной литературе системы НВ иногда называются «естественным выводом».

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

Г. Генцен писал: «Я хотел прежде всего построить такой формализм, который был бы как можно ближе к применяющимся в действительности рассуждениям»

[Генцен, с. 10]. Далее он определяет свою задачу более точно: «Мы хотим построить формализм, по возможности точно передающий логические заключения, которые в действительности встречаются в математических доказательствах» [Генцен, с. 17].

Созданию С. Яськовским систем НВ способствовало замечание Я. Лукасевича, что «математики строят свои доказательства, используя не аксиоматический метод, а иные способы рассуждения; главным образом, математики берут «произвольные посылки» и смотрят, что из этих посылок можно вывести» [Pelletier, с. 4].

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

Приведем цитаты, показывающие достоинства НВ перед другими типами логического вывода. «Естественный вывод гораздо более тонкий инструмент, чем семантические таблицы, обладающий большой аналитической силой и легко модифицируемый» [Непейвода, с. 297]. «Наиболее удобным способом ее (логики предикатов – В.Ш.) задания является система натурального вывода» [Ивлев, с. 95].

«Для применения в качестве логического аппарата наиболее удобными (системами исчисления предикатов – В.Ш.) являются натуральные системы (системы натурального вывода)» [Войшвилло, с. 85].

Размышляя о преимуществах натурального вывода перед методом резолюции, Д. Пеллетье пишет: «Я предположил, что представление вывода в виде натурального на самом деле обладает значительными преимуществами с познавательной точкой зрения:

такое максимально обобщенное представление позволяет студентам глубже проникнуть в структуру логических проблем» [Pelletier, с. 6].

Характеризуя гильбертовские исчисления, авторы [Смирнов и др., с. 21] пишут: «Сами способы построения и выводов в этих системах в значительной степени не соответствуют естественным способам рассуждений». Характеризуя секвенциальные и аналитико-табличные исчисления, эти же авторы пишут: «Сам стиль осуществления этих процедур во многом перестает носить «естественный» характер, т.е. перестает соответствовать обычным способам рассуждений» [Смирнов и др., с. 21].

аксиоматически, в виде табличного исчисления и т.д. Не все из них одинаково удобны для анализа выводов. Самые широкие возможности в этом плане открывают секвенциальные исчисления и системы натурального вывода» [Быстров, с. 139].

«Во всех этих приемах (секвенциальные исчисления и метод резолюции – В.Ш.) процедура выведения одних положений из других или вообще не представлена, или осуществляется в таком виде, который весьма далек от того, что понималось под выводом в истории логики. И секвенции, и метод резолюции – это скорее алгоритмы проверки общезначимости утверждений, чем вывод. Все они строятся на основе чисто аналитических процедур, в то время как традиционное понятие вывода представляет собой метод синтеза доказуемого утверждения из имеющихся посылок» [Болотов и др., с. 172].

Из перечисленного можно сделать вывод, что НВ обладает определенными преимуществами перед другими типами логического вывода: удобство и простота, конгениальность естественным рассуждениям и др.

Что касается дедуктивной силы НВ, то, представляя НВ, Г. Генцен конструктивно показал, что в классической логике предикатов НВ дедуктивно эквивалентен исчислению секвенций и гильбертовскому исчислению, т.е. вывод некоторой формулы в одном исчислении можно перестроить в вывод этой же формулы в другом исчислении [Генцен].

Также отметим, что в нашем исследовании используются только системы НВ для классической логики. Поэтому рассмотрение НВ для неклассических логик выходит за рамки нашего исследования. Подробнее о системах НВ для неклассических логик см. [Basin et al].

Возможны различные классификации систем НВ [Pelletier], [Смирнов].

Например, Д. Пеллетье выделяет девять основных пунктов («nine choice points»), по которым можно классифицировать системы НВ. В то же время он признает, что «многообразие систем НВ делает весьма затруднительным выделение необходимых и достаточных признаков, которые позволили бы однозначно назвать некоторую логическую систему натуральным выводом» [Pelletier, с. 11].

отечественными учеными, мы будем добавлять их в качестве примеров в соответствующие разделы классификации.

Первым основным пунктом является тип представления натурального вывода:

1) в виде дерева (Г. Генцен, Н.А. Шанин, Н.Н. Непейвода);

В.И. Маркин), где подвыводы обозначаются некоторыми графическими объектами (скобками, квадратными скобками, линиями и др.);

3) в виде линейного вывода (С. Яськовский, У. Куайн), где подвыводы обозначаются различными (числовыми) префиксами;

Е.К. Войшвилло).

Вторым основным пунктом является присутствие (Г. Генцен, У. Куайн, Е.К. Войшвилло) или отсутствие (С. Яськовский) в системе НВ некоторых аксиом наряду с правилами вывода.

Назовем систему НВ симметричной, если в ней для любого логического символа (связки или квантора) содержатся хотя бы одно правило введения и хотя бы одно правило удаления (исключения). Тогда наличие (Г. Генцен, Н.Н. Непейвода, В.А. Бочаров и В.И. Маркин) или отсутствие (Д. Пеллетье, Е.К. Войшвилло, Дж. Поллок, А.М. Анисов) симметричности в системе НВ – это третий основной пункт.

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

Обычным непрямым правилом является в: если из посылки С выводима формула В, значит, можно построить вывод формулы С В.

Например, Г. Генцен предложил следующее непрямое правило и: из формулы А В, подвывода С из посылки А и подвывода С из посылки В выводима формула С.

Однако можно предложить прямое правило и: из А В, А С, В С выводима формула С, или из А В, ¬А выводима формула В.

Д. Пеллетье также отмечает, что прямые и непрямые правила можно вводить для других пропозициональных связок (например, ¬, ).

Следующие основные пункты 5-9 касаются работы с переменными в системах НВ. Д. Пеллетье отмечает нетривиальность проблемы работы с переменными в системах НВ в сравнении с другими типами логического вывода.

Количество кванторов, которые используются в системах НВ, – это пятый основной пункт. Подавляющее большинство авторов используют и квантор общности, и квантор существования при формулировке своих систем НВ. Исключение составляет, например, С. Яськовский.

Шестой основной пункт – наличие прямого (У. Куайн, В.А. Бочаров и В.И. Маркин) или непрямого (Г. Генцен, Н.Н. Непейвода) правила удаления квантора существования.

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

В таких системах НВ появляется наряду с понятием вывода понятие завершенного вывода, т.е. вывода, в котором заключение логически следует из всех неисключенных посылок этого вывода. Далее мы подробнее остановимся именно на данном основном пункте.

В системах НВ формулировка правила в предполагает наличие произвольной или новой, ранее не встречающейся в выводе переменной. Седьмой основной пункт – это различные способы, которые гарантируют, что переменная в формулировке правила в является произвольной.

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

В.И. Маркиным, наличие произвольной переменной в формулировке правила в задается неявным образом.

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

Восьмым основным пунктом является разделение всех систем НВ на те, которые допускают вхождение свободных переменных в посылки и заключение выводов (У. Куайн, В.А. Бочаров и В.И. Маркин), и на те, которые не допускают посылок и заключений такого вида, т.е. посылки и заключения в таких системах могут быть только предложениями (В.А. Смирнов).

Дополнительно отметим, что возможна условная (В.А. Бочаров и В.И. Маркин) и универсальная (Д. Пеллетье) интерпретация свободных переменных.

Наконец, девятым основным пунктом является наличие (Дж. Поллок, В.А. Смирнов) или отсутствие (У. Куайн, В.А. Бочаров, В.И. Маркин) особых термов в формулировках кванторных правил.

Например, В.А. Смирнов формулирует кванторные правила в, и с помощью -термов, содержательно трактующихся как неопределенные дескрипции.

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

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

В оригинальной системе, предложенной Г. Генценом, имеется непрямое правило удаления : из формулы xA(x) выводима формула С, если формула С выводима из A(a), где a – новая, ранее не встречавшаяся в выводе константа. Таким образом, чтобы получить по такому правилу формулу С из формулы xA(x), необходимо построить вспомогательный вывод (он называется подвыводом) формулы С из формулы A(a). Только после построения такого подвывода можно утверждать, что из формулы xA(x) выводима формула С.

По-видимому, первым, кто обратил внимание на неудобство применения этого правила и кто предложил альтернативный вариант удаления, был У. Куайн [Quine]. В статье «On natural deduction» он сформулировал прямое правило удаления : из формулы xA(x) выводима формула A(y), где y – переменная, которая в алфавитном порядке не предшествует ни одной переменной, свободно входящей в xA(x).

Формулировка данного правила предполагает наличие некоторого упорядочения всех переменных из алфавита языка классической логики предикатов.

Фактически речь идет о линейном порядке, заданном на множестве переменных языка.

У. Куайн показывает, что именно такой порядок гарантирует непротиворечивость и полноту предложенной им системы НВ.

Однако подход У. Куайна не является единственным. Например, В.А. Смирнов в системе NC предлагает следующую формулировку прямого правила удаления : из формулы xA(x) следует формула A(xA(x)), где xA(x) – это -терм, содержательно трактующийся как неопределенная дескрипция вида «некоторые x, обладающие свойством А» [Смирнов].

Поскольку -термы не являются термами классической логики предикатов, то система NC не эквивалентна системе NC (системе НВ с непрямым правилом удаления, предложенной В.А. Смирновым там же): все, что доказуемо в NC, доказуемо в NC, но обратное неверно.

Однако для NC можно доказать теорему Гильберта об устранении -термов:

если в NC можно из (возможно, пустого) множества посылок Г вывести А и Г, А не содержат -термы, то А следует из Г в NC [Смирнов, с. 228], [Мендельсон, с. 111-112].

В.А. Бочаров и В.И. Маркин предлагают вводить абсолютно ограниченные и относительно ограниченные переменных в выводе. Тогда правило удаления запишется следующим образом: из формулы xA(x, z1,…, zn) выводима формула A(y, z1,…, zn), при этом переменная y становится абсолютно ограниченной в выводе переменной, а все переменные z1,…, zn – относительно ограниченными в выводе переменными (z1,…, zn суть все свободные переменные из xA(x)).

При этом требуется, чтобы ни одна переменная не была абсолютно ограничена в выводе более одного раза и чтобы ни одна переменная не ограничивала сама себя (непосредственно, т.е. y не входит в z1,…, zn, или по транзитивности, т.е. если x ограничивает y и y ограничивает x, то x ограничивает x). Во второй главе нашей работы показывается, что такой подход гарантирует непротиворечивость этой системы НВ.

Мы подробно останавливаемся на системах НВ с прямым правилом удаления, поскольку система BMV (Bocharov, Markin, Voishvillo), алгоритм поиска вывода в которой является предметом нашей работы, – система НВ именно такого типа.

С другой стороны, мы останавливаемся подробно на работе с переменными в системах НВ с непрямым правилом удаления, т.к. существуют примеры систем НВ, не корректно работающие с переменными.

В англоязычной литературе известна серия публикаций 60-70-х гг. XX века в «The Journal of Symbolic Logic» по поводу системы НВ, предложенной И. Копи (I. Copi). И. Копи публиковал не являющиеся семантически непротиворечивыми системы НВ с прямым правилом удаления [Copi]. Семантическая противоречивость предлагаемых И. Копи систем НВ была установлена Д. Калишем (D. Kalish) [Kalish].

Не является семантически непротиворечивой система НВ, предложенная Е.К. Войшвилло [Войшвилло]. В этой системе доказывается, например, формула y(xA(x, x) zA(y, z)). Данная формула ложна, если в качестве А взять отношение равенства на множестве натуральных чисел.

§ 1.2. История создания систем автоматического поиска вывода В данном параграфе мы даем краткий обзор истории создания систем автоматического поиска вывода. Поскольку неотъемлемой частью создания таких систем является наличие программируемых электронно-вычислительных устройств, в начале данного параграфа приводятся некоторые факты из истории создания ЭВМ.

Отметим, что системы автоматического поиска натурального вывода в данном параграфе не рассматриваются. Такие системы будут подробно рассмотрены в следующем параграфе данной главы.

Пионером создания вычислительных логических машин (именно логических, т.е. работающих с текстами, а не с цифрами) считается средневековый мыслитель Р. Луллий.

Создавая такую машину, Р. Луллий опирался на средневековое представление о науке. Считалось, что во всякой области знания имеется небольшое число исходных понятий, с помощью которых выражаются бесспорные, самоочевидные положения, не нуждающиеся в обосновании. Из комбинаций исходных понятий и представлений возникает знание. В обладании этими комбинациями и тем, что из них вытекает, заключается подлинная мудрость. Таким образом, логическая машина должна была служить инструментом для порождения таких комбинаций.

Построенные Р. Луллием многочисленные модели такой машины не заменяли деятельность человека. Человек был необходим для интерпретации понятийных комбинаций и получения, таким образом, окончательного знания. Отметим, что в своих машинах Р. Луллию удалось реализовать одну из важнейших функций вычислительных машин – перебор вариантов.

В 1834 году Ч. Бэббидж сконструировал цифровое счетное устройство.

Особенностью этой машины была способность выполнять инструкции, считываемые с перфокарт. В 1842 году А. Лавлейс сделала описание работы аналитической машины Бэббиджа и составила первую программу для нее.

В дальнейшем стали создаваться машины, совершенствующие модель Бэббиджа. В 1855 году Дж. и Э. Шутц, базируясь на работах Ч. Бэббиджа, построили свою механическую вычислительную машину. В 1869 году У.С. Джевонс, используя результаты Дж. Буля, построил усовершенствованную модель этой машины. В году Г. Холлерит создал первую электромеханическую вычислительную машину и основал фирму, которая впоследствии превратилась в корпорацию IBM.

Промежуток времени между двумя мировыми войнами считается сегодня периодом рождения первого компьютера. В 1927 году в Массачусетском технологическом институте был изобретен аналоговый компьютер. В 1937 году Дж. Стибитц построил первую вычислительную машину на основе двоичной системы счисления.

В 1938-41 гг. К. Цузе предложил несколько моделей (Z1, Z2 и Z3) своей механической программируемой цифровой машины. Модель Z1 иногда называют первым в мире компьютером. В 1942 году в Университете штата Айова Дж. Атанасов и К. Берри создают первый в США электронный цифровой компьютер.

В России созданием «умных» машин занимались П.Д. Хрущов и А.Н. Щукарев.

Создание вычислительных машин активно велось в советское время.

Появление первого компьютера открыло путь для развития механизируемых исчислений. В 50-е годы XX века были созданы две компьютерные программы, которые заложили два основных направления в области автоматического поиска доказательства.

Первая программа была создана М. Дэвисом на ламповом компьютере "Johniac". Эта программа могла доказать, что сумма двух четных чисел является четным числом – первое в истории доказательство математического утверждения, генерированное компьютером.

Вторая программа, которая могла доказывать ряд предложений из "Principia Mathematica" Б. Рассела и А.Н. Уайтхеда, была создана А. Невелом, Дж. К. Шоу и Г. Саймоном. Эта программа ориентировалась на человеческий способ рассуждений, пытаясь симулировать общие эвристические подходы и психологические моменты мышления.

В 1956 году результаты этой работы были доложены на конференции в Дартмаунте, которую считают местом рождения нового раздела компьютеристики – исследований по искусственному интеллекту. На этой конференции разгорелась дискуссия: необходимо ли пытаться реализовывать на вычислительных машинах процедуры вывода, формулируемые математической логикой, или, следуя А. Невелу, Дж. К. Шоу и Г. Саймону, симулировать человеческие эвристики.

В 1961 году М. Минский подвел итог этой дискуссии: «Кажется ясно, что программа решения реальных математических проблем должна комбинировать математические рассуждения... с эвристическими рассуждениями Невела, Шоу и Саймона».

логикоориентированной программы фирмы IBM по автоматическому доказательству.

Это был большой шаг вперед: его программа могла доказывать около 350 предложений «Principia Mathematica» для чистого исчисления предикатов с равенством.

В 1954 году А. Робинсон предложил рассматривать точки, линии и окружности, которые нужно строить для решения геометрических проблем, как элементы так называемого Эрбрановского универсума и переходить при доказательстве геометрических утверждений к алгебраическим методам.

Одной из первых программ, реализовавших эту идею, была программа М. Дэвиса и Х. Патнем. Она состояла из двух частей: первая часть программы генерировала Эрбрановский универсум и делала соответствующие подстановки в формулы, вторая – оценивала эти формулы. Основная проблема, которая возникла перед авторами, заключалась в несистематичности подстановок.

В 1960 году эту проблему решил Д. Правиц посредством механизма, названного унификацией. Позже был предложен унифицирующий алгоритм.

Независимо от этого над доказательствами математических утверждений в национальной лаборатории Аргонны работали Д. Карсон, Дж. Робинсон и Л. Уос.

Ученые поставили перед собой задачу разработать такой принцип, в котором бы объединились различные методы в одно общее логическое правило.

В 1963-1965 гг. такое правило было найдено, и Дж. Робинсон публикует свою работу "A machine oriented logic, based on the resolution principle" [Robinson]. С тех пор метод резолюции прочно вошел в практически любую образовательную программу по логике и информатике.

Однако скоро стало ясно, что сам по себе метод резолюции не дает алгоритма поиска доказательства. Поэтому возникли два больших направления с соответствующими школами, которые проходят сквозь всю историю теории автоматического поиска доказательства.

В то время как первое направление, самое большое по числу представителей, продолжало отстаивать и совершенствовать метод резолюции, второе направление видело своей задачей имитировать эвристические методы применяемые «человеческими» математиками.

К первому лагерю принадлежали ученые национальной лаборатории Аргонны под руководством Л. Уоса и группа под руководством Б. Мелтцера в университете Эдинбурга. В 1965-75 гг. они предложили десятки усовершенствованных стратегий поиска вывода.

Другим предметом исследований этого направления было само правило резолюции. Вскоре оказалось, что оно не всегда является удобным, и были предложены другие правила вывода, например, гиперрезолюция. Исследовались также возможности представления метода резолюций в виде графоориентированной процедуры. Так, основная структура данных – множество дизъюнктов – пополнялась дополнительной информацией, например, представлением возможных шагов в виде графа.

Следующим результатом этого направления оказался матричный метод, который разрабатывался независимо друг от друга П. Андреусом в Карнеги-Меллон университете и В. Бибелем в университете Мюнхена. Если предыдущие методы еще сохраняли некоторую аналогию с человеческими рассуждениями в виде пошаговой выводимости, то матричная процедура отказывается от этой логической традиции и является полностью машинноориентированной. Поиск доказательства протекает в определенной структуре данных, так называемой матрице, и найденное доказательство не имеет ничего общего с обычным пониманием этой процедуры.

Представители второго лагеря критически относились к такой механизации дедуктивных систем, в особенности М. Минский из Массачусетского института технологий. Основной аргумент заключался в том, что единственного метода никогда не будет достаточно для того, чтобы описать и реализовать интеллект. Для этой цели нужно использовать много других компонент.

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

В 60-е годы XX века Л.М. Нортон предложил эвристический прувер для теории групп, а А. Невинс – алгоритм, разрабатываемый на базе «человекоориентированной логики». Результаты данных программ оказались не достижимыми для резолюционных процедур того времени. Здесь можно отметить работу исследователей университета Техаса, развивавших специализированные методы доказательства для конкретных областей математики.

На сегодняшний день наиболее эффективными остаются пока системы автоматического поиска доказательства, основанные на единообразном методе резолюций. Их эффективность подкрепляется темпами развития электронной техники.

И если вначале относительно сложные теоремы доказывались исключительно специальными процедурами, то в дальнейшем становилось возможным получать их доказательство посредством единой резолюционной системы.

Наиболее результативными в этой области являются группы, работающие в национальной лаборатории Аргонны, Остине, Карлсруе и Кайзерслаутерна. Однако в последнее время наметилась тенденция синтеза различных методов в единой программной оболочке, что позволяет сгладить недостатки отдельных методов. Такую стратегию приняли разработчики наиболее успешной системы OTTER (лаборатория Аргонны).

Системы автоматического поиска доказательства долгое время считались эзотерической областью знания. Однако в последнее время появился ряд сфер применения результатов, достигнутых в этой области: развитие программного и аппаратного обеспечения; становление дедуктивных баз данных.

Другими областями, диктующими необходимость совершенствования методов автоматического доказательства, являются компьютерная алгебра, а также некоторые аспекты тестирования программ. В этот ряд можно включить экспертные системы, робототехнику и другие направления.

Системы доказательства теорем разбиваются на два больших лагеря. Первый лагерь – это системы интерактивного доказательства теорем (proof checker), другое название этих систем – редакторы доказательств.

Это системы, которые под своим контролем дают возможность пользователю строить доказательство. Они в большинстве своем основываются на теории типов (часто с зависимыми типами) и на системах правил заключения. При этом правила вывода обычно охватывают систему натурального вывода типа Генцена и зависят от желаемого поля применения. Шаги доказательства проверяются системой на применимость и корректность. Таким образом достигается уверенность, что в системе могут быть построены только корректные доказательства.

Примером редактора доказательств является система AUTOMATH, которая создана для проверки математических доказательств. В этой системе доказывается значительная часть теорем из чистой математики. Однако запись доказательств в AUTOMATH, как правило, в 10-20 раз длиннее, чем в естественном языке.

разработанную А.В. Смирновым при участии А.Е. Новодворского [Смирнов-мл]. Эта программа позволяет работать не только с одной стандартной логической системой, но и делать выбор из довольно широкого списка известных систем. Программа предоставляет также пользователю возможность описать некоторую собственную систему, после чего она автоматически начинает ее поддерживать.

Построение интерактивного доказательства можно сократить, если объединить многие шаги в так называемые тактики. Для этого предлагаются языки программирования, с помощью которых создаются редакторы доказательств. Такие системы были названы тактическими редакторами доказательств (например, система NuPRL). Высказывается предположение, что с развитием более сильных тактик возможно достижение высокого уровня автоматизации.

Ко второму лагерю относятся автоматические генераторы доказательств (automated prover). В отличие от редакторов доказательств, в которых пользователь сам строит доказательство, роль пользователя в автоматических генераторах доказательств сводится к постановке задания системе – доказать теорему. Далее система работает до тех пор, пока не найдено доказательство или не выполнится критерий, обрывающий работу системы. В качестве такого критерия стараются привести построение контрмодели для доказываемого утверждения.

Разработки программ в области автоматической дедукции проводятся в целом ряде крупных мировых научно-исследовательских центров. В национальной лаборатории Аргонны создана программа OTTER, основанная на теории резолюций.

OTTER является последним продуктом в цепи систем (AURA, ITP), которые были созданы под руководством Л. Уoca. Программа создана для поиска доказательств для классической логики предикатов первого порядка с равенством, написана на языке С, занимает примерно 180 Кб и способна оперировать большим количеством дизъюнктов (миллиардами), что показывает ее высокую эффективность.

В Кембридже создана программа автоматической дедукции Isabelle. В КарнегиМеллон университете создана программа для автоматического доказательства теорем для логики высоких порядков. В лаборатории KAKEHI и Университете WASEDA создана программа автоматического доказательства для секвенциального исчисления В отечественной науке подобные программы начали создаваться также достаточно давно. В 60-е годы XX века под руководством Шанина Н.А. разработан алгоритм машинного поиска логического вывода [Шанин и др.]. Программа, реализованная по этому алгоритму, ищет вывод в классическом секвенциальном исчислении высказываний и перерабатывает его далее в натуральный вид.

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

Надо отметить, что концентрация внимания исследователей в области автоматического вывода на этих популярных дедуктивных методах не случайна и обусловлена, в первую очередь, практическими соображениями. Так, например, исследования в области теории резолюций тесно связаны с языками логического программирования (в частности, типа Пролог), где выводы основаны на методе резолюций, который изначально являлся составной частью Пролога [Братко].

Еще одной причиной такой ситуации является факт достаточно успешного практического применения неклассических логик в рамках различных проектов тестирования аппаратных средств [Bochmann], нередко спонсирующихся ведущими производителями таких средств (например, Intel).

На сегодняшний день самым распространенным и эффективным методом в данной области является метод тестирования моделей. В данном методе для описания моделей аппаратных средств используется дедуктивный аппарат, чаще всего основанный на модальной или временной логике, семантика для которых чаще всего строится в форме аналитических таблиц [Bochmann], [Bolotov & Fisher].

§ 1.3. Автоматический поиск вывода в натуральном исчислении В данном параграфе мы анализируем алгоритмы поиска натурального вывода, выявляем сильные и слабые стороны данных программ.

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

Анализ работ будет зафиксирован в следующей таблице, в верхней строке которой будут перечислены следующие алгоритмы поиска натурального вывода в классической первопорядковой логике:

1) программа THINKER, разработанная Д. Пеллетье (J. Pelletier) [Pelletier];

2) программа OSCAR, разработанная Дж. Поллоком (J. Pollock) [Pollock];

3) программа ANDP (Automated Natural Deduction Prover), разработанная 4) программа CMU PT (Carnegie Mellon University Proof Tutor), разработанная У. Сигом (W. Sieg), Р. Шейнсом (R. Scheines) и Дж. Бернсом (J. Byrnes) [Sieg], [Sieg & Byrnes], [Byrnes];

(F. Portoraro) [Portoraro];

6) программа Prover, разработанная В.А. Бочаровым, А.Е. Болотовым и А.Е. Горчаковым и модифицированная В.О. Шангиным [Болотов и др.], [Болотов и др.1], [Шангин], [Bocharov et al].

В первом столбце таблицы находятся те самые признаки, по отсутствию или наличию которых мы анализируем данные алгоритмы поиска вывода:

1) алгоритм работает с предикатом равенства;

2) алгоритм работает с эквиваленцией;

3) алгоритм работает с неклассическими логиками;

4) множество используемых алгоритмом переменных ограничено;

(непротиворечивость, полнота и т.д.);

6) алгоритм использует сколемовские термы;

7) алгоритм имеет программную реализацию.

Значениями данной таблицы будут символы: + (признак имеется), – (признак отсутствует) и +– (требует доработки).

Из перечисленных программ только Thinker работает с предикатом равенства.

Соответственно, среди предложенных программ только Thinker может построить вывод для всех 75 проблем, предложенных в [Pelletier2], [Pelletier3]. Данный факт неудивителен, поскольку у Thinker и у списка 75 тестовых задач для алгоритма поиска вывода один и тот же автор – Д. Пеллетье.

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

Безусловным преимуществом алгоритма является возможность работы не только в классической, но и в неклассических логиках. Программа Thinker умеет работать в модальной логике [Pelletier]; программа Oscar – в логике «отменяемых»

(defeasible) рассуждений; программа ANDP – в интуиционистской логике, и, наконец, можно рассматривать работы [Макаров], [Шангин1], [Шангин3] о поиске вывода в интуиционистскую логику.

Только программа Thinker допускает ограничение (по умолчанию – 20) на количество переменных, которое можно использовать при построении вывода. По желанию пользователя, это количество может меняться. Однако наличие данного ограничения принципиально для поиска вывода. Если множество таких переменных исчерпано (т.е. все n переменных использованы в выводе), то поиск вывода прекращается.

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

Строка «Свойства» отмечает разработанность метатеоретических проблем для данных алгоритмов. Например, «+–» столбце для Oscar и ANDP означает: доказано, что данные алгоритмы семантически непротиворечивы, т.е. все, что доказуемо, является логически общезначимым; и не доказано, что данные алгоритмы семантически полны, т.е. с помощью данных алгоритмов можно доказать все логически общезначимые формулы. Дж. Поллок, автор Oscar, предполагает, что его программа полна в указанном смысле, однако доказательства этого факта пока нет.

По разным причинам, метатеоретическая проблематика отсутствует для программ Thinker и Symlog. По словам Ф. Портораро, автора программы Symlog, «мы считаем вопрос о полноте алгоритма второстепенным: во-первых, он слишком далеко отстоит от темы нашего исследования; во-вторых, он не отвечает задачам алгоритма.

Задача нашего алгоритма – предоставлять всестороннюю помощь при построении вывода, а не болезненно строить формальные выводы определенного вида. Поэтому вопрос о полноте нашего алгоритма отходит на второй план и вовсе исчезает тогда, когда алгоритм начинает оказывать помощь при работе с другими формальными системами, например, с арифметикой или теорией множеств» [Portoraro, с. 59].

Мы не можем согласиться с таким подходом, поскольку предоставлять действительно всестороннюю помощь при построении вывода может только алгоритм, для которого доказана теорема о семантической полноте.

Что касается Thinker, то данный алгоритм неполон, если учесть вышеуказанное ограничение на количество используемых в выводе переменных: «Очень трудно оценить семантическую полноту программы Thinker потому, что он может прийти к пункту J (остановка алгоритма) в различных случаях; в том числе и тогда, когда формула является логически общезначимой, Thinker может остановиться, потому что кончатся переменные» [Pelletier, с. 33]. С другой стороны, он пишет, что неясен ответ на вопрос, будет ли Thinker семантически полон, если данное ограничение на количество переменных будет снято.

Теорема о семантической полноте доказана для CMU PT. Предложенный У. Сигом метод (см. также [Sieg], [Sieg & Byrnes], [Byrnes]) заключается в том, что по дереву вывода, которое не является доказательством, можно построить контрмодель для данной формулы или для данной выводимости. Т.е. если формула не доказуема, то найдется (возможно, бесконечный) контрпример, показывающий, что при данных значениях исходная формула принимает значение «ложь». Сходным образом доказана семантическая полнота для Prover. О различиях в указанных подходах подробно говорится в конце данного параграфа.

сколемизацией здесь имеется ввиду явная сколемизация, т.е. добавление в язык логики предикатов особых свободных переменных и предметных функторов, с помощью которых образуется сколемовский терм. Сколемизация осуществляется в Oscar, CMU PT и Symlog.

Однако поиск вывод не обязательно предполагает явную сколемизацию.

Существуют различные формы неявной сколемизации. Например, Thinker предполагает в процессе поиска вывода использовать т.н. «шаблоны» (templates), которые при окончательном построении вывода превращаются в формулы. Например, снятие с формулы xA(x, y) порождает шаблон A(@, y). Prover также использует неявную сколемизацию, о чем подробно говорится далее.

Все алгоритмы имеют программные реализации, доступные в сети Интернет.

Имеется пропозициональный фрагмент программной реализации Prover. Что касается кванторного фрагмента Prover, то он находится в стадии разработки.

Из данного анализа заметно, что проблема исследований метатеоретических свойств алгоритмов поиска натурального вывода или вообще не ставится, или не решается. Фундаментальными в этом отношении являются работы У. Сига. Именно на них во многом базируется наше исследование.

Однако здесь мы отметим те существенные различия, которые лежат между подходом У. Сига и нашим подходом.

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

Во-вторых, в диссертационном исследовании поиск вывода осуществляется непосредственно в системе НВ, а предложенный У. Сигом алгоритм CMU PT использует для поиска вывода промежуточные, вставочные исчисления (intercalation calculi). По внешнему виду такие исчисления напоминают секвенциальные исчисления.

Вывод в таких исчислениях затем перестраивается в натуральный вывод.

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

Что касается Prover, то программа строит натуральный вывод именно в системе натурального вывода. Таким образом, наша работа заполняет своеобразную лакуну, которая образовалась в области автоматического поиска НВ.

Глава 2. Анализ системы натурального вывода BMV § 2.1. Формулировка системы BMV Задается алфавит языка L классической логики предикатов:

1. х, у, z, x1, y1, z1, x2,... – бесконечный список индивидных переменных, 2. a, b, c, a1, b1, c1, a2,... – бесконечный список индивидных констант, 3. f, g, h, f1, g1, h1, f2,... – бесконечный список предметно-функциональных констант (функторов) различной местности, 4. Р, Q, R, P1, Q1, R1, P2,... – бесконечный список предикаторных констант (предикаторов) различной местности, &,,, ¬,, – логические символы, 6. (, ),, – технические символы.

В дальнейшем буквы,,, 1, 1, 1, 2,… обозначают произвольные индивидные переменные, буквы Ф, Ф1, Ф2,… обозначают произвольные функторы и буквами П, П1, П2,… обозначаются произвольные предикаторы.

Определение 2.1.1. Термом является объект, обладающий следующими свойствами:

1. Произвольная индивидная переменная есть терм, 2. Произвольная индивидная константа есть терм, 3. Если Ф – n-местный функтор, а t1, t2,..., tn – термы, то выражение Ф(t1, t2,..., tn) – 4. Ничто иное не является термом.

Определение 2.1.2. Формулой является объект, обладающий следующими свойствами:

1. Если П – n-местный предикатор, а t1, t2,..., tn – термы, то выражение П(t1, t2,..., tn) Если А – формула, то ¬А – формула, Если А – формула и – индивидная переменная, то А и А – формулы, 5. Ничто иное не является формулой.

Формулы, определяемые пунктом 1, называются элементарными формулами.

Все остальные формулы называются сложными формулами. Буквами А, В, С,… (с индексами и без них) обозначаются произвольные формулы.

формулировки правил исчисления.

В выражениях А и А формула А называется областью действия кванторов и, взятых по индивидной переменной.

Вхождение индивидной переменной называется связанным, если расположена непосредственно справа от квантора или находится в области действия квантора, взятого по. Остальные вхождения называются свободными. Индивидная переменная является свободной (связанной) в формуле А, если она имеет хотя бы одно свободное (связанное) вхождение в формуле А.

Вхождение квантора в выражениях А и А называется вырожденным, если ни одно вхождение переменной не находится в А. Например, вхождение в формулу xyP(y) вырождено. Если некоторое вхождение переменной в А связано двумя или более вхождениями кванторов по, то все эти вхождения кванторов по, кроме самого правого, являются вырожденными [Непейвода, с. 184]. Например, вхождение в формулу xхP(х) вырождено.

Пусть t – терм, – индивидная переменная. Тогда выражение вида А(/t) обозначает результат подстановки в формулу А() вместо всех свободных вхождений терма t. Подстановка A(/t) считается правильной, если никакое свободное вхождение не лежит в области действия никакого квантора по каждой переменной, входящей в терм t.

обозначающее правильную подстановку в А переменной вместо переменной. При этом фиксируется множество всех свободных переменных 1,…, n в А и {1,…, n}.

Данное выражение обозначается как A(/, 1,…, n).

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

Задаются следующие правила системы BMV (BMV-правила):

В правилах в и ¬в формула С является последней неисключенной посылкой (это понятие будет разъяснено ниже). А(/t) и A(/) – результаты правильной подстановки.

В правилах в и и запись « – абс.; 1,…, n – огр.» означает, что абсолютно ограничена в выводе и переменная относительно ограничивает в выводе каждую переменную из множества 1,…, n, где {1,…, n} – это множество всех свободных переменных, входящих в посылки данных правил.

В дальнейшем мы иногда вместо « относительно ограничена в выводе» будем писать « ограничена», не указывая на ту переменную, которая относительно ограничивает, а вместо « абсолютно ограничена в выводе» – « абсолютна».

Переменные, не ограниченные абсолютно в выводе, будут называться неабсолютными.

«относительно ограниченная переменная» см. [Бочаров и Маркин, с. 133-134].

Определение 2.1.3. Выводом в системе BMV (ВМV-выводом) называется непустая конечная последовательность формул С1, C2,…, Cn (n 1), удовлетворяющая следующим условиям:

1. каждая формула есть либо посылка, либо получена из предыдущих по одному из BMV-правил;

при применении правил в и ¬в все формулы, начиная с последней неисключенной посылки Сi (1 i n) и вплоть до результата применения данного правила Ci Cj (1 j n) или ¬Сi, исключаются из дальнейших шагов вывода в том смысле, что к ним запрещено применять правила вывода;

3. ни одна индивидная переменная в выводе не ограничивается абсолютно более одного раза; 4. ни одна переменная не ограничивает в выводе сама себя.

Выводом формулы В из непустого множества посылок Г называется BMVвывод, в котором множество неисключенных посылок есть Г и последняя формула есть формула В.

Доказательством формулы В называется BMV-вывод формулы В из пустого множества неисключенных посылок.

Теоремой называется формула, для которой имеется доказательство.

Определение 2.1.4. Завершенным ВМV-выводом называется ВМV-вывод, в котором никакая переменная, абсолютно ограниченная в выводе, не встречается свободно ни в неисключенных посылках, ни в заключении. Завершенное доказательство есть завершенный ВМV-вывод из пустого множества неисключенных посылок.

Проанализируем правила системы.

Правила для конъюнкции, а также правило введения дизъюнкции, обычны для систем натурального вывода: их можно обнаружить в [Генцен].

Что касается правила для исключения дизъюнкции, то иногда его формулируют в виде правила разбора случаев (р.с.): из A B, A C, B C следует C. Известно, что р.с. сильнее, чем и в том смысле, что, например, в интуиционистской логике можно показать с помощью р.с. производность и, но невозможно показать с помощью и производность р.с.. Однако существуют определенные трудности с построением процедуры поиска натурального вывода типа Куайна с правилом р.с. [Макаров].

Что касается правила введения импликации, то специфика этого правила в том, что формула С является последней неисключенной посылкой. Данное требование необходимо для корректности системы. При применении этого правила выводима формула С В и из вывода исключаются все формулы, начиная с формулы С и заканчивая формулой, непосредственно предшествующей формуле С В. Формула исключается из вывода не в том смысле, что она стирается и удаляется, а в том смысле, что к данной формуле не может быть применено ни одно правило вывода.

Наличие правила и – чуть ли не обязательное свойство всех систем натурального вывода.

Правило ¬и (снятие двойного отрицания) стандартно.

Что касается правила введения отрицания, то иногда используют два правила:

из В, ¬В следует и из следует С, где – знак противоречия (тождественно ложной формулы) и С – произвольная формула. В нашей системе формула С не произвольна:

она является последней неисключенной посылкой, что, опять же, обусловлено требованием корректности системы. Применение этого правила также влечет исключение из вывода всех формул, начиная с формулы С и заканчивая формулой, непосредственно предшествующей формуле ¬С.

Кванторные правила исключения квантора общности и введения квантора существования обычны. Специфика нашей системы – в формулировке правила введения квантора общности и правила исключения квантора существования.

Пусть yP(y) – формула, причем P – одноместный предикатор. Можно, например, не нарушая требования правильной подстановки, получить из yP(y) по и формулу P(x), затем применить в и получить yP(y). Из yP(y) с помощью правил и, в можно снова получить yP(y) и т.д.

Отметим, что в системе BMV такие бесконечные преобразования формул ограничиваются понятием вывода. Однако нам важен тот факт, что такие Иногда пишут «не может абсолютно ограничиваться дважды». При этом Е.К. Войшвилло отмечал, что данное требование можно нарушить без ущерба для корректности, «когда правило в или и вторично применяется для вывода из той же формулы» [Войшвилло, с. 90-91].

преобразования возможны, если не следовать понятию вывода, а следовать только формулировкам в, и и требованию правильной подстановки.

Иногда формулировки данных правил не позволяют такие взаимопревращения формул [Войшвилло]. Более того, Дж. Пеллетье вообще не формулирует правила введения квантора общности явным образом. Аналог этого правила имплицитно содержится в формулировке достижимости некоторого подвывода [Pelletier].

Необходимость учета абсолютных и ограниченных переменных обусловлена, как мы далее увидим, требованием, чтобы ни одна переменная не ограничивала в выводе сама себя.

У. Куайн, например, явно указывает на наличие абсолютно ограниченных (flagged) переменных и не указывает явно на наличие относительно ограниченных переменных. Однако он задает свободные переменные в алфавитном порядке и требует, чтобы при применении правил и, в новая свободная переменная не предшествовала в алфавитном порядке имеющимся в формуле свободным переменным [Quine]. Именно таким образом У. Куайн избегает самоограничения переменной.

симметричность: каждой логической связке соответствуют хотя бы одно правило исключения и хотя бы одно правило введения. Свойство симметричности правил натурального вывода идет от работ Г. Генцена [Генцен]. См. также [Fitch]. В то же время симметричность правил не является необходимым свойством натурального вывода. Можно указать на системы натурального вывода, где данное свойство не выполняется [Pelletier].

Проанализируем понятие вывода в системе.

Требование, чтобы в правилах в, ¬в формула С была последней неисключенной посылкой, обосновывается следующим образом:

В данном выводе мы от вывода формулы С из посылок A, B по правилу в перешли к доказательству формулы A C. Однако такой переход семантически неверен, т.е. из A, B |= C не следует |= A C.

Аналогично обосновывается данное требование в формулировке правила ¬в.

Обоснование требования не ограничивать абсолютно некоторую переменную более одного раза, а также требований наличия завершенного вывода, можно найти в [Quine, стр. 97-99].

Что касается запрета на самоограничение переменной, которого нет в [Quine], то он обосновывается, например, невозможностью построения завершенного вывода xyA(x, y) из yxA(x, y) [Бочаров и Маркин, с. 136].

Необходимость введения понятия завершенного вывода (доказательства), наряду с понятием вывода (доказательства), является характерным свойством выводов в первопорядковых натуральных исчислениях типа Куайна, где в общем случае заключение не следует из своих посылок: «При незавершенности вывода не обеспечена истинность заключения при истинности посылок» [Войшвилло, с. 94].

Натуральные исчисления типа Куайна [Quine], [Войшвилло], [Бочаров и Маркин], [Ивлев] противопоставляются натуральным исчислениям типа Генцена [Генцен], [Fitch], [Li], не требующим введения понятия завершенного вывода.

В качестве примеров приведем завершенный BMV-вывод ¬xP(x) |– x¬P(x).

Помещаем формулу ¬xP(x) в качестве посылки. Берем другую посылку P(x).

Применяя к этой формуле правило в, выводим формулу xP(x). Поскольку формула ¬xP(x) (шаг 1) противоречит формуле xP(x) (шаг 3), на шаге 4 выводим формулу ¬P(x), применяя правило ¬в. Формула ¬P(x) является отрицанием последней неисключенной посылки P(x). При этом все формулы, начиная с формулы P(x) и заканчивая формулой xP(x), исключаются из дальнейших шагов вывода. Применяя к формуле ¬P(x) правило в, выводим формулу x¬P(x). При этом переменная х является абсолютно ограниченной в выводе.

Данная последовательность формул является завершенным выводом формулы x¬P(x) из посылки ¬xP(x), поскольку она является выводом формулы x¬P(x) из посылки ¬xP(x) и абсолютно ограниченная переменная х не входит свободно ни в x¬P(x), ни в ¬xP(x).

§ 2.2. Семантическая непротиворечивость системы BMV Определение 2.2.1. Переменная называется активной (пассивной) в BMVвыводе, если абсолютно ограничена в этом выводе и (не) существует абсолютно ограниченная в этом выводе переменная, которую относительно ограничивает переменная.

При применении правила в к формуле А(/, 1,…, n) выводится формула А(), переменная становится абсолютно ограниченной и относительно ограничивает все переменные из 1,…, n.

При применении правила и к формуле А() выводится формула А(/, 1,…, n), переменная становится абсолютно ограниченной и относительно ограничивает все переменные из 1,…, n.

Построим следующий завершенный вывод xyA(x, y) |– xzA(x, z).

В этом выводе переменная x пассивна и переменная y активна, поскольку абсолютно ограниченная переменная y относительно ограничивает другую абсолютно ограниченную переменную x на шаге 4.

Лемма 2.2.2. В произвольном BMV-выводе D с непустым множеством М всех абсолютно ограниченных переменных в D найдется переменная : М и не ограничивает относительно в D ни одну переменную из М. Доказательство: от противного.

Допустим, что в D каждая переменная из М ограничивает относительно некоторую переменную из М.

Техникой доказательства этой леммы мы обязаны В.М. Попову.

Для всякой переменной, пусть [] – это множество всех переменных из М, каждую из которых ограничивает относительно в D, и пусть для всякого непустого множества X переменных (X)min есть переменная из X, которая нестрого предшествует в алфавитном порядке переменных любой переменной из X.

Поскольку произвольный BMV-вывод конечен (определение 2.1.3), найдется такое натуральное число n: М есть n-элементное множество. Пусть для определенности n0 есть натуральное число и М есть n0-элементное множество.

Рассмотрим последовательность множеств М1, М2, …, Мn0, Mn0+1, определяемую следующим образом: М1 = [(M)min], Mk+1 = [(Mk)min], 1 < k n0.

Легко видеть, что все множества М1, М2, …, Мn0, Mn0+1 непусты, а (M1)min, (M2)min, …, (Mn0)min, (Mn0+1)min – это переменные, принадлежащие множеству М.

Ясно, что для любого i и для любого j, 1 i < j n0 +1, переменная (Мni)min ограничивает относительно в D переменную (Мnj)min.

Отсюда из антирефлексивности и транзитивности отношения «переменная … ограничивает относительно в D переменную …» получаем, что (M1)min, (M2)min, …, (Mn0)min, (Mn0+1)min попарно различны. Но все они принадлежат множеству М. Следовательно, множеству М принадлежит не менее n0+1 элементов, что противоречит тому, что М есть n0элементное множество.

Значит, допущение неверно, и в произвольном BMV-выводе D некоторая переменная из непустого множества М абсолютно ограниченных переменных в D не ограничивает относительно ни одну переменную из М.

Лемма 2.2.2 доказана для произвольного BMV-вывода. Поскольку всякий завершенный BMV-вывод есть BMV-вывод, лемма 2.2.2 верна для произвольного завершенного BMV-вывода с непустым множеством абсолютных переменных.

По определению вывода в системе BMV, вывод – это непустая конечная последовательность формул, каждая из которых является либо посылкой, либо получена из предыдущих формул по одному из правил вывода системы BMV.

Подробный логический анализ данного отношения проводится в параграфе 3.1 нашего исследования.

Таким образом, важным параметром любого завершенного вывода является число применений в нем правил вывода. Будем обозначать это число посредством q. Из определения вывода следует, что q 0.

Специфическим свойством вывода в данном исчислении является наличие в выводе (возможно, пустого) множества абсолютно ограниченных переменных. Будем называть рангом вывода число абсолютно ограниченных переменных данного вывода и обозначать ранг вывода посредством r. Из определения вывода следует, что r 0.

Пусть Г – произвольное непустое множество формул языка логики предикатов, тогда из Г логически следует формула В (обозначается записью «Г |= В»), если и только если не существует модели и приписывания значений предметным переменным, при которых каждая формула из Г принимает значение «истина», а формула В – значение «ложь».

Лемма 2.2.3. В произвольном завершенном выводе, число применений правил вывода в котором есть q и ранг которого есть r, последняя формула этого вывода семантически следует из множества всех неисключенных в этом выводе посылок.

Доказательство.

Данная лемма будет доказана методом двойной математической индукции по числу применений правил вывода и по рангу произвольного завершенного вывода. В обосновании данного метода мы следуем [Смирнов, с. 122-123].

Запишем сокращенно данную лемму в виде qrЛ(q, r).

Для доказательства этой леммы достаточно доказать три утверждения:

Принцип полной математической индукции имеет вид Пусть A(n) равняется rЛ(n, r), тогда Пусть A(r) равняется Л(n, r), тогда покажем, что из (А), (Б), (С), (I) и (II) следует qrЛ(q, r).

8. {Л(n+1, 0) & r[r1(r1 r Л(n+1, r1)) Л(n+1, r+1)]} rЛ(n+1, r) (II), n = n+ 11. m(m n rЛ(m, r)) rЛ(n+1, r) 13. {rЛ(0, r)& n[m(m n rЛ(m, r)) rЛ(n+1, r)]} qrЛ(q, r) (I) Поэтому доказательство леммы сводится к доказательству утверждений (А), (Б) и (С).

(А) Л(0, 0): лемма верна для всех завершенных выводов, ранг и число применений правил вывода в которых равны 0.

Пусть последовательность формул С1, C2,…, Сt (t 1) есть завершенный вывод, ранг и число применений правил вывода в котором равны 0. Для доказательства Л(0, 0) достаточно показать, что формула Сt семантически следует из множества всех неисключенных посылок в выводе С1, C2,…, Сt.

По определению семантического следования, получаем, что {С1, C2,…, Сt} |= Сt. Но множество {С1, C2,…, Сt} есть множество всех неисключенных посылок в выводе С1, C2,…, Сt. Поэтому Сt семантически следует из множества всех неисключенных посылок в выводе С1, C2,…, Сt.

(Б) лемма верна для всех завершенных выводов, ранг которых равен 0 и число применений правил вывода в которых равно n+1, в предположении, что лемма верна для всех завершенных выводов любого ранга, число применений правил вывода в которых меньше или равно n.

Ранг вывода равен 0, значит, в выводе не применялись правила в, и.

Таким образом, (Б) распадается на 10 случаев по количеству BMV-правил (все BMV-правила, кроме в, и).

Последняя формула завершенного вывода получена по правилу &и.

Тогда вывод имеет следующий вид: С1, C2,…, Cj,…, Сt, где t > 0, t > j, Сj есть A & Ct и Сt есть В.

Вывод С1, C2,…, Cj является завершенным, т.к. в выводе С1, C2,…, Cj,…, Сt не применялись правила в, и.

По индуктивному предположению, Г1 |= Cj, где Г1 (Г1 Г) – множество неисключенных посылок из С1, C2,…, Cj и Г – множество неисключенных посылок из С1, C2,…, Cj,…, Сt. Значит, Г1 |= A & B.

Учитывая Г1 |= A & B и A & B |= B, получаем Г1 |= B. Отсюда, используя Г Г, получаем Г |= B.

Подслучай, когда Сj есть Ct & А, рассматривается симметрично.

Аналогичным образом рассматриваются еще 4 случая однопосылочных правил: в, ¬и, и и в.

Последняя формула завершенного вывода получена по правилу &в.

Тогда вывод имеет следующий вид: С1, C2,…, Cj,…, Сi,…, Сt, где t > 1, t > j, t > i, Сj есть A, Ci есть В и Сt есть А & В.

Вывод С1, C2,…, Cj является завершенным, т.к. в выводе С1, C2,…, Cj,…, Сi,…, Сt не применялись правила в, и.

Вывод С1, C2,…, Ci является завершенным, т.к. в выводе С1, C2,…, Cj,…, Сi,…, Сt не применялись правила в, и.

По индуктивному предположению, Г1 |= Cj, где Г1 (Г1 Г) – множество неисключенных посылок из С1, C2,…, Cj и Г – множество неисключенных посылок из С1, C2,…, Cj,…, Сi,…, Сt. Значит, Г1 |= A.

По индуктивному предположению, Г2 |= Ci, где Г2 (Г2 Г) – множество неисключенных посылок из С1, C2,…, Ci и Г – множество неисключенных посылок из С1, C2,…, Cj,…, Сi,…, Сt. Значит, Г2 |= B.

Аналогичным образом рассматриваются еще 2 случая однопосылочных правил: и и и.

Последняя формула завершенного вывода получена по правилу ¬в.

Тогда вывод имеет следующий вид: С1, C2,…, Сh,…, Cj,…, Сi,…, Сt, где t > 2, t > j, t > i, t > h, Сj есть D, Ci есть ¬D и Сt есть ¬Ch, где Ch есть последняя неисключенная посылка в выводе.

Вывод С1, C2,…, Cj является завершенным, т.к. в С1, C2,…, Сh,…, Cj,…, Сi,…, Сt не применялись правила в, и.

Вывод С1, C2,…, Ci является завершенным, т.к. в С1, C2,…, Сh,…, Cj,…, Сi,…, Сt не применялись правила в, и.

По индуктивному предположению, Г1 |= Cj, где Г1 (Г1 Г) – множество неисключенных посылок из С1, C2,…, Cj и Г – множество неисключенных посылок из С1, C2,…, Сh,…, Cj,…, Сi,…, Сt. Значит, Г1 |= D. Отсюда Г1, Сh |= D.

По индуктивному предположению, Г2 |= Ci, где Г2 (Г2 Г) – множество неисключенных посылок из С1, C2,…, Ci и Г – множество неисключенных посылок из С1, C2,…, Сh,…, Cj,…, Сi,…, Сt. Значит, Г2 |= ¬D. Отсюда Г2, Сh |= ¬D.

Учитывая Г1, Сh |= D и Г2, Сh |= ¬D, получаем Г1, Г2 |= ¬Сh. Отсюда, используя Г1 Г и Г2 Г, получаем Г |= Сt.

Последняя формула завершенного вывода получена по правилу в.

Тогда вывод имеет следующий вид: С1, C2,…, Ch,…, Cj,…, Сt, где t > 2, t > h, t > j, Сt есть Ch Cj, где Ch есть последняя неисключенная посылка в выводе.

Вывод С1, C2,…, Cj является завершенным, т.к. в выводе С1, C2,…, Cj,…, Сt не применялись правила в, и.

По индуктивному предположению, Г1 |= Cj, где Г1 (Г1 Г) – множество неисключенных посылок из С1, C2,…, Cj и Г – множество неисключенных посылок из С1, C2,…, Cj,…, Сt. Значит, Г1 |= Сj. Отсюда Г1, Ch |= Сj.

Из Г1, Ch |= Сj получаем Г1 |= Ch Cj. Отсюда, используя Г1 Г, получаем Г |= Ch Cj.

Таким образом, имеет место m(m n rЛ(m, r)) Л(n+1, 0).

(С) лемма верна для всех завершенных выводов, ранг которых равен r+1 и число применений правил вывода в которых равно n, в предположении, что лемма верна для всех завершенных выводов, ранг которых меньше или равен r и число применений правил вывода в которых равно n.

Т.е. докажем rЛ(n, r+1) в предположении, что r1(r1 r Л(n, r1)).

Пусть имеется завершенный вывод Д с n+1 количеством абсолютно ограниченных переменных и {1, 2, …, n+1} – множество (n 1) абсолютно ограниченных переменных в этом выводе.

По лемме 2.2.2, среди {1, 2, …, n+1} найдется пассивная переменная i, 1 i n+1. Если в Д несколько пассивных переменных, то мы выбираем первую (сверху вниз) из них.

С1. Пассивная переменная i абсолютно ограничена по правилу в.

С2. Пассивная переменная i абсолютно ограничена по правилу и.

h. C(i) Построим следующий вывод Д*, который будет отличаться от предыдущего только наличием посылки 0 вида К М, где К – формула, находящаяся на шаге h в выводе Д, и М – формула, находящаяся на шаге k в выводе Д.

h. C(i) В Д* i не является абсолютно ограниченной переменной, т.к. формула C() или C(i), которая находится на шаге k, получена по правилу и.

Д* является завершенным, т.к.

• ни одна переменная из {1, 2, …, n+1} не входит свободно ни в Г, ни в формулу В (поскольку Д – это завершенный вывод);

• из {1, 2, …, n+1} только i входит свободно в посылку, находящуюся на шаге 0 (поскольку i пассивна).

Поскольку Д* завершен, в Д* n абсолютно ограниченных переменных (i не является абсолютно ограниченной переменной в Д*) и число применений правил вывода в Д* равно числу применений правил вывода в Д, по индуктивному предположению, 0, Г |= В, т.е. C(i) C(), Г |= В или C() C(i), Г |= В.

Из Г, C(i) C() |= В следует, что Г, i(C(i) C()) |= В, или Согласно формулировке правил в, и, переменная i не входит свободно ни в C(), ни в C(), значит, |= i(C(i) C()) или |= i(C() C(i)).

Таким образом, имеет место r1(r1 r Л(n, r1)) Л(n, r+1).

Теорема 2.2.4. Система BMV семантически непротиворечива.

Доказательство. Следует из леммы 2.2.3.

Глава 3. Алгоритм поиска вывода в системе BMV § 3.1. Изменение формулировки системы BMV В целях эффективности автоматического поиска вывода добавим к BMVправилам следующие правила исключения логических связок:

Несложно показать, что данные правила производны: их добавление не влияет на множество теорем исчисления.

Теперь объясним необходимость введения именно таких правил.

Отсутствие этих правил приводит к следующим затруднениям [Болотов и др.].

Пусть (ситуация «а») в алгоритме необходимо доказать формулу А В, но в выводе нет ни А, ни В.

Тогда (ситуация «б») в качестве последней посылки в последовательность вывода помещается ¬(А В) и теперь необходимо получить не формулу А В, а противоречие в выводе. Допустим, что противоречие не получено (и вывод, следовательно, не построен).

Значит, (ситуация «в») алгоритм использует формулу ¬(А В) в качестве источника для взятия целей и теперь необходимо получить А В снова, т.е. алгоритм возвращается к ситуации «а».

Значит, в работе алгоритма имеет место цикл.

Во избежании цикла авторы предлагают переходить от ситуации «б» к ситуации «в» только, если этим двум ситуациям не предшествовала ситуация «а», т.е.

формула ¬(А В) не была помещена в качестве последней посылки тогда, когда необходимо было получить А В.

В противном случае от ситуации «б» алгоритм переходит не к ситуации «в», а к ситуации «в1»: происходит «выход из алгоритма» и обосновывается выводимость формул ¬А, ¬В из ¬(А В).

Т.к. алгоритм всегда построит вывод формул ¬А, ¬В из формулы ¬(А В), отмечается, что формула ¬(А В) не может быть источником для взятия целей и не возникнет необходимости получать А В. Т.е. от ситуации «в1» алгоритм не перейдет к ситуации «а».

Таким образом, цикл в работе алгоритма ликвидирован. Нетрудно видеть, что выводимость формул ¬А, ¬В из ¬(А В) в ситуации «в1» есть ничто иное, как вводимое сейчас в системы правило ¬и.

Что касается правила ¬и, то объяснение необходимости данного правила сходно с объяснением необходимости правила ¬и, учитывая аналогию между и.

Еще раз обращаем внимание, что может быть построен алгоритм поиска вывода в BMV без правил ¬и, ¬и [Болотов и др.], [Болотов и др.1].

Однако введение этих правил облегчает поиск вывода. Другими словами, вместо того чтобы переходить от ситуации «а» к ситуациям «в» или «в1», если в выводе имеется формула ¬(А В) или ¬А(), мы предлагаем применять к этим формулам, соответственно, правило ¬и или ¬и.

Теперь рассмотрим правила в и и, т.е. те правила системы, которые приводят к появлению в выводе абсолютных переменных.

В формулировке в и и переменные 1,…, n суть все свободные переменные, соответственно, из A(, 1,…, n) и A(, 1,…, n). Отметим, что не может принадлежать {1,…, n}, т.к., согласно определению BMV-вывода, ни одна переменная не может ограничивать сама себя (Определение 2.1.3).

Покажем, что система BMV неявно использует сколемовские функции в правилах в, и. (Явно сколемовские термы используются при формулировке правила и в системе натурального вывода, предложенной Е.К. Войшвилло [Войшвилло], т.е. в той системе, модификацией которой является BMV.) Приведем вариант записи данных правил с использованием сколемовских функций, 1 и т.д. [Мендельсон, с. 111]: в: из А(/(1,…, n)) выводима А; и: из А выводима А(/(1,…, n)), где – новая сколемовская функция, 1,…, n – все свободные переменные в А и в А. При этом нульместные сколемовские функции обозначаются константами a, b и т.д.

Например, результатом сколемизации формулы vwxyz(Q(v, w, y, z) P(f(x, y), g(z))) будет Q(a, w, y, 1(w, y)) P(f((w), y), g(1(w, y))).

Теперь сравним запись с неявным использованием сколемовских термов и запись с использованием таких термов.

А(/(1,…, n)), где – новая функция, A(/, 1,…, n), где – абс., 1,…, n – отн., A(/a), где a – новая константа, если n = В обоих вариантах множество {1,…, n} совпадает. Подстановка везде правильна.

Различия заключаются в следующем: (1) вариант BMV не использует функторы для образования сколемовского терма; (2) в случае n = 0 сколемовский вариант использует константы, а вариант BMV – абсолютные переменные. Более того, сколемовский вариант требует, чтобы константы и функторы были новыми, а вариант BMV не требует, чтобы абсолютные переменные были новыми.

Данные различия исчезают, если отметить содержательную трактовку (полностью верную для правила и и частично верную для правила в) абсолютной переменной как константы, обозначающей некий объект, для которого выполняется А в записи A(/, 1,…, n) или A(/): «Переменная в этом случае … абсолютно ограничена в том смысле, что должна теперь рассматриваться как имя какого-то вполне определенного объекта, удовлетворяющего условию А» [Бочаров и Маркин, с. 133].

Таким образом, везде, где в сколемовском варианте используются константы, вариант BMV использует абсолютные переменные, ведущие себя как константы.

Значит, второе различие устраняется.

Что же касается первого различия в записях A(/, 1,…, n) и А(/(1,…, n)), то содержательно они обозначают одно и тоже: выбор значения для объекта, обозначенного в одном случае как « – абс., 1,…, n – отн.», а в другом – как «(1,…, n)», ограничивает значения для остальных свободных переменных 1,…, n.

Требованию в сколемовском варианте, чтобы сколемовская функция или константа была новой, соответствует требование в варианте BMV, что в BMV-выводе ни одна переменная не может быть абсолютно ограничена дважды (более одного раза).

Таким образом, на самом деле при каждом применении в, и используется новая переменная.

Итак, анализ показал, что в системе BMV неявным образом используется сколемизация. Значит, при задании процедуры поиска вывода в нашей системе можно обойтись без введения сколемовских термов.

содержательно трактующихся как константы, а не как переменные, а также наличие условий корректного использования таких переменных.

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

Другой важной проблемой при поиске вывода является отслеживание переменных, которые ограничивают сами себя (непосредственно или по транзитивности).

Проиллюстрируем необходимость запрета на самоограничение переменной примерами из [Бочаров и Маркин, с. 135]: именно данный запрет, а не требование правильной подстановки не позволяет вывести в системе из A(y, y) формулу xA(x, y) и из xB(x, y) формулу B(y, y). Отмечается, что «при таком переходе переменная y ограничивает сама себя».

Далее авторы пишут: «Надо только учитывать, что ситуация, когда переменная ограничивает сама себя, может возникнуть не только прямым образом, как это было в приведенных примерах, но и косвенно. Здесь имеется в виду то обстоятельство, что отношение «x ограничивает y» является транзитивным, то есть для него верно соотношение: «если ограничивает, а ограничивает, то ограничивает ». В силу этого в системе не проходит доказательство формулы xyP(x, y) yxP(x, y).

Пусть запись < означает, что переменная абсолютно ограничена и переменная ограничена относительно переменной. Т.е. при применении правила в или и по переменной была относительно ограничена переменная, входящая свободно в формулу A() или A().

Свойства отношения ограничения на множестве переменных задаются двумя аксиомами:

¬( < ) – иррефлексивность: ни одна переменная не ограничивает сама себя;

и ограничивает, то ограничивает.

Таким образом, отношение ограничения есть отношение строгого (частичного) порядка.

Заметим, что теория строгого порядка разрешима.

Поскольку в конечном выводе (доказательстве) мы имеем дело только с разрешимость теории строго порядка позволяет за конечное число шагов определить, ограничивает ли произвольная переменная в произвольном BMV-выводе сама себя.

§ 3.2. Унификация Введем основные определения, следуя [Чень и Ли].

абсолютными и неабсолютными переменными, а также работа с множествами ограниченных переменных. Поскольку семантически абсолютные переменные сходны с константами, алгоритм, например, запрещает подстановку одной абсолютной переменной вместо другой абсолютной переменной.

Определение 3.2.1. Подстановка – это конечное множество вида {1/t1, …, n/tn}, где неабсолютных переменных и не заменяет вхождения абсолютных переменных, констант, предметных функторов, предикаторов и логических связок и кванторов.

Свойство 2 исключает подстановку неабсолютной переменной вместо ее самой.

Свойство 3 исключает различные варианты подстановки для одной и той же неабсолютной переменной.

Пусть = {1/t1, …, n/tn} – подстановка и А – формула. Тогда А – формула, полученная из А заменой одновременно всех вхождений i (1 i n) в А на ti.

Пусть = {1/t1, …, n/tn} и = {1/t*1, …, m/t*m} – две подстановки. Тогда композиция и есть подстановка (°), которая получается из множества {1/t1, …, n/tn, 1/t*1, …, m/t*m} вычеркиванием (1) всех элементов j/tj, для которых tj = j, и (2) всех элементов i/t*i таких, что i {1, …, n}.

Свойство (1) отбрасывает подстановки неабсолютной переменной вместо самой себя.

Свойство (2) запрещает различные варианты подстановок вместо одной и той же неабсолютной переменной.

одновременно и левое и правое тождество, т.е. (°)°µ = °(°µ) и ° = ° для всех, Подстановка накрывает подстановку 1 (обозначается 1), если существует подстановка 2: 1 = °2. Если 1 и 1, то = 1.

Определение 3.2.2. Подстановка называется унификатором для множества формул {A1, …, Ak} т.т.т., когда A1 = A2 = … = Ak. Множество формул {A1, …, Ak} унифицируемо, если для этого множества существует унификатор.

Например, подстановка = {x/y, z/v}, где x, z – неабсолютные переменные, y, v – абсолютные переменные, в формулы A(x, v) и A(y, z) приводит к тому, что A(x, v) = A(y, v) = A(y, z). Значит, множество формул {A(x, v) и A(y, z)} унифицируемо.

Определение 3.2.3. Унификатор для множества формул {A1, …, Ak} будет наиболее общим унификатором т.т.т., когда для каждого унификатора для этого множества существует такая подстановка, что = °.

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

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

Например, алгоритм не будет стараться унифицировать формулы P(x, y) и Q(x, y), поскольку данные формулы различаются между собою входящими предикаторами.

Для целей нашего исследования можно ограничиться унификацией только пар формул.

Множество рассогласований D для непустого множества подобных формул {А1, A2} получается выявлением первой (слева) позиции, на которой символы, входящие в формулы А1 и A2, не совпадают, и затем выписыванием из формул А1 и A каждого терма, занимающего эту позицию. Множество этих термов есть множество рассогласований в {А1, A2}.

Например, для формул А1 = P(x, v) и A2 = P(y, z), где x, z – неабсолютные переменные, y, v – абсолютные переменные, множество рассогласований D есть {x, y}.

Поскольку x – неабсолютная переменная и y – абсолютная переменная, то возможна подстановка 1 = {x/y}, которая устраняет множество рассогласований D (индекс 1 обозначает по-порядку номер позиции, на которой возникло данное множество рассогласований).

Однако 1 не является унификатором для {P(x, v), P(y, z)}, поскольку P(x, v) = P(y, v) P(y, z).

Формулы P(y, v) и P(y, z) не совпадают на второй позиции, образуя множество рассогласований D2 = {v, z}. Поскольку z – неабсолютная переменная и v – абсолютная переменная, то возможна подстановка 2 = {z/v}, которая устраняет множество рассогласований D2.

Таким образом, унификатором для формул P(x, v) и P(y, z) является композиция подстановок 1°2 = {x/y, z/v}.

В процессе унификации возможно появление унификатора (подстановки, унифицирующей две формулы), который является композицией подстановок. Значит, первоначальные формулы, унификация которых является исходной задачей, в процессе поиска унификатора изменяются с помощью новых подстановок. В предыдущем примере из формулы P(x, v) при помощи подстановки {x/y} получили формулу P(y, v), а из формулы P(y, z) при помощи подстановки {z/v} получили формулу P(y, v).

Другими словами, если мы обозначим исходную формулу P(x, v) как А0 и исходную формулу P(y, z) как В0, то А1 есть P(y, v) и В1 = В0 = P(y, z). Далее А2 = А1 = P(y, v) и В2 есть P(y, v). Таким образом, А2 = В2, т.е. P(x, v) и P(y, z) унифицируемы.

При этом подстановка {x/y, z/v} – унификатор для формул P(x, v) и P(y, z) – является композицией подстановок {x/y} и {z/v}.

Поскольку {A, A} = {A}, мы будем называть множество вида {A, A} одноэлементным.

Шаг 1. k = 0, Аk = А, Вk = В, k = (пустая подстановка). /Алгоритм берет исходные две формулы А и В, для которых необходимо найти унификатор. Исходным унификатором при этом является пустая подстановка./ Шаг 2. Если ни одна переменная в выводе не ограничивает сама себя, то перейти к шагу 3.

Иначе стоп: Ak и Вk не унифицируемы. Выход из алгоритма. /Попытка унифицировать формулы Ak и Вk приводит к появлению в выводе переменной, которая ограничивает сама себя./ Шаг 3. Если {Ak, Вk} – одноэлементное множество, то стоп: k – наиболее общий унификатор для Ak и Вk. /Устранив k множеств рассогласований между формулами A0 и В0 и получив из формулы A0(B0) формулу Аk(Bk), алгоритм добился, что Ak = Bk. Значит, последняя подстановка является наиболее общим унификатором для формул A0 и В0./ Иначе найдем множество рассогласований Dk для формул Ak и Вk.

Шаг 4. Если существуют такие элементы k и tk в Dk, что k – неабсолютная переменная, которая не входит в tk, то перейти к шагу 5. /Подстановка, во-первых, осуществляется только вместо неабсолютной переменной и другие термы, а также предикаты и логические связки не подлежат замене. Во-вторых, осуществляя подстановку терма вместо неабсолютной переменной, необходимо следить, чтобы заменяемая переменная не входила в этот терм./ Иначе стоп: формулы Ak и Вk не унифицируемы. Выход из алгоритма.

Шаг 5. Пусть k+1 = {k/tk}, Ak+1 = Ak{k/tk} и Вk+1 = Вk{k/tk}. /Осуществляем подстановку k+1 в формулу Ak(Вk) и получаем формулу Ak+1(Вk+1)./ Заметим, что Ak+1 = Ak+1 и Bk+1 = Bk+1. /Это означает, что формула Ak+1(Вk+1) может быть получена из формулы A0(В0) с помощью подстановки k+1 = ((1°2)°3)…°k)), т.е. с помощью композиции k подстановок./ Шаг 6. Присвоить значение k+1 и перейти к шагу 2.

Теорема 3.2.4. Вышеприведенный алгоритм конечен и всегда находит наиболее общий унификатор для унифицируемого множества A.

Доказательство: наш алгоритм унификации отличается от оригинального алгоритма унификации, предложенного в [Чень и Ли], наличием шага 2, т.е. проверкой наличия переменной, которая ограничивает сама себя.

Данная проверка конечна в силу разрешимости теории строго порядка, которая описывает абсолютно и относительно ограниченные переменные в выводе.

С другой стороны, данная проверка сужает множество подстановок, допустимых согласно алгоритму унификации в [Чень и Ли].

Поскольку алгоритм унификации в [Чень и Ли] конечен и всегда находит наиболее общий унификатор, наш алгоритм унификации также конечен и всегда находит наиболее общий унификатор.

Поясним данный алгоритм на примерах.

Рассмотрим несложный пример, когда необходимо унифицировать формулы P(x) и P(y), где х – неабсолютная переменная и y – абсолютная переменная.

Пусть А есть Р(х) и В есть Р(у). Помещаем эти формулы в алгоритм. Тогда А = Р(х) и В0 есть Р(у), k = 0, k = (пустая подстановка) (шаг 1).

Допустим, что в вывод не входит переменная, которая ограничивает сама себя (шаг 2).

Тогда найдем область рассогласований D0 = {x, y} для формул А0 и В0 (шаг 3).

Поскольку неабсолютная переменная х не входит в у, переходим к осуществлению подстановки (шаг 4).

Осуществляем подстановку 1 = {х/у} в формулы А0, B0 и получаем формулы А1, B1. Отметим, что А1 = А01 и B1 = B01 (шаг 5).

Присвоить параметру k значение 1 и вернуться на шаг 2.

Допустим, что в вывод не входит переменная, которая ограничивает сама себя (шаг 2).

А1 = P(y) и В1 = P(y). Значит, {A1, B1} одноэлементное множество. Стоп: 1 = {х/у} – наиболее общий унификатор для Р(х) и Р(у) (шаг 2).

Если в вышеприведенном примере переменная x, как и переменная y, является абсолютной, то формулы не унифицируемы, т.к. подстановка = {x/y} невозможна, поскольку в формулах, согласно определению подстановки, замене подлежат только неабсолютные переменные. В таком случае алгоритм унификации остановится и выдаст ответ, что данное множество формул не унифицируемо.

переменной, которая ограничивает сама себя, для поиска унификатора.

Пусть требуется унифицировать формулы P(x1, y1), P(y2, x2), где y1 < x1 и y2 < x2 и х1, х2 суть неабсолютные переменные. Напомним, что yi < xi означает, что переменная yi абсолютна ограничена и xi относительно ограничена.

Пусть А есть P(x1, y1) и В есть P(y2, x2). Помещаем эти формулы в алгоритм.

Тогда А0 = P(x1, y1) и В0 есть P(y2, x2), k = 0, k = (пустая подстановка) (шаг 1).

Поскольку в y1 < x1 и y2 < x2 ни одна переменная не ограничивает сама себя (шаг 2), то найдем область рассогласований D0 = {x1, y2} для формул А0 и В0 (шаг 3).

Поскольку неабсолютная переменная х1 не входит в у2, переходим к осуществлению подстановки (шаг 4).

Pages: |

| 2 |

Главная >> Диссертации - все темы

[ СКАЧАТЬ ОРИГИНАЛ ДОКУМЕНТА .pdf ]

Похожие работы:

«из ФОНДОВ РОССИЙСКОЙ ГОСУДАРСТВЕННОЙ БИБЛИОТЕКИ Павловская, Елена Эммануиловна 1. Дизайн рекламы 1.1. Российская государственная Библиотека diss.rsl.ru 2003 Павловская, Елена Эммануиловна Дизайн рекламы [Электронный ресурс]: Стратегия проектного творчества : Дис.. д-ра искусствоведения : 17.00.06.-М.: РГБ, 2003 (Из фондов Российской Государственной Библиотеки) Текническая эстетика и дизайн Полный текст: http://diss.rsl.ru/diss/03/1079/031079029.pdf Текст воспроизводится по экземпляру,...»

«Орлов Константин Александрович ИССЛЕДОВАНИЕ СХЕМ ПАРОГАЗОВЫХ УСТАНОВОК НА ОСНОВЕ РАЗРАБОТАННЫХ ПРИКЛАДНЫХ ПРОГРАММ ПО СВОЙСТВАМ РАБОЧИХ ТЕЛ Специальность 05.14.14 – Тепловые электрические станции, их энергетические системы и агрегаты Диссертация на соискание ученой степени кандидата технических наук Москва, 2004 г. -2Расчет свойств газов и их смесей 3.1. Введение В настоящее время теплотехнические расчеты...»

«Карпова Яна Александровна ИНЖЕНЕРНО-ГЕОЛОГИЧЕСКОЕ ОБЕСПЕЧЕНИЕ НАЗЕМНОГО И ПОДЗЕМНОГО СТРОИТЕЛЬСТВА В УСЛОВИЯХ АКТИВНОГО ТЕХНОГЕНЕЗА КОМПОНЕНТОВ ПОДЗЕМНОГО ПРОСТРАНСТВА ПРИМОРСКОГО РАЙОНА САНКТ-ПЕТЕРБУРГА Специальность 25.00.08 – Инженерная геология, мерзлотоведение и...»

«ТВЕРИТНЕВА НАТАЛЬЯ НИКОЛАЕВНА Экономическая оценка эффективности инвестиций в инновационную деятельность, направленную на улучшение экологии мегаполисов Специальность 08.00.05.Экономика и управление народным хозяйством: экономика, организация и управление отраслями, предприятиями, комплексами (строительство) Диссертация на соискание учёной степени кандидата экономических наук Научный руководитель : кандидат...»

«Ермилов Алексей Валерьевич Методы, алгоритмы и программы решения задач идентификации языка и диктора Специальность 05.13.11 — Математическое обеспечение вычислительных машин, комплексов и компьютерных сетей Диссертация на соискание учёной степени кандидата физико-математических наук Научный руководитель :...»

«ЗАЙКИН ОЛЕГ АРКАДЬЕВИЧ Совершенствование приводов транспортно-технологических машин использованием зубчатого бесшатунного дифференциала Специальность 05.02.02 – Машиноведение, системы приводов и детали машин Диссертация на соискание ученой степени кандидата технических наук Научный...»

«Сабанцев Антон Владимирович Молекулярные механизмы действия белков FtsZ, виллина и системы рестрикции-модификации Esp1396I, исследованные флуоресцентными методами. 03.01.02 – биофизика Диссертация на соискание ученой степени кандидата физико-математических наук Научный руководитель : к.ф.-м.н. Ходорковский...»

«из ФОНДОВ РОССИЙСКОЙ ГОСУДАРСТВЕННОЙ БИБЛИОТЕКИ Огарков, Константин Николаевич 1. Юридические формы обеспечения законности в правотворчестве субъектов Российской Федерации 1.1. Российская государственная библиотека diss.rsl.ru 2005 Огарков, Константин Николаевич Юридические формы обеспечения законности в правотворчестве субъектов Российской Федерации [Электронный ресурс]: Дис.. канд. юрид. наук : 12.00.01.-М.: РГБ, 2005 (Из фондов Российской Государственной библиотеки) Государство и право....»

«СВИРИДОВ Константин Сергеевич ПРАВОВОЕ РЕГУЛИРОВАНИЕ ДЕЯТЕЛЬНОСТИ ПО ОКАЗАНИЮ ТУРИСТИЧЕСКИХ УСЛУГ Специальность 12.00.03 Гражданское право; предпринимательское право; семейное право; международное частное право. Диссертация на соискание ученой степени кандидата юридических наук Научный руководитель доктор юридических наук профессор Владимир Федорович ПОПОНДОПУЛО Санкт-Петербург 2003 2 ОГЛАВЛЕНИЕ ВВЕДЕНИЕ ГЛАВА 1. ОБЩАЯ...»

«РЫБАКОВА ЛАРИСА ВЛАДИМИРОВНА МИФОЛОГИЧЕСКИЕ И ОБРЯДОВЫЕ СВЯЗИ РУССКИХ НАРОДНЫХ НЕОБРЯДОВЫХ ПЕСЕН (песни о молодушке и свекре) Специальность 07.00.07 – Этнография Диссертация на соискание ученой степени кандидата исторических наук Научный руководитель – доктор филологических наук Б.Н. ПУТИЛОВ Ленинград СОДЕРЖАНИЕ Введение. Задачи, метод, материал Глава I. О мифологических...»

«Балахонова Алина Сергеевна РЕНИЕВОЕ ОРУДЕНЕНИЕ В ДИКТИОНЕМОВЫХ СЛАНЦАХ ПРИБАЛТИЙСКОГО БАССЕЙНА (ЛЕНИНГРАДСКАЯ ОБЛАСТЬ) Специальность 25.00.11 – геология, поиски и разведка твердых полезных ископаемых, минерагения Диссертация на соискание ученой степени кандидата геолого-минералогических наук Научный руководитель доктор геолого-минералогических...»

«из ФОНДОВ РОССИЙСКОЙ ГОСУДАРСТВЕННОЙ БИБЛИОТЕКИ Иванов, Кирилл Александрович 1. Налоговый дчет и контроль расчетов по налогу на приБыль в производственнык организацияк 1.1. Российская государственная Библиотека diss.rsl.ru 2005 Иванов, Кирилл Александрович Налоговый учет и контроль расчетов по налогу на приБъ1ль в производственны к организацияк [Электронный ресурс]: Дис.. канд. экон. наук : 08.00.12.-М.: РГБ, 2005 (Из фондов Российской Государственной Библиотеки) Экономика — Учет — Российская...»

«Фетисова Евгения Владимировна МЕТОДИКА ДОВУЗОВСКОГО ОБУЧЕНИЯ МАТЕМАТИКЕ ИНОСТРАННЫХ СТУДЕНТОВ, ОБУЧАЮЩИХСЯ НА РУССКОМ ЯЗЫКЕ (МЕДИКО-БИОЛОГИЧЕСКИЙ ПРОФИЛЬ) 13.00.02 - теория и методика обучения и воспитания (математика) Диссертация на соискание ученой степени кандидата педагогических наук Научный руководитель доктор физико-математических...»

«АБРОСИМОВА Светлана Борисовна СОВЕРШЕНСТВОВАНИЕ МЕТОДОВ СЕЛЕКЦИИ КАРТОФЕЛЯ НА УСТОЙЧИВОСТЬ К ЗОЛОТИСТОЙ ЦИСТООБРАЗУЮЩЕЙ НЕМАТОДЕ (GLOBODERA ROSTOCHIENSIS (WOLL.) Специальность: 06.01.05 – селекция и семеноводство сельскохозяйственных растений ДИССЕРТАЦИЯ на соискание учёной степени кандидата...»

«ИЗ ФОНДОВ РОССИЙСКОЙ ГОСУДАРСТВЕННОЙ БИБЛИОТЕКИ Лю Цунъин Особенности этнического самосознания современной учащейся молодёжи Китая Москва Российская государственная библиотека diss.rsl.ru 2006 Лю Цунъин. Особенности этнического самосознания современной учащейся молодёжи Китая [Электронный ресурс] : Дис. . канд. психол. наук : 19.00.01. М.: РГБ, 2006. (Из фондов Российской Государственной Библиотеки). Общая психология, психология личности, история психологии Полный текст:...»

«ИЗ ФОНДОВ РОССИЙСКОЙ ГОСУДАРСТВЕННОЙ БИБЛИОТЕКИ Тюхтенев, Алексей Степанович Экономическая (материальная) основа местного самоуправления в Российской Федерации Москва Российская государственная библиотека diss.rsl.ru 2006 Тюхтенев, Алексей Степанович. Экономическая (материальная) основа местного самоуправления в Российской Федерации [Электронный ресурс] : Теоретикоправовые аспекты : Дис. . канд. юрид. наук : 12.00.02. М.: РГБ, 2006. (Из фондов Российской Государственной Библиотеки)....»

«из ФОНДОВ РОССИЙСКОЙ ГОСУДАРСТВЕННОЙ БИБЛИОТЕКИ Ко5елев, Александр Вячеславович 1. Повышение эффективности культиваторного агрегата с трактором класса О,6 применением активный колес—рыклumeлей 1.1. Российская государственная Библиотека diss.rsl.ru 2003 Ко5елев, Александр Вячеславович Повышение эффективности культиваторного агрегата с трактором класса О,6 применением активный колес-рыклителеи [Электронный ресурс]: Дис.. канд. теки. наук : 05.20.01.-М.: РГБ, 2003 (Из фондов Российской...»

«ПЕТРОВА Татьяна Павловна ЭВОЛЮЦИЯ ВНЕШНЕЙ ПОЛИТИКИ И ДИПЛОМАТИИ ПЕРУ (1821-2013 гг.) Диссертация на соискание ученой степени доктора исторических наук Специальность: 07.00.15 – история международных отношений и внешней политики Москва – 2014 2 Содержание ВВЕДЕНИЕ 5 ГЛАВА 1 34 ФОРМИРОВАНИЕ МИНИСТЕРСТВА ИНОСТРАННЫХ ДЕЛ РЕСПУБЛИКИ ПЕРУ. ОСНОВНЫЕ ЦЕЛИ И ЗАДАЧИ ВНЕШНЕЙ ПОЛИТИКИ В НАЧАЛЬНЫЙ ПЕРИОД НЕЗАВИСИМОСТИ Раздел 1.1. Анализ начального этапа...»

«АБУ ТРАБИ Айман Яхяевич^ КЛИНИЧЕСКОГО ПР0ЯВЛЕНР1Я И ОСОБЕННОСТИ ЛЕЧЕНИЯ ДОБРОКАЧЕСТВЕННОЙ ОПЕРАТИВНОГО ГИПЕРПЛАЗИИ ПРЕДСТАТЕЛЬНОЙ ЖЕЛЕЗЫ У БОЛЬНЫХ С КРУПНЫМИ И ГИГАНТСКИМИ ОБЪЁМАМИ ПРОСТАТЫ 14.00.40. - урология ДИССЕРТАЦИЯ на соискание ученой степени кандидата медицинских наук Научный руководитель : Доктор медицинских наук, профессор М.И. КОГАН Ростов-на-Дону 2003 г. ОГЛАВЛЕНИЕ стр. ВВЕДЕНИЕ ОБЗОР ЛИТЕРАТУРЫ...»

«ИЗ ФОНДОВ РОССИЙСКОЙ ГОСУДАРСТВЕННОЙ БИБЛИОТЕКИ Кирпичев, Александр Александрович Повышение эффективности вибродиагностики с использованием пьезоэлектрических и вихретоковых преобразователей Москва Российская государственная библиотека diss.rsl.ru 2007 Кирпичев, Александр Александрович. Повышение эффективности вибродиагностики с использованием пьезоэлектрических и вихретоковых преобразователей [Электронный ресурс] : дис. . канд. техн. наук : 05.11.13. М.: РГБ, 2007. (Из фондов...»

наверх

<< ГЛАВНАЯ | КОНТАКТЫ

БЕСПЛАТНАЯ ЭЛЕКТРОННАЯ БИБЛИОТЕКА (Авторефераты, диссертации, методички, учебные программы, монографии)

«АВТОМАТИЧЕСКИЙ ПОИСК НАТУРАЛЬНОГО ВЫВОДА В КЛАССИЧЕСКОЙ ЛОГИКЕ ПРЕДИКАТОВ Диссертация на соискание ученой степени кандидата философских наук ...»

ШАНГИН ВАСИЛИЙ ОЛЕГОВИЧ

АВТОМАТИЧЕСКИЙ ПОИСК НАТУРАЛЬНОГО ВЫВОДА

В КЛАССИЧЕСКОЙ ЛОГИКЕ ПРЕДИКАТОВ

ОГЛАВЛЕНИЕ

БЕСПЛАТНАЯ ЭЛЕКТРОННАЯ БИБЛИОТЕКА
(Авторефераты, диссертации, методички, учебные программы, монографии)