How to generate satisfying interpretation using sequent calculus with tool ?

Question

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} |- {} ?

Answer 1

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.

Comments

Got your point.
Thanks for the explanation.