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

1.1k questions

1.3k answers

1.7k comments

556 users

0 votes

The question from the VRS paper on 14th February 2024. This is the question 1)d) satisfiability of phi through sequent calculus. How is the last before node split into two leaf nodes? How do we split the (a xor b) in  sequent calculus?

Sequent calculus

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

1 Answer

0 votes
 
Best answer

We have sequent calculus rules for our basic operators, i.e., negation, conjunction and disjunction. For any other operator like NAND, NOR, XOR, etc. you just have to think about possible ways to rewrite them using negation, conjunction and disjunction, and that will give you rules for the sequent calculus. For XOR, you can use the following rules which create only two subgoals:

  •     XOR_RIGHT (p xor q) <-> (!p|!q) & (p|q)
  •     XOR_LEFT  (p xor q) <-> (p&!q) | (!p&q)

In the same way, you can also obtain rules for equivalence and the if-then-else operator.

by (170k points)
selected by
I got it now.Thank you very much:)!
Imprint | Privacy Policy
...