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

+1 vote
in * TF "Emb. Sys. and Rob." by (430 points)
Exam August 2018, Sequent calculus: Find satisfying assignments for formula (b ∧ d) ⊕  (¬c ∨ a). Why does the example solution

1. start with ⊢  ¬((b ∧ d ↔(¬c ∨ a))?
2. place the formula on the right?

1 Answer

0 votes
How does the transformation work? First, what is xor ⊕? Xor ⊕ is true if exactly one or its two arguments is true. It is hence the dual of biimplication/equality, which is true if precisely zero or two of its two arguments become true. Hence, ((b ∧ d) ⊕ (¬c ∨ a)) and ¬((b ∧ d) ↔ (¬c ∨ a)) are equal.

Note that there are two negation symbols on the right of ⊢. One is part of the substituted formula. The other one flips sides. In sequent calculus, you find satisfying assignments (i.e. counterexamples to unsatisfiability) by putting the formula in question to the left. A negation in sequent calculus means a switch of sides. That's why our online tool added a second negation and started on the right. It is equivalent to not adding a negation to this formula and starting on the left.
by (25.6k points)
edited by
Imprint | Privacy Policy