homework.tex

\documentclass[11pt,a4paper,oneside]{book}
\usepackage[utf8]{inputenc}
\usepackage[english,russian]{babel}
\usepackage{amssymb}
%\usepackage{mathabx}
\usepackage[left=2cm,right=2cm,top=2cm,bottom=2cm,bindingoffset=0cm]{geometry}
\usepackage{bnf}
\newcommand{\lit}[1]{\mbox{`\texttt{#1}'}}
\newcommand{\ntm}[1]{<\mbox{#1}>}
\begin{document}

\begin{center}
\begin{Large}Домашние задания по курсу <<Математическая логика>>\end{Large}\\
ИТМО, группы 2537-2539, осень 2013 г.
\end{center}

Задания с дробными номерами необязательны, их решение, впрочем, будет давать бонус
для зачета. Для всех программ кодировка выходных файлов должна быть либо CP1251,
либо UTF8.

\begin{enumerate}
\item[1] Написать программу, проверяющую доказательства в исчислении высказываний на корректность.
Входной файл представляет из себя последовательность высказываний, по высказыванию
на строку. Высказывания удовлетворяют приведенной ниже грамматике. 
\begin{bnf}\begin{eqnarray*}
\ntm{выражение} &::=& \ntm{дизъюнкция} | \ntm{дизъюнкция} \lit{->} \ntm{выражение}\\
\ntm{дизъюнкция} &::=& \ntm{конъюнкция} | \ntm{дизъюнкция} \lit{|} \ntm{конъюнкция}\\
\ntm{конъюнкция} &::=& \ntm{отрицание} | \ntm{конъюнкция} \lit{\&} \ntm{отрицание}\\
\ntm{отрицание} &::=& (\lit{A} \dots \lit{Z}) \{\lit{0}\dots\lit{9}\}^* | \lit{!} \ntm{отрицание} | \lit{(} \ntm{выражение} \lit{)}
\end{eqnarray*}\end{bnf}%

Результатом работы программы должен быть либо текст: 
\begin{verbatim}
Доказательство корректно.
\end{verbatim}
либо указание на ошибку --- текст вида: 
\begin{verbatim}
Доказательство некорректно начиная с высказывания номер <№>.
\end{verbatim}
где \texttt{<№>} --- это номер строки, содержащей первое недоказанное высказывание.

\item[2] Написать программу, преобразующую вывод $\Gamma, \alpha \vdash \beta$ в вывод
$\Gamma \vdash \alpha \rightarrow \beta$ (либо уведомляющую, что исходный вывод некорректен).
Первой строкой входного файла должна являться строка, перечисляющая гипотезы, использованные 
в выводе, и выводимое утверждение. На следующих строчках входного файла перечислены высказывания
исходного вывода. Высказывания удовлетворяют грамматике из предыдущего задания,
первая строка соответствует следующей грамматике:
\begin{bnf}\begin{eqnarray*}
\ntm{заголовок} &::=& \{\ntm{выражение} \lit{,}\}^* \ntm{выражение} \lit{|-} \ntm{выражение}
\end{eqnarray*}\end{bnf}%

Символ `\texttt{|}' имеет ASCII-код $124$ (десятичное).

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

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

Входной файл состоит из единственной строки, содержащей формулу исчисления высказываний, которую
требуется доказать или опровергнуть. Высказывание удовлетворяет грамматике из первого задания.
Выходной файл должен либо содержать доказательство высказывания (в формате доказательства из 
первого задания), либо содержать фразу, удовлетворяющую грамматике:
\begin{bnf}\begin{eqnarray*}
\ntm{строка} &::=& \lit{Высказывание ложно при } ~\ntm{назначение} \{\lit{,} \ntm{назначение} \}^*\\
\ntm{назначение} &::=& \ntm{переменная} \lit{=} (\lit{И}|\lit{Л})
\end{eqnarray*}\end{bnf}%
Например, при входной формуле \texttt{!A\&!B} результат (с точностью до порядка переменных
и конкретного контрпримера) должен выглядеть так:
\begin{verbatim}
Высказывание ложно при A=И, B=Л
\end{verbatim}

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

Входной файл --- единственная строка, содержащая формулу исчисления высказываний.
Выходной файл --- либо единственная строка
\begin{verbatim}Высказывание общезначимо в интуиционистской логике.\end{verbatim}
либо запись опровергающей его модели Крипке в следующем формате.

Файл состоит из некоторого количества ($n$) строк, $i$-я строчка файла содержит описание  
мира $W_i$. Миры должны быть топологически отсортированы:
если $W_i > W_j$, то $i > j$. При этом все миры, большие данного, должны идти непосредственно
за ним, одним куском: для любого $i$ найдется такой $k$, что $W_i < W_j$ 
тогда и только тогда, когда $i < j \le k$.
Описание представляет из себя символ звёздочки, за которым идет список имен переменных, 
которые вынуждены в данном мире, указанных через запятую. 
Все миры $W_j$, такие что $W_j > W_i$, должны быть описаны в последующих строках,
с отступом от позиции мира $W_i$. Все миры с одинаковым отступом считаются братьями. 
Например:
\begin{verbatim}
*
  * P
    * P,Q
    * P,R
  * Q
\end{verbatim}
В данном примере $W_1 < W_2, W_3, W_4, W_5$, также $W_2 < W_3, W_4$.
Также $W_2 \Vdash P$, $W_3 \Vdash Q$,$W_4 \Vdash R$, $W_5 \Vdash Q$.
Да, этот пример опровергает высказывание $P\vee\neg P\vee Q\vee R$, которое не вынуждено в $W_1$.

\item[4] Написать программу, преобразующую вывод $\Gamma, \alpha \vdash \beta$ в вывод
$\Gamma \vdash \alpha \rightarrow \beta$ (либо уведомляющую, что исходный вывод некорректен)
в исчислении предикатов. Задание аналогично заданию 2, со следующими отличиями:

\begin{itemize}
\item Грамматика исчисления предикатов расширена следующим образом:
\begin{bnf}\begin{eqnarray*}
\ntm{выражение} &::=& \ntm{дизъюнкция} | \ntm{дизъюнкция} \lit{->} \ntm{выражение}\\
\ntm{дизъюнкция} &::=& \ntm{конъюнкция} | \ntm{дизъюнкция} \lit{|} \ntm{конъюнкция}\\
\ntm{конъюнкция} &::=& \ntm{унарное} | \ntm{конъюнкция} \lit{\&} \ntm{унарное}\\
\ntm{унарное} &::=& \ntm{предикат} | \lit{!} \ntm{унарное} | \lit{(} \ntm{выражение} \lit{)}\\
                &|& (\lit{@}|\lit{?}) \ntm{переменная} \ntm{унарное}\\
\ntm{переменная} &::=& (\lit{a} \dots \lit{z}) \{\lit{0}\dots\lit{9}\}^*\\
\ntm{предикат} &::=& (\lit{A} \dots \lit{Z}) \{\lit{0}\dots\lit{9}\}^* [ \lit{(} {\ntm{терм} \{ \lit{,} \ntm{терм} \}^*} \lit{)} ]\\
\ntm{терм} &::=& (\lit{a} \dots \lit{z}) \{\lit{0}\dots\lit{9}\}^*  \lit{(} {\ntm{терм} \{ \lit{,} \ntm{терм} \}^*} \lit{)} \\
             &|& \ntm{переменная} | \lit{(} \ntm{терм} \lit{)}
\end{eqnarray*}\end{bnf}%
Символ `\texttt{@}' обозначает квантор всеобщности, символ `\texttt{?}' --- квантор существования.
Грамматика не различает переменные и константы;
мы можем предполагать, что константы в формуле --- это свободные переменные.

\item Входной файл может содержать некорректный вывод --- а именно, некоторые переходы
в выводе могут быть корректными; входной файл по-прежнему синтаксически корректен.
В этом случае программа должна выдать текст
вида: 
\begin{verbatim}
Вывод некорректен начиная с формулы номер <№>[: <ошибка>]
\end{verbatim}
где вместо \texttt{<№>} подставлен номер первой некорректной формулы. Необязательное поле
\texttt{<ошибка>} должно появляться, если формула не является аксиомой или допущением,
не может быть выведена из предыдущих, но являлась бы (или могла бы быть выведена), 
если бы не нарушение ограничений на переменные. Возможные варианты ошибок:
\begin{verbatim}
терм <X> не свободен для подстановки в формулу <Y> вместо переменной <a>.

переменная <a> входит свободно в формулу <X>.

используется <правило|схема аксиом> с квантором по переменной <a>, 
входящей свободно в допущение <X>.
\end{verbatim}
\end{itemize}

\item[5] Написать программу, проверяющую доказательство в формальной арифметике на корректность.

Грамматика формул формальной арифметики:
\begin{bnf}\begin{eqnarray*}
\ntm{выражение} &::=& \ntm{дизъюнкция} | \ntm{дизъюнкция} \lit{->} \ntm{выражение}\\
\ntm{дизъюнкция} &::=& \ntm{конъюнкция} | \ntm{дизъюнкция} \lit{|} \ntm{конъюнкция}\\
\ntm{конъюнкция} &::=& \ntm{унарное} | \ntm{конъюнкция} \lit{\&} \ntm{унарное}\\
\ntm{унарное} &::=& \ntm{предикат} | \lit{!} \ntm{унарное} | \lit{(} \ntm{выражение} \lit{)}\\
               &|& (\lit{@}|\lit{?}) \ntm{переменная} \ntm{унарное}\\
\ntm{переменная} &::=& (\lit{a} \dots \lit{z}) \{\lit{0}\dots\lit{9}\}^*\\
\ntm{предикат} &::=& (\lit{A} \dots \lit{Z}) \{\lit{0}\dots\lit{9}\}^* [ \lit{(} {\ntm{терм} \{ \lit{,} \ntm{терм} \}^*} \lit{)} ]\\
             &|& \ntm{терм} \lit{=} \ntm{терм}\\
\ntm{терм}   &::=& \ntm{слагаемое} | \ntm{терм} \lit{+} \ntm{слагаемое}\\
\ntm{слагаемое} &::=& \ntm{умножаемое} | \ntm{слагаемое} \lit{*} \ntm{умножаемое}\\
\ntm{умножаемое} &::=& (\lit{a} \dots \lit{z}) \{\lit{0}\dots\lit{9}\}^*  \lit{(} {\ntm{терм} \{ \lit{,} \ntm{терм} \}^*} \lit{)} \\
             &|& \ntm{переменная} | \lit{(} \ntm{терм} \lit{)}\\
             &|& \lit{0} | \ntm{умножаемое} \lit{'}
\end{eqnarray*}\end{bnf}%
От грамматики исчисления предикатов она отличается специальным синтаксисом для предикатов ($=$),
функциональных символов и констант ($\cdot$, $+$, $'$, $0$), использующихся в формальной арифметике.

Выходной файл --- либо фраза 
\begin{verbatim}Доказательство корректно.\end{verbatim}
либо указание об ошибке в формате указания об ошибках для задачи 4.

\item[6] Выразить через примитивы рекурсивных функций:
\begin{itemize}
\item сложение
\item ограниченное вычитание (`$\mathop{-^{\hspace{-.55em}\cdot}\,\,}$'); $a \mathop{-^{\hspace{-.55em}\cdot}\,\,} b = max (a-b,0)$,
\item целочисленное деление ($div$)
\item остаток от деления ($mod$)
\item проверку на простоту ($isPrime$); $isPrime(5)=1, isPrime(9)=0$
\item вычисление $n$-го простого числа ($nthPrime$); $nthPrime(0)=2$
\item частичное логарифмирование ($plog(p,x)$) --- максимальное целое число $r \ge 0$,
такое, что $x$ делится на $p^r$ --- например, $plog (3,12) = 2, plog (5,7) = 0$.
\end{itemize}

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

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

\item[6.5] Реализовать в условиях задачи 6 рекурсивную функцию, вычисляющую функцию Аккермана.
Решение данной задачи должно выдавать корректный ответ для первых чисел Аккермана 
($A(1,1)$, а лучше $A(2,2)$) за разумное время (несколько минут) --- пусть даже для этого
потребуется подменить примитивно-рекурсивную реализацию арифметических функций на <<нативную>>. 

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

\item[7]Написать программу, по натуральному числу $n$ доказывающую
утверждение $(a=0\vee a=\overline{1} \vee \dots \vee a=\overline{n}) \rightarrow a \le \overline{n}$.
Результатом работы программы должен являться текст доказательства --- последовательность формул, по
формуле на каждой строке, записанных в соответствии с требованиями к грамматике формул из задачи 5.

\end{enumerate}

\end{document}