Skip to content

Latest commit

 

History

History

B

Folders and files

NameName
Last commit message
Last commit date
src
src
 
 
Makefile
Makefile
 
 
README.md
README.md
 
 

README.md

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

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

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

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

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

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

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

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

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

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

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

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

    1. Аксиома: номер аксиомы
    2. Предположение: номер предположения
    3. 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