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

0 votes

Paper -2016.09

Why is the first node in the Sequent calculus tree negated? Is this is a mistake or is there some specific reason?

in * TF "Emb. Sys. and Rob." by (1k points)

1 Answer

+1 vote
 
Best answer
To check satisfiability of a formula, we would have to construct a proof tree where the formula occurs on the left hand side only, and no formula is on the right hand side. The tool is only made for validity, and therefore we start with the negated formula on the right hand side. The next node will be the one you would like to really start with.

Hence, this is just for technical reasons. But you can also say that a formula phi is satisfied by any counterexample shown that its negation is not valid.
by (143k points)
selected by
I understood now. Thank you very much.
Imprint | Privacy Policy
...