+
Действующая цена700 499 руб.
Товаров:
На сумму:

Электронная библиотека диссертаций

Доставка любой диссертации в формате PDF и WORD за 499 руб. на e-mail - 20 мин. 800 000 наименований диссертаций и авторефератов. Все авторефераты диссертаций - БЕСПЛАТНО

Расширенный поиск

Некоторые алгоритмические вопросы для формальных систем со свойством интернализации выводов

  • Автор:

    Крупский, Николай Владимирович

  • Шифр специальности:

    01.01.06

  • Научная степень:

    Кандидатская

  • Год защиты:

    2006

  • Место защиты:

    Москва

  • Количество страниц:

    80 с.

  • Стоимость:

    700 р.

    499 руб.

до окончания действия скидки
00
00
00
00
+
Наш сайт выгодно отличается тем что при покупке, кроме PDF версии Вы в подарок получаете работу преобразованную в WORD - документ и это предоставляет качественно другие возможности при работе с документом
Страницы оглавления работы

0.1 Введение
1 Отраженная логика доказательств
1.1 Основные определения
1.2 Конструкция наименьшей модели
1.3 Отраженный фрагмент логики доказательств
1.4 Сложность фрагментов логики доказательств
2 Типизация термов в рефлексивной комбинаторной логике
2.1 Определение правильно построенных формул ВСІ—,
2.2 Типизация подтермов
2.3 Типы в ВСІ ,
2.4 Соответствие между правильно построенными формулами и типами
2.5 Восстановление типов
3 Выводимость в рефлексивной комбинаторной логике
3.1 Выводимость из гипотез в ВС1__*
3.2 Устранение сечения в ВСЬТс
3.3 Разрешимость ВССГс
3.4 Оценки сложности

0.1 Введение.
Под свойством интернализации выводов для формальной системы Т ниже понимается ее способность формализовать рассуждения про свои собственные выводы и их связь с выводимыми ими формулами. Типичным примером формализма такого рода является формальная арифметика первого порядка РА (арифметика Пеано). Гёделевская нумерация синтаксиса РА (см. [15], [11]) позволяет определить инъективное кодирование формул и выводов натуральными числами таким образом, что предикат доказательств
“ж есть код вывода формулы с гёделевским номером у”
оказывается выразимым арифметической формулой .Рг/(ж, у). При этом для любой арифметической формулы <р справедливо
РА ~ (р <^> РА Н Рг/(п, г<рп) для некоторого натурального числа п.
(Здесь п — нумерал, соответствующий числу п, а г<р~1 — гёделевский номер формулы <р.)
Множество всех теорем РА вида Рг/(п, г<рп) образует отраженный фрагмент РА. Фактически, он уже содержит формулировки всех доказуемых в РА утверждений, но в несколько иной форме и с дополнительной информацией про их выводы. В то же время он существенно проще множества всех теорем РА. Естественный выбор деталей кодирования приводит к выражению предиката доказательств посредством Д 1-формулы. Это обеспечивает разрешимость отраженного фрагмента, в то время как множество всех теорем РА неразрешимо.
Аналогичное наблюдение имеет место для всех рекурсивно аксиоматизируемых расширений Т теории РА истинными (в стандартной модели арифметики) формулами. Факт разрешимости отраженного фрагмента теории Т является следствием разрешимости отношения

“d есть вывод формулы <р” для теории Т, а сама теория Т неразрешима ввиду существенной неразрешимости РА (см. [15]). Поэтому отраженный фрагмент устроен проще всей теории Т. Заметим, что это рассуждение использует факт неразрешимости теории Т и неприменимо в случае разрешимых теорий. Для ряда разрешимых формализмов вопрос о сравнении проблем разрешения для теории и сс отраженного фрагмента остается открытым.
Логика доказательств LP С.Н. Артёмова [1], [2], [3], [5], [6] является примером разрешимой пропозициональной логики со свойством интернализации выводов. В языке LP присутствуют выражения двух видов — термы, или полиномы доказательств (proof polynomials), и формулы. Термы строятся из переменных и констант первого вида (“по доказательствам”) с помощью унарной операции “!” (верификация) и бинарных операций (аппликация, применение modus ponens), “+” (объединение доказательств). Формулы строятся из пропозициональных переменных (второго вида) с помощью булевых связок и дополнительного конструктора квазиатомарных формул действующего по следующему правилу:
если t — терм, a F — формула, то t:F является формулой. Логика доказательств LP задается следующим исчислением: Аксиомы:
АО Аксиомы классической логики высказываний в языке LP,
A1 t:F -> F,
А2 t:(F -* G) —> (s:F -> (t ■ s):G),
A3 t.F —► (f + s):F, sF —► (t + s):F,
A4 t:F ->!f:(f:F).
Правила вывода :
(MP) F -> G, F h G,

с-шаблонов определяются аналогично (6). Это размеченные формулы следующих видов (соответственно):
Определение 3.1.2 Будем рассматривать секвенции вида Г =г» где F € ЬРт, а Г является конечным мультимножеством размеченных формул. Секвенция называется правильно построенной, если F и все члены Г являются типами. Секвенциальный вывод назовем правильно построенным, если все секвенции в нем правильно построены. Секвенциальное исчисление БС1_Тс определяется следующим образом:
Аксиомы: все секвенции вида Р, Г =>■ Р, где Р есть типовая переменная р1 или размеченная формула вида Ьс: (7.
Правила:
(р - (<7 -> Н)) - —► <7) ^ > Я)),
(10)
F^G)Г^Я
Г ^ F -> С

Г => А (Яг) Г 1А: А

Рекомендуемые диссертации данного раздела

Название работыАвторДата защиты
F-локальные подгруппы в группах с обобщённо конечными элементами Янченко, Михаил Васильевич 2007
Эффективные алгоритмы для некоторых задач обработки слов Стариковская, Татьяна Андреевна 2012
Алгебра регулярных функций на квантовых M х N -матрицах Мосин, Владимир Геннадьевич 1998
Время генерации: 0.148, запросов: 967