Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

928 questions

1k answers

1.4k comments

441 users

Two of us encountered two different solutions for Sequent calculus LEFT rule for a implies b as following:

#2 is in out Exercise solution.

#1 is used by few students who passed VRS (also got a decent grade).

Now I am confused which one is correct. Can you please confirm?

UPDATE

Professor confirmed: #1 is correct

I am afraid that the former VRS students are not right, the correct rule is number 2. You can see that also with the following sequent calculus proof trees generated by the tool, and you can verify them also by proving the following formula valid:

((φ → ψ) ∧ Γ → ∆) ↔ ((Γ → φ ∨ ∆) ∧ (ψ ∧ Γ → ∆))