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

928 questions

1k answers


441 users

0 votes

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

  1. Split( {} |- a, b |- {} )
  2. Split( {} |- a, {} |- b )

#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?


Professor confirmed: #1 is correct

in * TF "Emb. Sys. and Rob." by (770 points)
edited by

1 Answer

+1 vote
Best answer

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:

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

by (143k points)
selected by
Professor: one question, you said #2 is valid, but the formula you gave above and the tool output aren't proposing #1 is valid?
No, it is number 2. It is the third proof tree from the left where we have a->b on the left side, and this branches into |-a and b|- which is rule #2 you had in question, right?
#2 is |-a and |-b, both on right side
#1 is |-a and b|-, a on right side, bon left side
Ah, got it. Then it is indeed #1, and the exercise solution is wrong.
Imprint | Privacy Policy