Домашние задания по курсу «Математическая логика» ИТМО, группы 2536-2539, осень 2014 г.

Задания 1, 2 и 4. Сделано на С++ в Qt Creator 3.1.0 (основан на Qt 5.2.1). ...

-

Домашние задания по курсу «Математическая логика»
ИТМО, группы 2536-2539, осень 2014 г.
Для всех программ кодировка выходных файлов должна быть либо СР1251, либо 11ТЕ8. Задания 1-4 — для всех групп. Для групп 2536 и 2537 требуется дополнительно сделать одно из заданий 5-8. Для групп 2538 и 2539 требуется выполнить либо 5, либо 6, либо одновременно 7 и 8 задания.
1 Написать программу, проверяющую доказательства в исчислении высказываний на кор¬ректность. Входной файл представляет из себя последовательность высказываний, по вы¬сказыванию на строку. Высказывания удовлетворяют приведенной ниже грамматике.
(выражение)
(дизъюнкция)
(конъюнкция)
(отрицание)
:= (дизъюнкция) | (дизъюнкция) (выражение)
:= (конъюнкция) | (дизъюнкция)11 ’(конъюнкция)
:= ( ) | ( ) ( )
:= (‘А’... ‘Z’) {‘0’..39’}* | ‘! ’ (отрицание) | 1 (’ (выражение) ‘)'
Пробелы в строке должны игнорироваться. Результатом работы программы должен быть проаннотированный текст доказательства, каждая строка должна соответствовать грамма¬тике:
(строка) ::= Ч ’(номер)1) ’(выражение)1 (’(аннотация)!) ’
( ) ::= ( )
| !М.Р. ’(номер)1, ’(номер)
|
(номер) ::= (0’.. 39’) +
Выражение не должно содержать пробелов, номер от выражения и выражение от аннотации должны отделяться одним пробелом. Выражения в доказательстве должны нумероваться подряд натуральными числами с 1. Если выражение получено из у, и у?, где уj = у,, ^ уга путем применения правила Modus Ponens, то аннотация должна выглядеть как !М.Р. г, j’, обратный порядок номеров не допускается.
Уделите внимание производительности: ваша программа должна проверять доказательство в 5000 выражений (общим объемом 1Мб) на Intel Core i5-2520M (2.5 GHz) за несколько секунд.
2 Написать программу, преобразующую вывод Г, а Ь в в вывод Г Ь а ^ в- Первой стро¬кой входного файла должна являться строка, перечисляющая гипотезы, использованные в выводе, и выводимое утверждение. На следующих строчках входного файла перечислены высказывания исходного вывода. Высказывания удовлетворяют грамматике из предыдуще¬го задания, первая строка соответствует следующей грамматике:
(заголовок) ::= {(выражение)1,’}* (выражение)11 -’ (выражение)
Символ Ч’ имеет АБСИ-код 124щ.
Результатом работы программы должен быть текст, содержащий преобразованный вывод. Формат выходного файла совпадает с форматом входного файла. Вы можете предполагать что входной файл содержит корректный вывод требуемой формулы.
3 Написать программу, строящую доказательство указанного во входном файле высказыва¬ния (если оно общезначимо), либо дающую оценку пропозициональных переменных, на ко¬торых высказывание ложно (если оно опровержимо).?
Входной файл состоит из единственной строки, содержащей формулу исчисления высказы¬ваний, которую требуется доказатв или опровергнутв. Ввгсказвгоание удовлетворяет грам¬матике из первого задания. Выходной файл должен либо содержатв доказателвство выска¬зывания (в формате доказателвства из первого задания), либо содержатв фразу, удовлетво¬ряющую грамматике:
(строка) ::= ‘Высказывание ложно при ’ (назначение) {‘,’ (назначение)}* (назначение) ::= (переменная) ‘=’ (‘И’ | ‘Л’)
Например, при входной формуле ! А&! В резулвтат (с точностью до порядка переменных и конкретного контрпримера) должен выглядетв так:
Высказывание ложно при А=И, В=Л
4 Написатв программу, проверяющую доказателвство в формалвной арифметике на коорект- ноств, а также преобразующую вывод Г, а Ь в в вывод Г Ь а ^ в
Грамматика входного файла:
(
(
(
(
(
(
(
(
(
(
(
(
(заголовок) ‘\п’ (доказателвство)
{(выражение) ‘, ’}* (выражение)11 (выражение) {(выражение) ‘\п’}*
(дизъюнкция) | (дизъюнкция) (выражение)
(конъюнкция) | (дизъюнкция)11 ’ (конъюнкция) (унарное) | (конъюнкция) (унарное)
(предикат) | ‘! ’ (унарное) | 1 (’ (выражение) ‘) ’
(‘@’ | ‘?’) (переменная) (унарное)
(‘а’ ...‘г ’) {‘О ’...‘9 ’}*
(‘А’...‘г’) {о’...‘9’}* [ч’(терм) {V (терм)}*1)’] (терм) ‘=’ (терм)
(слагаемое) | (терм) V (слагаемое)
(умножаемое) | (слагаемое)(умножаемое)
(‘а’... ‘г’) {‘О’.. . ‘9’}*‘(’(терм) {‘, ’ (терм)}*1) ’ (переменная) ф(’ (терм) ‘)’
| ( )
Символ ‘®’ обозначает квантор всеобщности, символ “?’ — квантор существования. Грам¬матика не различает переменные и константы; мы можем предполагатв, что константы в формуле — это свободные переменные. Предполагается, что нетерминал разбирается «жадно» — записи ‘®х0=0’ означает некорректное выражение Ужо = 0.
Входной файл может содержатв некорректный вывод — а именно, некоторые переходы в выводе могут бытв корректными; входной файл по-прежнему синтаксически корректен. В этом случае программа должна выдатв текст вида:
Вывод некорректен начиная с формулы номер [: ]
з
где вместо подставлен номер первой некорректной формулы. Необязателвное поле должно появлятися, если формула не является аксиомой или допущением, не может бытв выведена из предыдущих, но являласв бы (или могла бы бытв выведена), если бы не нару¬шение ограничений на переменные. Возможные варианты ошибок:
терм не свободен для подстановки в формулу вместо переменной . переменная входит свободно в формулу .
используется с квантором по переменной , входящей свободно в допущение .
Выходной файл — либо измененное доказательство утверждения Г Ь а ^ в) ПРИ этом вывод должен соответствовать грамматике для ввода, либо сообщение об ошибке. Если в заголовке доказательства отсутствуют гипотезы, то требуется выдать исходное доказательство.
5 Написать программу, по формуле интуиционистского исчисления высказываний строящую опровергающий ее пример в Алгебре Гейтинга, построенной на топологическом простран¬стве R.
Входной файл - формула исчисления высказываний. Выходной файл - либо строчка Формула общезначима
Либо множество вещественных чисел, задаваемое выражением в следующей грамматике:
(строка) ::= {‘(’(граница), (граница)‘)’}+
(граница) ::= ({‘0’ ...‘9’}+ |‘inf’)
а
постными кванторами в вместе с доказательством а Ь в- Доказательство должно соответ¬ствовать формату входных и выходных файлов для задачи 4.
7 Выразите в формальной арифметике отношение и напишите программу, которая по за¬данным входным параметрам доказывает необходимые для представимости утверждения. Идеи по представлению соответствующих формул можно найти в книге Э. Мендельсона «Введение в математическую логику».
Для групп 2538, 2539 необходимо выразить отношение «Ж1 делится на Ж2». Для групп 2536, 2537 — отношение x1 < x2.
Входной файл — числа x1,x2 через пробел.
Выходной файл — доказательство p(x1, x2) ил и —p(x1, x2) (в зависимости от того, выполнено ли R(x1,..., x2)) в формате выходного файла из п. 4 (здесь р — формула, выражающая отношение).
8 Калькулятор ординалов. На вход программе дано два ординала, разделенных символом равенства:
= (выражение) ‘=’ (выражение)
= (слагаемое) | (выражение) ‘+’ (слагаемое)
= (умножаемое) | (слагаемое) ‘*’ (умножаемое) = (умножаемое)| (умножаемое)‘"’(терм)
(
(
(
(
(
| {‘0 ’..‘9 ’}+
| ( )
Выведите в выходной файл слово «Равны», если ординалы равны, и «Не равны», если ординалы отличаются.