diff --git a/src/components/RulesOfInferencePlayground.tsx b/src/components/RulesOfInferencePlayground.tsx new file mode 100644 index 0000000..c6e0ba0 --- /dev/null +++ b/src/components/RulesOfInferencePlayground.tsx @@ -0,0 +1,331 @@ +import { useEffect, useMemo, useState } from "react"; +import { Button } from "@/components/ui/button"; +import { Select, SelectContent, SelectItem, SelectTrigger, SelectValue } from "@/components/ui/select"; +import { useToast } from "@/components/ui/use-toast"; + +// Rules of Inference Playground (Example 1: Resolution) +// Layout: 3 columns (Premises | Notepad lines with rule margin | Rules) +// Below: pool of intermediate statements + distractors +// Interaction: drag premises/clauses onto lines, drag a rule to the small right margin for that line, +// then drag a conclusion from the pool to a new line. We validate the step. + +// Types +interface Line { + statement?: string; + rule?: string; // rule id placed in the margin for this line + status?: "pending" | "correct" | "incorrect"; +} + +type DragType = "premise" | "statement" | "rule"; + +interface RuleDef { + id: string; + label: string; + help?: string; +} + +interface ExampleDef { + id: string; + title: string; + premises: string[]; + conclusion: string; + rules: RuleDef[]; + pool: string[]; // candidate intermediate and target statements +} + +const EXAMPLES: ExampleDef[] = [ + { + id: "ex-resolution-1", + title: "(p ∧ q) ∨ r, r → s ⊢ p ∨ s", + premises: ["(p ∧ q) ∨ r", "r → s"], + conclusion: "p ∨ s", + rules: [ + { + id: "distribution", + label: "Distribution: (A ∧ B) ∨ C ≡ (A ∨ C) ∧ (B ∨ C)", + help: "From (p ∧ q) ∨ r you may derive p ∨ r or q ∨ r.", + }, + { + id: "implication-elim", + label: "→ elimination: (A → B) ≡ (¬A ∨ B)", + help: "From r → s you may derive ¬r ∨ s.", + }, + { + id: "resolution", + label: "Resolution", + help: "From (X ∨ r) and (¬r ∨ Y) derive (X ∨ Y).", + }, + ], + pool: [ + "p ∨ r", + "q ∨ r", + "¬r ∨ s", + "p ∨ s", // target + // distractors + "p", + "q", + "r", + "s", + "p ∨ q", + "¬p ∨ s", + ], + }, +]; + +// Small helper to attach drag payload +function onDragStart(e: React.DragEvent, type: DragType, value: string) { + e.dataTransfer.setData("text/plain", JSON.stringify({ type, value })); + e.dataTransfer.effectAllowed = "move"; +} + +function parseDragData(e: React.DragEvent): { type: DragType; value: string } | null { + try { + const raw = e.dataTransfer.getData("text/plain"); + return JSON.parse(raw); + } catch { + return null; + } +} + +function DraggableChip({ label, onDragStart: handle }: { label: string; onDragStart: (e: React.DragEvent) => void }) { + return ( +
+ {label} +
+ ); +} + +function DropZone({ children, onDrop, className }: { children?: React.ReactNode; onDrop: (e: React.DragEvent) => void; className?: string }) { + return ( +
e.preventDefault()} + onDrop={onDrop} + className={ + "min-h-12 rounded-md border border-dashed border-border bg-background/60 p-2 " + + (className ?? "") + } + > + {children} +
+ ); +} + +export default function RulesOfInferencePlayground() { + const { toast } = useToast(); + const [exampleId, setExampleId] = useState(EXAMPLES[0].id); + const example = useMemo(() => EXAMPLES.find((e) => e.id === exampleId)!, [exampleId]); + + const [lines, setLines] = useState(Array.from({ length: 6 }, () => ({ status: "pending" }))); + + useEffect(() => { + // Reset when example changes + setLines(Array.from({ length: 6 }, () => ({ status: "pending" }))); + }, [exampleId]); + + const previousStatements = (upto: number) => + lines.slice(0, upto).map((l) => l.statement).filter(Boolean) as string[]; + + const setLineStatement = (i: number, statement: string) => { + setLines((prev) => { + const next = [...prev]; + next[i] = { ...next[i], statement, status: validateLine(i, { ...next[i], statement }) }; + return next; + }); + }; + + const setLineRule = (i: number, rule: string) => { + setLines((prev) => { + const next = [...prev]; + next[i] = { ...next[i], rule, status: validateLine(i, { ...next[i], rule }) }; + return next; + }); + }; + + const validateLine = (i: number, candidate?: Line): Line["status"] => { + const l = candidate ?? lines[i]; + const stmt = l.statement?.trim(); + const rule = l.rule; + + // Premises allowed with no rule. + if (stmt && example.premises.includes(stmt) && !rule) return "correct"; + + if (!stmt || !rule) return "pending"; + + // Gather earlier statements + const prev = previousStatements(i); + + // Validation rules specific to this example + if (example.id === "ex-resolution-1") { + switch (rule) { + case "distribution": + if (stmt === "p ∨ r" || stmt === "q ∨ r") { + if (prev.includes("(p ∧ q) ∨ r")) return "correct"; + } + break; + case "implication-elim": + if (stmt === "¬r ∨ s" && prev.includes("r → s")) return "correct"; + break; + case "resolution": + if ( + stmt === "p ∨ s" && + prev.includes("p ∨ r") && + prev.includes("¬r ∨ s") + ) + return "correct"; + break; + } + } + + // Not validated + return "incorrect"; + }; + + const handleStatementDrop = (lineIdx: number, e: React.DragEvent) => { + const data = parseDragData(e); + if (!data) return; + if (data.type === "premise" || data.type === "statement") { + setLineStatement(lineIdx, data.value); + const status = validateLine(lineIdx, { ...lines[lineIdx], statement: data.value }); + if (status === "incorrect") + toast({ title: "Not quite", description: "That statement doesn’t follow from your chosen rule and prior lines.", variant: "destructive" }); + } + }; + + const handleRuleDrop = (lineIdx: number, e: React.DragEvent) => { + const data = parseDragData(e); + if (!data) return; + if (data.type === "rule") { + setLineRule(lineIdx, data.value); + } + }; + + const reset = () => setLines(Array.from({ length: 6 }, () => ({ status: "pending" }))); + + const reachedTarget = lines.some((l) => l.statement === example.conclusion && l.status === "correct"); + + return ( +
+ {/* Top controls */} +
+ +
+ {reachedTarget && ( + Nice! You derived the target. + )} + +
+
+ + {/* Arena */} +
+ {/* Left: Premises */} +
+

Premises

+
+ {example.premises.map((p) => ( + onDragStart(e, "premise", p)} + /> + ))} +
+
+ + {/* Center: Notepad lines with rule margin */} +
+
+
+ {Array.from({ length: 6 }).map((_, i) => { + const line = lines[i]; + const ringCls = + line.status === "correct" + ? "ring-1 ring-primary" + : line.status === "incorrect" + ? "ring-1 ring-destructive" + : ""; + return ( +
+ {/* statement area (left) */} + handleStatementDrop(i, e)} + className={"bg-background min-h-12 flex items-center " + ringCls} + > +
+ {line.statement ? ( + {line.statement} + ) : ( + Drop a statement or premise here + )} +
+ + + {/* rule margin (right) */} + handleRuleDrop(i, e)}> +
+ {line.rule ? {line.rule} : Drop rule} +
+ +
+ ); + })} +
+ + {/* Target below last line */} +
+ Target conclusion: {example.conclusion} +
+
+
+ + {/* Right: Rules */} +
+

