Mathlogic ITMO 2018 course practice tasks

Page at Yandex.Contest

Statement for tasks in russian

Task 0:

Parse logical expressions and print them in prefix form.

Examples:

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

should be

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

---

P->!QQ->!R10&S|!T&U&V

should be

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

Task 1:

Check and annotate proof of classical propositional calculus.

Example:

A,B|-A&B
A
B
A->B->A&B
B->A&B
A->A
A&B

should be

(1) A (Предп. 1)
(2) B (Предп. 2)
(3) (A->(B->(A&B))) (Сх. акс. 3)
(4) (B->(A&B)) (M.P. 3, 1)
(5) (A->A) (Не доказано)
(6) (A&B) (M.P. 4, 2)

Task 2:

Deduction theorem constrictive proof.

Example:

A|-B->A
A->B->A
A
B->A

should be

|-(A->(B->A))
((A->(B->A))->(A->(A->(B->A))))
(A->(B->A))
(A->(A->(B->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->(B->A)))->(A->(B->A))))
((A->(A->(B->A)))->(A->(B->A)))
(A->(B->A))