Skip to content

Latest commit

 

History

History

mathematical-logic

README.md

Mathematical Logic

Задача 1. Разбор утверждения

Имя входного файла: стандартный ввод
Имя выходного файла: стандартный вывод
Ограничение по времени: 2 секунды
Ограничение по памяти: 256 мегабайт

На вход вашей программе дается утверждение в следующей грамматике:

⟨Файл⟩ ::= ⟨Выражение⟩
⟨Выражение⟩ ::= ⟨Дизъюнкция⟩|⟨Дизъюнкция⟩->⟨Выражение⟩
⟨Дизъюнкция⟩ ::= ⟨Конъюнкция⟩|⟨Дизъюнкция⟩|⟨Конъюнкция⟩
⟨Конъюнкция⟩ ::= ⟨Отрицание⟩|⟨Конъюнкция⟩&⟨Отрицание⟩
⟨Отрицание⟩ ::= !⟨Отрицание⟩|⟨Переменная⟩| (⟨Выражение⟩)
⟨Переменная⟩ ::= (A-Z) {A-Z, 0-9, '}

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

⟨Файл⟩ ::= ⟨Вершина⟩
⟨Вершина⟩ ::= (⟨Знак⟩,⟨Вершина⟩,⟨Вершина⟩)
            | (!⟨Вершина⟩)
            | ⟨Переменная⟩
⟨Знак⟩ ::= ->, |, &
⟨Переменная⟩ ::= (A-Z) {A-Z, 0-9, '}

Формат входных данных

В единственной строке входного файла дано утверждение в грамматике из условия. Размер входного файла не превышает 100 КБ.

Формат выходных данных

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

Примеры

стандартный ввод

!A&!B->!(A|B)

стандартный вывод

(->,(&,(!A),(!B)),(!(|,A,B)))

стандартный ввод

P1'->!QQ->!R10&S|!T&U&V

стандартный вывод

(->,P1',(->,(!QQ),(|,(&,(!R10),S),(&,(&,(!T),U),V))))

Задача 2. Минимизация доказательства

Имя входного файла: стандартный ввод
Имя выходного файла: стандартный вывод
Ограничение по времени: 15 секунд
Ограничение по памяти: 512 мегабайт

На вход вашей программе дается доказательство утверждения в следующей грамматике:

⟨Файл⟩ ::= ⟨Контекст⟩ |- ⟨Выражение⟩ \n ⟨Строка⟩*
⟨Контекст⟩ ::= ⟨Выражение⟩ [,⟨Выражение⟩]*
⟨Строка⟩ ::= ⟨Выражение⟩\n
⟨Выражение⟩ ::= ⟨Выражение⟩&⟨Выражение⟩
              | ⟨Выражение⟩|⟨Выражение⟩
              | ⟨Выражение⟩->⟨Выражение⟩
              | !⟨Выражение⟩
              | (⟨Выражение⟩)
              | ⟨Переменная⟩
⟨Переменная⟩ ::= (A-Z) {A-Z, 0-9, '}

Операторы & и | левоассоциативны. Оператор -> правоассоциативен. Операторы в порядке уменьшения приоритета: !, &, |, ->. Имена переменных не содержат пробелов. Между символами одного оператора нет пробелов (-> и |-). В остальных местах пробелы могут присутствовать. Символы табуляции и возврата каретки должны трактоваться как пробелы. Требуется проверить доказательство на корректность. Если оно неверно, выведите «Proof is incorrect». Иначе минимизируйте и проаннотируйте доказательство. Под минимизацией доказательства подразумевается создание нового доказательства такого, что:

  • Новое доказательство доказывает то же самое утверждение в том же самом контексте

  • Строки нового доказательства являются подпоследовательностью строк исходного доказатель- ства

  • В новом доказательстве ни одно выражение не встречается в нескольких строках

  • В новом доказательстве нет неиспользуемых выражений, т.е. все выражения, кроме последне- го, должны использоваться одним или более применением правила Modus Ponens.

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

  • Все строки должны быть пронумерованы

  • Каждая строка должна содержать пояснение, как она была выведена:

    Аксиома: номер аксиомы
    Предположение: номер предположения
    Modus Ponens: номера строк, в которых записаны выражения, используемые для вывода
    выражения в текущей строке

Формат входных данных

Во входном файле задано доказательство в приведенной выше грамматике. Размер входного файла не превышает 10 МБ.

Формат выходных данных

Если данное доказательство является некорректным, в единственной строке выходного файла должна быть запись «Proof is incorrect». Иначе в файле должно быть минимизированное проаннотированое корректное доказательство. Каждая строка, кроме последней, должна быть использована хотя бы в одной аннотации Modus Ponens. Подробный формат аннотаций смотрите в примерах.

Примеры

стандартный ввод

|- A -> A
A & A -> A
A -> A -> A
A -> (A -> A) -> A
A & A -> A
(A -> A -> A) -> (A -> (A -> A) -> A) -> A -> A
(A -> (A -> A) -> A) -> A -> A
A & A -> A
A -> A

стандартный вывод

|- (A -> A)
[1. Ax. sch. 1] (A -> (A -> A))
[2. Ax. sch. 1] (A -> ((A -> A) -> A))
[3. Ax. sch. 2] ((A -> (A -> A)) -> ((A -> ((A -> A) -> A)) -> (A -> A)))
[4. M.P. 3, 1] ((A -> ((A -> A) -> A)) -> (A -> A))
[5. M.P. 4, 2] (A -> A)

стандартный ввод

A->B, !B |- !A
A->B
!B
!B -> A -> !B
A -> !B
(A -> B) -> (A -> !B) -> !A
(A -> !B) -> !A
!A

стандартный вывод

(A -> B), !B |- !A
[1. Hypothesis 1] (A -> B)
[2. Hypothesis 2] !B
[3. Ax. sch. 1] (!B -> (A -> !B))
[4. M.P. 3, 2] (A -> !B)
[5. Ax. sch. 9] ((A -> B) -> ((A -> !B) -> !A))
[6. M.P. 5, 1] ((A -> !B) -> !A)
[7. M.P. 6, 4] !A

стандартный ввод

A, C |- B'
B'

стандартный вывод

Proof is incorrect

Задача 3. Теорема Гливенко

Имя входного файла: стандартный ввод
Имя выходного файла: стандартный вывод
Ограничение по времени: 15 секунд
Ограничение по памяти: 512 мегабайт

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

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

Формат входных данных

Во входном файле задано доказательство утверждения в классическом исчислении высказываний. Размер входного файла не превышает 5 КБ.

Формат выходных данных

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

Пример

стандартный ввод

A |- A
A

стандартный вывод

A |- !!A
A
(A -> (!A -> A))
(!A -> A)
(!A -> (!A -> !A))
((!A -> (!A -> !A)) -> ((!A -> ((!A -> !A) -> !A)) -> (!A -> !A)))
((!A -> ((!A -> !A) -> !A)) -> (!A -> !A))
(!A -> ((!A -> !A) -> !A))
(!A -> !A)
((!A -> A) -> ((!A -> !A) -> !!A))
((!A -> !A) -> !!A)
!!A

Замечание

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

  1. α -> β -> α
  2. (α -> β) -> (α -> β -> γ) -> (α -> γ)
  3. α -> β -> α & β
  4. α & β -> α
  5. α & β -> β
  6. α -> α | β
  7. β -> α | β
  8. (α -> γ) -> (β -> γ) -> (α | β -> γ)
  9. (α -> β) -> (α -> ¬β) -> ¬α
  10. ¬¬α -> α

В интуиционистском исчислении высказываний 10 -я схема аксиом заменяется на:

  1. α -> ¬α -> β

Задача 4.Полнота исчисления высказываний

Имя входного файла: стандартный ввод
Имя выходного файла: стандартный вывод
Ограничение по времени: 15 секунд
Ограничение по памяти: 512 мегабайт

На вход вашей программе дается утверждениев грамматике из предыдущих заданий. От вас требуется найти:

  • Набор гипотез Γ1 со следующими свойствами:
    • Γ1 состоит только из переменных
    • Γ1 ⊢ α

В этом случае вам нужно вывести доказательство Γ1 ⊢ α.

  • Если такого набора гипотез не нашлось, то нужно найти наименьший набор гипотез Γ2:
    • Γ2 состоит только из отрицаний переменных
    • Γ2 ⊢ ¬α

В этом случае вам нужно вывести доказательство Γ2 ⊢ ¬α.

  • Если и такого набора гипотез не нашлось, то выведите «:(». Если среди предыдущих случаев существует несколько подходящих наборов гипотез (а еслитакие наборы есть, то их всегда бесконечно много), то требуется вывести любой подходящий наборнаименьшего размера.

Формат входных данных

Во входном файле задано утверждение. Размер входного файла не превышает 50 байт. Количество различных переменных, входящих в α, не превосходит 3.

Формат выходных данных

Если требуемого набора гипотез не существует, в единственной строке выведите «:(». Иначе выведите требуемое в условии доказательство, используя грамматику из предыдущих заданий.

Примеры

стандартный ввод

!A

стандартный вывод

:(

стандартный ввод

A -> A & B

стандартный вывод

B |- A -> A & B
B
B -> A -> B
A -> B
A -> B -> A & B
(A -> B) -> (A -> B -> A & B) -> A -> A & B
(A -> B -> A & B) -> A -> A & B
A -> A & B