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

1.6k comments

546 users

0 votes
Hello all,

Given the question:

Find a satisfying interpretation of the formula by means of sequent calculus :  

(b ∧ d) ⊕ (¬c ∨ a)

What do I do with the ⊕? What is the rule?

Thanks in advance
in * TF "Intelligent Systems" by (640 points)

1 Answer

+1 vote
 
Best answer

Remember that we defined propositional logic on top of the Hilbert base, i.e., negation, conjunction, and disjunction and introduced all other operators as abbreviations. So, you may just use that abbreviation which is how you should read these operators. 

Clearly, any equivalent form will also do, so you can use in particular one of the following two:

p⊕q = p&!q | !p&q
p⊕q = (!p|!q)&(p|q)

Which one is better? That depends on your example.  Choose a version that minimized branching. 

You may also test which rules are used in the teaching tool for the sequent calculus, and if you create proof trees for p⊕q and its negation, you will obtain the following two (internally, there is no ⊕, so it is expanded to a negated equivalence):

by (166k points)
selected by
Okay..Thank you :)
Imprint | Privacy Policy
...