Lesson 5 — Simulating Rules of Inference

Setup Common imports & the Rule abstraction SymPy

Every exercise below assumes:

Python — preamblefrom dataclasses import dataclass from typing import Callable, Tuple from sympy import symbols, And, Or, Not, Implies from sympy.logic.boolalg import Boolean from sympy.logic.inference import satisfiable # Generic propositional atoms used throughout p, q, r, s, t, u = symbols('p q r s t u') class InferenceError(Exception): """Raised when a rule's premises don't fit its pattern.""" @dataclass class Rule: name: str arity: int # how many premises it takes apply: Callable[..., Boolean] # function: premises -> conclusion def __call__(self, *premises): if len(premises) != self.arity: raise InferenceError( f"{self.name} expects {self.arity} premise(s), got {len(premises)}" ) return self.apply(*premises)

Each exercise asks you to fill in an apply function and wrap it in a Rule.

Conventions: use isinstance(x, Implies) / And / Or / Not to pattern-match; use x.args to access sub-formulae; raise InferenceError when the premises don't match the rule's pattern.

Ex 1 Modus Ponens SymPy

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

Implement modus_ponens(prem1, prem2) -> q. Either order should be accepted (the rule should figure out which premise is the implication).

Skeletondef mp_apply(a, b): """Return q from premises (p, p→q) or (p→q, p).""" # 1. Identify which of a, b is an Implies; let imp be that one and fact the other. # 2. Check that imp.args[0] == fact; else raise InferenceError. # 3. Return imp.args[1]. ... MP = Rule(name="Modus Ponens", arity=2, apply=mp_apply) # Test: assert MP(p, Implies(p, q)) == q assert MP(Implies(p, q), p) == q print("Modus Ponens simulated:", MP(p, Implies(p, q)))

Ex 2 Modus Tollens SymPy

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

Implement modus_tollens(prem1, prem2) -> Not(p). The premises can be given in either order.

Skeletondef mt_apply(a, b): """Return Not(p) from premises (¬q, p→q) or (p→q, ¬q).""" # 1. Find the Implies among a, b; call it imp. # 2. The other premise should be Not(imp.args[1]); else raise. # 3. Return Not(imp.args[0]). ... MT = Rule(name="Modus Tollens", arity=2, apply=mt_apply) # Test: assert MT(Not(q), Implies(p, q)) == Not(p) print("Modus Tollens simulated:", MT(Not(q), Implies(p, q)))

Ex 3 Hypothetical Syllogism SymPy

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

Implement hyp_syll(imp1, imp2) -> Implies(p, r). The two implications must chain — the consequent of one must equal the antecedent of the other.

Skeletondef hs_apply(a, b): """Return Implies(p, r) from (p→q, q→r) in any order.""" # 1. Both a, b must be Implies; let ((pA, qA), (pB, qB)) = (a.args, b.args). # 2. If qA == pB: return Implies(pA, qB) # 3. Elif qB == pA: return Implies(pB, qA) # 4. Else raise InferenceError. ... HS = Rule(name="Hypothetical Syllogism", arity=2, apply=hs_apply) assert HS(Implies(p, q), Implies(q, r)) == Implies(p, r) assert HS(Implies(q, r), Implies(p, q)) == Implies(p, r) print("Hyp. Syll. simulated:", HS(Implies(p, q), Implies(q, r)))

Ex 4 Disjunctive Syllogism SymPy

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

Implement disj_syll(disj, neg) -> q. The function must also handle (¬q, p ∨ q) → p (the cancelled side can be either disjunct).

Skeletondef ds_apply(a, b): """Return the surviving disjunct from (a∨b, ¬a) or (a∨b, ¬b).""" # 1. Identify the Or-formula and the Not-formula among a, b. # 2. Let neg.args[0] be the cancelled atom x. # 3. Check x ∈ disj.args; the surviving args are the rest. # 4. If a single arg survives, return it; otherwise return Or(*rest). ... DS = Rule(name="Disjunctive Syllogism", arity=2, apply=ds_apply) assert DS(Or(p, q), Not(p)) == q assert DS(Or(p, q), Not(q)) == p print("Disj. Syll. simulated:", DS(Or(p, q), Not(p)))

