From 970f503da54aeae4b2f9b6aedf5c7ca1b8a263cc Mon Sep 17 00:00:00 2001
From: "gpt-engineer-app[bot]"
 <159125892+gpt-engineer-app[bot]@users.noreply.github.com>
Date: Mon, 11 Aug 2025 12:00:48 +0000
Subject: [PATCH] Add more examples to playground

Add two new exercises to the Rules of Inference Playground, making a total of three accessible examples.
---
 src/components/RulesOfInferencePlayground.tsx | 112 ++++++++++++++++++
 1 file changed, 112 insertions(+)

diff --git a/src/components/RulesOfInferencePlayground.tsx b/src/components/RulesOfInferencePlayground.tsx
index 95f6778..ae13252 100644
--- a/src/components/RulesOfInferencePlayground.tsx
+++ b/src/components/RulesOfInferencePlayground.tsx
@@ -71,6 +71,73 @@ const EXAMPLES: ExampleDef[] = [
       "¬p ∨ s",
     ],
   },
+  {
+    id: "ex-modus-ponens-1",
+    title: "A → B ∧ (C ∨ D), A, ¬C ⊢ D",
+    premises: ["A → B ∧ (C ∨ D)", "A", "¬C"],
+    conclusion: "D",
+    rules: [
+      {
+        id: "modus-ponens",
+        label: "Modus Ponens: A, A → B ⊢ B",
+        help: "From A and A → B you may derive B.",
+      },
+      {
+        id: "simplification",
+        label: "Simplification: A ∧ B ⊢ A, A ∧ B ⊢ B",
+        help: "From A ∧ B you may derive A or B.",
+      },
+      {
+        id: "disjunctive-syllogism",
+        label: "Disjunctive Syllogism: A ∨ B, ¬A ⊢ B",
+        help: "From A ∨ B and ¬A you may derive B.",
+      },
+    ],
+    pool: [
+      "B ∧ (C ∨ D)",
+      "C ∨ D",
+      "D", // target
+      // distractors
+      "A",
+      "B",
+      "C",
+      "¬C",
+      "A ∧ B",
+      "B ∨ D",
+    ],
+  },
+  {
+    id: "ex-hypothetical-syllogism",
+    title: "p → q, ¬p → r, r → s ⊢ ¬q → s",
+    premises: ["p → q", "¬p → r", "r → s"],
+    conclusion: "¬q → s",
+    rules: [
+      {
+        id: "contrapositive",
+        label: "Contrapositive: A → B ≡ ¬B → ¬A",
+        help: "From A → B you may derive ¬B → ¬A.",
+      },
+      {
+        id: "hypothetical-syllogism",
+        label: "Hypothetical Syllogism: A → B, B → C ⊢ A → C",
+        help: "From A → B and B → C you may derive A → C.",
+      },
+    ],
+    pool: [
+      "¬q → ¬p",
+      "¬q → r",
+      "¬q → s", // target
+      // distractors
+      "p",
+      "q",
+      "r",
+      "s",
+      "¬p",
+      "¬q",
+      "p → r",
+      "q → s",
+    ],
+  },
 ];
 
 // Small helper to attach drag payload
@@ -192,6 +259,51 @@ export default function RulesOfInferencePlayground({ onComplete }: { onComplete?
           break;
         }
       }
+    } else if (example.id === "ex-modus-ponens-1") {
+      switch (rule) {
+        case "modus-ponens": {
+          // From A and A → B ∧ (C ∨ D) derive B ∧ (C ∨ D)
+          if (selected.includes("A") && selected.includes("A → B ∧ (C ∨ D)") && selected.length === 2) {
+            return ["B ∧ (C ∨ D)"];
+          }
+          break;
+        }
+        case "simplification": {
+          // From B ∧ (C ∨ D) derive B or (C ∨ D)
+          if (selected.includes("B ∧ (C ∨ D)") && selected.length === 1) {
+            return ["C ∨ D"];
+          }
+          break;
+        }
+        case "disjunctive-syllogism": {
+          // From C ∨ D and ¬C derive D
+          if (selected.includes("C ∨ D") && selected.includes("¬C") && selected.length === 2) {
+            return ["D"];
+          }
+          break;
+        }
+      }
+    } else if (example.id === "ex-hypothetical-syllogism") {
+      switch (rule) {
+        case "contrapositive": {
+          // From p → q derive ¬q → ¬p
+          if (selected.includes("p → q") && selected.length === 1) {
+            return ["¬q → ¬p"];
+          }
+          break;
+        }
+        case "hypothetical-syllogism": {
+          // From ¬q → ¬p and ¬p → r derive ¬q → r
+          if (selected.includes("¬q → ¬p") && selected.includes("¬p → r") && selected.length === 2) {
+            return ["¬q → r"];
+          }
+          // From ¬q → r and r → s derive ¬q → s
+          if (selected.includes("¬q → r") && selected.includes("r → s") && selected.length === 2) {
+            return ["¬q → s"];
+          }
+          break;
+        }
+      }
     }
 
     return [];