Was this solved correctly? (resolution method)

Question

Using the method of resolution, I can't get to the empty bracket, hence the conclusion isn't a logical consequence.

$s\implies(\neg s\lor t)\vDash \neg s$

My solution:

$s\implies(\neg s\lor t)\vDash \neg s$

$=\neg s \lor(\neg s\lor t)\vDash \neg s$

$=\neg s \lor\neg s\lor t\vDash \neg s$

$=\neg s\lor \neg s\lor t\vDash s$ (conclusion negated)

$=\neg s\lor t \vDash s$ (simplified)

In arrow form: $(t\leftarrow s),\ s\leftarrow$

I'm left with $t$. Since I can't get the empty arrow, then the logical consequence cannot be proven.

Is this correct?

Answer 1

You were mostly correct up until the "conclusion negated" step.

$\lnot s\lor\lnot s\lor\lnot t\vDash \lnot s$ is represented in clausal form as $\big\{\{\lnot s,\lnot s,t\},\{s\}\big\}$ and this simplifies to $\big\{\{\lnot s,t\},\{s\}\big\}$.   Applying resolution to this gives $\big\{\{t\}\big\}$ which cannot be resolved further and is not empty.

Since the clausal form cannot be resolved down to the empty set, therefore the validity of the sequent is determined to be ….