Rules

+
+ {example.rules.map((r) => ( +
+ onDragStart(e, "rule", r.id)} + /> + {r.help && ( +

{r.help}

+ )} +
+ ))} +
+
+
+ + {/* Pool */} +
+

Intermediate statements

+
+ {example.pool.map((s) => ( + onDragStart(e, "statement", s)} /> + ))} +
+
+
+ ); +} diff --git a/src/pages/theme-pages/discrete-math/Foundations.tsx b/src/pages/theme-pages/discrete-math/Foundations.tsx index 1cdf8c0..afadca3 100644 --- a/src/pages/theme-pages/discrete-math/Foundations.tsx +++ b/src/pages/theme-pages/discrete-math/Foundations.tsx @@ -9,6 +9,7 @@ import BalancedTernaryGame from "@/components/BalancedTernaryGame"; import ZeckendorfGame from "@/components/ZeckendorfGame"; import ZeckendorfSearchTrick from "@/components/ZeckendorfSearchTrick"; import KnightsAndKnavesI from "@/components/KnightsAndKnavesI"; +import RulesOfInferencePlayground from "@/components/RulesOfInferencePlayground"; interface Interactive { id: string; title: string; @@ -52,6 +53,13 @@ const interactives: Interactive[] = [{ tags: ["logic", "puzzle", "knights", "knaves", "truth-tellers"], component: KnightsAndKnavesI, greenScreenPath: "/themes/discrete-math/foundations" +}, { + id: "rules-of-inference", + title: "Rules of Inference Playground", + description: "Practice applying resolution and equivalence rules to derive conclusions step by step.", + tags: ["logic", "proofs", "inference", "resolution", "deduction"], + component: RulesOfInferencePlayground, + greenScreenPath: "/themes/discrete-math/foundations" }]; const Foundations = () => { const [searchTerm, setSearchTerm] = useState("");