MHB Solving Inference Exercise: ¬t∨w

[Quintessential]

Given the following premises: {¬p→r∧¬s, t→s, u→¬p, ¬w, u∨w}
The conclusion is said to be: ¬t∨w
Here are my steps. My conclusion is different from the supposed one, therefore I would appreciate it if any of you can point out my error.

Thank You.

1
¬p→(r∧¬s)
Premise

2
p∨(r∧¬s)
Implication law: 1

3
(p∨r)∧(p∨¬s)
Distributivity: 2

4
(p∨¬s)
Simplification: 3

5
t→s
Premise

6
¬t∨s
Implication law: 5

7
p∨¬t
Resolution: 4 & 6

8
u→¬p
Premise

9
¬u∨¬p
Implication law: 8

10
¬t∨¬u
Resolution: 7 &9

11
u∨w
Premise

12
¬t∨w
Resolution: 10 & 11

13
¬w
Premise

14
¬t
Disjunctive Syllogism: 12 & 13 AND Conclusion

 

[I like Serena]

Hey Quintessential!

Isn't step 12 the conclusion that you're supposed to reach (and prove)?
I think you are done at step 12.
You can always find more conclusions if you want to, but I presume that is not what the problem statement asks.

 

[Quintessential]

Makes sense, thanks!
I was confused because for some of the exercises, I couldn't reach the right conclusion.

For example, the following's conclusion should be t, Given: {p∨q, q→r, p∧s→t, ¬r, ¬q→u∧s}

Yet I find q∨t.
That said. If you prove a contradiction between two premises, and thus dismiss it with either Resolution or Disjunctive Syllogism, is that premise void of future use? In other words, can I reuse previously used premises when stuck?1
p∨q
Premise

2
q→r
Premise

3
¬q∨r
Implication law: 2

4
p∨r
Resolution: 1 & 3

5
p∧s→t
Premise

6
¬p∨(¬s∨t)
Implication law and Associativity: 5

7
r∨(¬s∨t)
Resolution: 4 & 6

8
¬r
Premise

9
¬s∨t
Disjunctive Syllogism: 7 & 8

10
¬q→(u∧s)
Premise

11
q∨(u∧s)
Implication law: 10

12
(q∨u)∧(q∨s)
Distributivity: 11

13
q∨s
Simplification: 12

14
q∨t
Resolution: 9 & 13

 

[I like Serena]

Makes sense, thanks!
I was confused because for some of the exercises, I couldn't reach the right conclusion.

For example, the following's conclusion should be t, Given: {p∨q, q→r, p∧s→t, ¬r, ¬q→u∧s}

Yet I find q∨t.

Perhaps you can combine 3 and 8 to find ¬q?

That said. If you prove a contradiction between two premises, and thus dismiss it with either Resolution or Disjunctive Syllogism, is that premise void of future use? In other words, can I reuse previously used premises when stuck?

Err... you can use any premisse or previous step as often as you like.

 

[Quintessential]

Err... you can use any premisse or previous step as often as you like.

And here I thought, that was a big no no.
Thanks again!

 

[solakis1]

Given the following premises: {¬p→r∧¬s, t→s, u→¬p, ¬w, u∨w}
The conclusion is said to be: ¬t∨w
Here are my steps. My conclusion is different from the supposed one, therefore I would appreciate it if any of you can point out my error.

Thank You.

1
¬p→(r∧¬s)
Premise

2
p∨(r∧¬s)
Implication law: 1

3
(p∨r)∧(p∨¬s)
Distributivity: 2

4
(p∨¬s)
Simplification: 3

5
t→s
Premise

6
¬t∨s
Implication law: 5

7
p∨¬t
Resolution: 4 & 6

8
u→¬p
Premise

9
¬u∨¬p
Implication law: 8

10
¬t∨¬u
Resolution: 7 &9

11
u∨w
Premise

12
¬t∨w
Resolution: 10 & 11

13
¬w
Premise

14
¬t
Disjunctive Syllogism: 12 & 13 AND Conclusion

Your proof is icorrect you need one more step to complete it

And another thing.

If you mention in your proof a law that is not commonly used( like the law resolution in your proof) you have to state clearly how that law works