Ex 5 Addition SymPy

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

Unlike the other rules, Addition introduces a new formula. Implement addition(p_formula, extra) -> Or(p_formula, extra) with arity 2: the second argument is the disjunct you choose to add.

Skeletondef add_apply(a, extra): """Return Or(a, extra) — no constraint on extra.""" return Or(a, extra) ADD = Rule(name="Addition", arity=2, apply=add_apply) assert ADD(p, q) == Or(p, q) print("Addition simulated:", ADD(p, q))

Ex 6 Simplification SymPy

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

Implement simplification(conj, side='left') returning either the left or the right operand of an And. Use arity 1 (the second parameter is a keyword option).

Skeletondef simp_left(conj): if not isinstance(conj, And): raise InferenceError("Simplification: premise is not a conjunction") return conj.args[0] def simp_right(conj): if not isinstance(conj, And): raise InferenceError("Simplification: premise is not a conjunction") return conj.args[-1] SIMP_L = Rule("Simplification (left)", 1, simp_left) SIMP_R = Rule("Simplification (right)", 1, simp_right) assert SIMP_L(And(p, q)) == p assert SIMP_R(And(p, q)) == q print("Simplification simulated:", SIMP_L(And(p, q)))

Ex 7 Conjunction SymPy

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

Implement conjunction(a, b) -> And(a, b). The simplest rule of all.

Skeletondef conj_apply(a, b): return And(a, b) CONJ = Rule("Conjunction", 2, conj_apply) assert CONJ(p, q) == And(p, q) print("Conjunction simulated:", CONJ(p, q))

Ex 8 Resolution SymPy

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

Implement resolution(c1, c2) -> Or(...). Both premises are clauses (each a literal or an Or of literals). The function must find a complementary pair — a literal $\ell$ in one clause whose negation $\neg \ell$ is in the other — and return the disjunction of the remaining literals.

Skeletondef literals(clause): """Treat a single literal as a 1-element Or.""" return list(clause.args) if isinstance(clause, Or) else [clause] def negate(lit): return lit.args[0] if isinstance(lit, Not) else Not(lit) def res_apply(c1, c2): L1, L2 = literals(c1), literals(c2) # Find any literal x in L1 such that negate(x) is in L2 for x in L1: if negate(x) in L2: rest1 = [y for y in L1 if y != x] rest2 = [y for y in L2 if y != negate(x)] combined = rest1 + rest2 if not combined: return None # empty clause (contradiction) return combined[0] if len(combined) == 1 else Or(*combined) raise InferenceError("Resolution: no complementary literal") RES = Rule("Resolution", 2, res_apply) assert RES(Or(p, q), Or(Not(p), r)) == Or(q, r) print("Resolution simulated:", RES(Or(p, q), Or(Not(p), r)))

Ex 9 Rule registry & dispatcher SymPy

Collect every Rule from exercises 1–8 in a dictionary keyed by name. Then write

SkeletonRULES = {r.name: r for r in [MP, MT, HS, DS, ADD, SIMP_L, SIMP_R, CONJ, RES]} def apply(rule_name, *premises): """Look up a rule by name and apply it to the given premises.""" if rule_name not in RULES: raise InferenceError(f"unknown rule {rule_name!r}") return RULES[rule_name](*premises) # Quick check assert apply("Modus Ponens", p, Implies(p, q)) == q print("Registry contains:", sorted(RULES))

Verify that for every rule, applying it then asking SymPy satisfiable(And(*premises, Not(conclusion))) returns False — i.e. the simulated conclusion is logically entailed.
Print one line per rule confirming this.

Ex 10 Chain the rules to derive a goal SymPy

Reproduce the proof from the lesson (slide 8) by simulation. Given:

$H_1: p \to q,\quad H_2: q \to r,\quad H_3: (r \wedge s) \to t,\quad H_4: t \to u,\quad H_5: s$
Assumption: $p$

