Further Reading: Rules of Inference

Annotated pointers for going deeper into inference, fallacies, and the systems that run on them. Start with the textbook sections to firm up the rules, then follow whichever thread pulls you — proof technique, automated reasoning, or the type systems and provers of §3.6.

Core textbook treatments

Rosen, Discrete Mathematics and Its Applications (8th ed.), §1.6–§1.7 The market-standard treatment of rules of inference for propositions and quantifiers, with a large, well-graded exercise bank and tables of the rules matching the ones in this chapter. The best place for extra drill on building derivations and spotting fallacies.

Lehman, Leighton & Meyer, Mathematics for Computer Science (MIT 6.042), proofs chapters Freely available. The most CS-flavored development of "what is a proof and why does each step preserve truth," written for exactly this audience. Pairs well with §3.5 (derivations) and §3.6 (where inference lives in CS); its emphasis on proofs-as-certificates mirrors ours.

Epp, Discrete Mathematics with Applications (5th ed.), §2.3 and §3.4 A patient, example-rich treatment of valid and invalid argument forms (§2.3) and arguments with quantified statements (§3.4). Especially good on naming the fallacies and on the side conditions for universal/existential instantiation — the §3.4 material that trips people up.

Levin, Discrete Mathematics: An Open Introduction (3rd ed.), the logic chapter Freely available. A clean, free alternative to Rosen for the propositional rules and deductions, with approachable exercises. Good if you want a second exposition in different words before exam review.

On proof technique and writing derivations

Velleman, How to Prove It (3rd ed.), the chapters on logic and proof strategy The gentlest careful treatment of turning rules of inference into written proofs. If §3.5's "work backward from the goal, write forward" still feels unsteady, this is the standard recommendation; its strategy-first approach is the same one this chapter teaches.

On automated reasoning and where inference runs

Russell & Norvig, Artificial Intelligence: A Modern Approach (4th ed.), the logical-agents and first-order-inference chapters The standard reference for how machines do inference at scale: resolution, forward and backward chaining, and unification — the algorithmic life of the §3.2 rules (especially resolution) and the §3.4 quantifier rules. Read it to see modus ponens and resolution become search procedures.

Pierce, Types and Programming Languages, the chapters on typed lambda calculus and type checking The canonical text for §3.6's claim that "a type system is a set of inference rules." It develops typing rules in exactly the premises-over-bar notation of this chapter and shows type checking as constructing a derivation. The deep-dive companion to "where inference lives in CS."

Pierce et al., Software Foundations (Volume 1: Logical Foundations) Freely available. An interactive, machine-checked introduction to logic and proof in the Coq proof assistant. The best way to feel §3.5's "a derivation is machine-checkable line by line" — you write proofs and a kernel checks every step, exactly the tool you build in Case Study 2.

Background and the long view

Kahneman, Thinking, Fast and Slow, the chapters on heuristics and biases Not a logic text, but the definitive popular account of why fallacies like affirming the consequent are so persuasive: fast, intuitive reasoning leaps from effect to cause. Useful context for §3.3's claim that spotting bad inference is a learnable, deliberate skill.

Suggested order

  1. Re-read §§3.1–3.3 here, then drill with Rosen §1.6 (propositional rules and fallacies).
  2. Do Rosen §1.7 or Epp §3.4 for the quantifier rules and their side conditions (§3.4).
  3. Read the MIT 6.042 proofs chapters for the CS framing, then Velleman if writing derivations still feels hard (§3.5).
  4. For the §3.6 payoff: skim Russell & Norvig on resolution and chaining, then — if the type-system thread grabs you — Pierce, TAPL, and try a few exercises in Software Foundations to see a real proof checker in action.