Math Help - Inference

1. Inference

Use rules of inference to show that the hypotheses "If it does not rain or if it is not foggy, then the sailing race will be held and the lifesaving demonstration will go on," "If the sailing race is held, then the trophy will be awarded," and "The trophy was not awarded" imply the conclusion "It rained."

I have this so far:
Let p, q, r, s, and t be the propositions.
p: It rained.
q: It is foggy.
r: The sailing race is held.
s: The lifesaving demonstration will go on.
t: The trophy is awarded.

Then the argument form is
( -p V -q) --> (r /\ s)
r --> t
-r
therefore p

How do I break the argument down? The first premise is the issue for me.

2. Originally Posted by lm6485
Use rules of inference to show that the hypotheses "If it does not rain or if it is not foggy, then the sailing race will be held and the lifesaving demonstration will go on," "If the sailing race is held, then the trophy will be awarded," and "The trophy was not awarded" imply the conclusion "It rained."

I have this so far:
Let p, q, r, s, and t be the propositions.
p: It rained.
q: It is foggy.
r: The sailing race is held.
s: The lifesaving demonstration will go on.
t: The trophy is awarded.

Then the argument form is
( -p V -q) --> (r /\ s)
r --> t
-r
therefore p

How do I break the argument down? The first premise is the issue for me.
.
This is an exercise straight out of the middle of chapter 1 in Rosen.
The sections leading up to this exercise cover literally every rule used in the sketch that was presented.
Do addition, simpflication, conjunction, double negation, "modus ponens" (yes Rosen too even calls it detachment), "proof by contradiction" (just another rule) ring any bells?

3. The way we have been doing it in class we have listed each premise fully and then used inference rules to get to the conclusion. My issue is how to get past the first premise ( -p V -q) --> (r /\ s).

4. I don't think you necessarily have to "get past" the first premiss. PiperAlpha167 is correct about your final premiss, incidentally. So you're working with the following:

$(\neg p\vee\neg q)\to(r\land s)$

$r\to t$

$\neg t$

You're asked to prove $p$

So my proof would start like this:

1. $\neg t$ (Premiss 3)

2. $\neg r$ (Modus Tollens with 1. and Premiss 2.)

3. $\neg r\vee\neg s$ (OR introduction, 2.)

Can you see where to go from here?

5. What programming language, uh, inference rules are you using?
PiperAlpha167 has written an outline that is easy to convert into a formal proof in some systems but not others. From my rant in another thread:
If you are looking for a syntactic proof, then you must work with precise inference rules. Saying which formal system you are using is essential in order to get help because there are dozens of such systems, similar to how there are dozens of programming languages. If one asks for help with writing a program but does not specify the programming language, then the most he/she can get is some informal pseudocode.

6. would i use resolution?

7. Like emakarov said, you need to tell us what rules we can invoke here. I don't recognize the term "resolution". It's not a Copi rule or a natural deduction rule. What, in general, does resolution allow you to infer?

8. using precise rules of inference:
resolution
p V q
--p V r

therefore qVr

9. You might be able to use that rule, but I'm not sure where. What group of inference rules are you using?

10. Rules of inference for propositional logic. It is a list from my book. I am just confused how to get to my conclusion with such a large first premise. I have never encountered one that has implies in it. They have always just been one form.

11. Which book? Can you list all the rules?

12. Resolution is a one-rule system that is sound and complete. It is used, for example, in the programming language Prolog.

Resolution is used to build proofs by contradiction: one assumes the negation of the goal and derives a falsehood. Here is falsehood is an empty disjunction. (Recall that a disjunction is true iff there exists a true disjunct.)

To use resolution, all assumptions and the negation of the goal have to be converted into conjunctive normal form. Then individual conjuncts can be separated and considered as independent assumptions.

In this case, (~p V ~q) --> (r /\ s) is equivalent to the conjunction of ~p -> r /\ s and ~q -> r /\ s. The former formula is in turn equivalent to the conjunction of p \/ r and p \/ s. The assumption ~q -> r /\ s is not needed.

Besides this, we have assumptions ~r \/ t, ~t, and the negation of the conclusion ~p. I believe that from here, the empty disjunct can be constructed in three steps using resolution.

13. I think I'm out of my league here. Take it away, emakarov!

14. Discrete Mathematics and Its Applications by Kenneth H. Rosen 6th edition