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

524 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 (165k points)
selected by
Got your point.
Thanks for the explanation.

Related questions

Imprint | Privacy Policy
...