Use your simulated rules to build the proof step by step and finish at $u$:

Skeleton# Premises and assumption H1, H2, H3, H4, H5 = ( Implies(p, q), Implies(q, r), Implies(And(r, s), t), Implies(t, u), s, ) step3 = apply("Hypothetical Syllogism", H1, H2) # p → r step5 = apply("Modus Ponens", p, step3) # r step7 = apply("Conjunction", step5, H5) # r ∧ s step9 = apply("Modus Ponens", step7, H3) # t step11 = apply("Modus Ponens", step9, H4) # u print("Derived:", step11) assert step11 == u

Print each intermediate conclusion with its step number, mimicking the lesson's numbered proof list.
Confirm the final step equals u.

Ex 11 Quantifier rules — UI & EG SymPy

$\dfrac{\forall x\, P(x)}{P(c)}$ Universal Instantiation

$\dfrac{P(c)}{\exists x\, P(x)}$ Existential Generalization

SymPy's ForAll / Exists are limited; we simulate them with an explicit predicate + substitution.

Skeletonfrom sympy import Function, Lambda, Symbol, Dummy def universal_instantiation(forall_body, var, c): """forall_body is P(x); we substitute the bound var by constant c.""" return forall_body.subs(var, c) def existential_generalization(P_of_c, c, var): """Represent ∃x P(x) by a Lambda(var, …) wrapped in a marker.""" # Build a fresh body by replacing every occurrence of c with var body = P_of_c.subs(c, var) return ("∃", var, body) # a tagged tuple is enough for simulation UI = Rule("Universal Instantiation", 3, universal_instantiation) EG = Rule("Existential Generalization", 3, existential_generalization) x = Symbol('x') o = Symbol('o') P = Function('P') # UI test: from P(x) (interpreted as ∀x P(x)), conclude P(o) assert UI(P(x), x, o) == P(o) # EG test: from P(o) conclude ∃x P(x) assert EG(P(o), o, x) == ("∃", x, P(x)) print("Quantifier rules simulated correctly.")

Side conditions: in your UI, accept any constant; in UG (not implemented here) you would require the constant be arbitrary (i.e. not occurring in any open assumption); in EI the chosen constant must be fresh.

Ex 12 Mini natural-deduction engine SymPy

Combine everything into a tiny proof checker that takes a proof script — a list of steps where each step is either a premise or (rule_name, [indices into earlier steps]) — and produces a numbered transcript.

Skeletondef run_proof(script): """ script = [ ("premise", H1), ("premise", H2), ("rule", "Hypothetical Syllogism", [0, 1]), ("premise", p), ("rule", "Modus Ponens", [3, 2]), ... ] Returns the list of derived formulae (one per step). """ derived = [] for i, step in enumerate(script): kind = step[0] if kind == "premise": formula = step[1] tag = "premise" else: _, name, ids = step args = [derived[k] for k in ids] formula = apply(name, *args) tag = f"{name} on {ids}" derived.append(formula) print(f"{i:>2}. {formula} [{tag}]") return derived # Run the slide-8 proof script = [ ("premise", Implies(p, q)), # 0 H1 ("premise", Implies(q, r)), # 1 H2 ("rule", "Hypothetical Syllogism", [0, 1]), # 2 p→r ("premise", p), # 3 assumption ("rule", "Modus Ponens", [3, 2]), # 4 r ("premise", s), # 5 H5 ("rule", "Conjunction", [4, 5]), # 6 r∧s ("premise", Implies(And(r, s), t)), # 7 H3 ("rule", "Modus Ponens", [6, 7]), # 8 t ("premise", Implies(t, u)), # 9 H4 ("rule", "Modus Ponens", [8, 9]), # 10 u ] trace = run_proof(script) assert trace[-1] == u

Extend the engine to print a fraction $\dfrac{\text{premises used}}{\text{conclusion}}$ for each step.
Add error reporting: when a rule raises InferenceError, prefix the offending line with FAIL: and continue.
(Bonus) Build a proof_to_latex(script) function that emits a natural-deduction tree in LaTeX (`bussproofs` package).