Lesson 5 — Exercises: Rules of Inference

Ref Rules of Inference — Quick Reference

Each rule is shown in natural-deduction (Gentzen) form: premises above the bar, conclusion below.

$\dfrac{p,\;\; p \to q}{q}$ Modus Ponens

$\dfrac{\neg q,\;\; p \to q}{\neg p}$ Modus Tollens

$\dfrac{p \to q,\;\; q \to r}{p \to r}$ Hypothetical Syllogism

$\dfrac{p \vee q,\;\; \neg p}{q}$ Disjunctive Syllogism

$\dfrac{p}{p \vee q}$ Addition

$\dfrac{p \wedge q}{p}$ Simplification

$\dfrac{p,\;\; q}{p \wedge q}$ Conjunction

$\dfrac{p \vee q,\;\; \neg p \vee r}{q \vee r}$ Resolution

Helper to use in all exercises: write a function valid(premises_conj, conclusion) -> bool that returns True iff the argument is valid.

Hint: An argument is valid iff its premises cannot be True while the conclusion is False — i.e., not satisfiable(And(premises, Not(conclusion))).

Ex 1 Modus Ponens SymPy

Verify the validity of Modus Ponens using the valid helper.

$\dfrac{p,\;\; p \to q}{q}$ Modus Ponens

Call valid(And(p, Implies(p, q)), q) and assert the result is True.
In plain language: if it's raining and rain implies wet ground, what can you conclude?

Ex 2 Modus Tollens SymPy

Verify Modus Tollens:

$\dfrac{\neg q,\;\; p \to q}{\neg p}$ Modus Tollens

Build the premises with And(Not(q), Implies(p, q)) and check against Not(p).
Why does this rule work? (Hint: think about the contrapositive.)

Ex 3 Hypothetical Syllogism SymPy

Verify Hypothetical Syllogism:

$\dfrac{p \to q,\;\; q \to r}{p \to r}$ Hypothetical Syllogism

Use three symbols $p, q, r$.
Assert validity and print a confirmation message.

Ex 4 Disjunctive Syllogism SymPy

Verify Disjunctive Syllogism:

$\dfrac{p \vee q,\;\; \neg p}{q}$ Disjunctive Syllogism

In plain language: "It will rain or snow. It will not rain. Therefore it will snow." — verify this is valid.

Ex 5 Addition and Simplification SymPy

Verify both rules:

$\dfrac{p}{p \vee q}$ Addition

$\dfrac{p \wedge q}{p}$ Simplification

For Addition: why is it valid to conclude a weaker statement from a stronger one?
For Simplification: what information is lost when going from $p \land q$ to $p$?

Ex 6 Conjunction and Resolution SymPy

Verify both rules:

$\dfrac{p,\;\; q}{p \wedge q}$ Conjunction

$\dfrac{p \vee q,\;\; \neg p \vee r}{q \vee r}$ Resolution

Resolution is the basis of logic programming (Prolog) and SAT solvers. Why?
Verify both with the valid helper and assert the results.

Ex 7 All Eight Rules in One Sweep SymPy

Store all eight rules in a dictionary mapping rule names to (premises, conclusion) tuples. Iterate over the dictionary and verify every rule is valid.

Print one line per rule: "Modus Ponens : True", etc.
Assert every result is True — if any assertion fails, which rule is broken?

Ex 8 Multi-Step Inference — Swimming SymPy

Model the following argument and verify its validity:

You will go swimming or go to the gym. $\mathrm{Swim} \vee \mathrm{Gym}$
If you go swimming, you will need a swimsuit. $\mathrm{Swim} \to \mathrm{Swimsuit}$

Conclusion: You will need a swimsuit or go to the gym. $\mathrm{Swimsuit} \vee \mathrm{Gym}$

Declare the three symbols, build the premises with And, and call valid.
Which rule of inference is applied here?

Ex 9 Invalid Argument — Affirming the Consequent fallacy

The following is a common logical fallacy. Show that it is not a valid argument:

$\dfrac{p \to q,\;\; q}{p}$ ✗ Affirming the Consequent

Use valid and assert the result is False.
Use satisfiable to find and print a counterexample (assignment where premises are True but conclusion is False).
Give a real-world example of this fallacy.

Example fallacy: "If it rains, the ground is wet. The ground is wet. Therefore it rained." — Can you think of another reason the ground might be wet?

Ex 10 Quantified Rules — Universal & Existential Instantiation Z3

Use Z3 to verify two quantified rules of inference:

Universal Instantiation: $\forall x\; H(x) \to M(x)$ and $H(\text{socrates})$ implies $M(\text{socrates})$.

Declare Person = DeclareSort('Person'), declare functions $H$ and $M$, add the axioms, assume $\neg M(\text{socrates})$, and check for unsat.

Existential Generalization: $M(\text{socrates})$ implies $\exists x\; M(x)$.

Add $M(\text{socrates})$, assume $\neg\exists x\; M(x)$, and check for unsat.

Ex 11 Exam & Director — Full Worked Example SymPy

Model and verify the following argument:

If no one cheated, no one meets the director. $\neg\exists x\,\mathrm{Cheat}(x) \to \neg\exists x\,\mathrm{Director}(x)$
Octave (class president) met the director. $\mathrm{ExDirector}$
Either no one cheated, or someone gets detention. $\neg\mathrm{ExCheat} \vee \mathrm{ExDetention}$

Conclusion: Someone gets a detention. $\mathrm{ExDetention}$

Model each existential claim as a single propositional variable (ExCheat, ExDirector, ExDetention).
Verify the argument with valid and identify which rules are applied (modus tollens + disjunctive syllogism).

Lesson 5 — Rules of Inference