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

1.1k questions

1.2k answers


543 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 (166k points)
selected by
I understood now. Thank you very much.
Imprint | Privacy Policy