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

870 questions

988 answers

1.4k comments

439 users

0 votes

I checked the tool (TU Kaiserslautern - Computer Science - Embedded Systems Group: Teaching (uni-kl.de) it is generating the proof tree for validity only like following {} |- {phi} but how can I make it to calculate the satisfiability proof like {phi} |- {} ?

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

1 Answer

+1 vote
 
Best answer
On slide 12, you can see that SAT(φ) holds iff not VALID(¬φ) holds. Hence, to use the sequent calculus (tool) to generate a satisfying assignment, you try to prove that ¬φ is valid. If that proof fails with a counterexample to ¬φ, you have a satisfying assignment for φ. See also slice 108 of the propositional logic chapter that discusses that in detail.
by (139k points)
selected by
Got your point.
Thanks for the explanation.
Imprint | Privacy Policy
...