Add inference rules playground
Create a new interactive playground for practicing rules of inference under Discrete Math > Foundations. The playground will feature a three-column layout for premises, a workspace with parallel lines for derivations, and a column for relevant inference rules. Users can drag and drop elements, apply rules, and receive validation for their steps. The initial example will be based on the provided screenshot.
This commit is contained in:
gpt-engineer-app[bot]
parent
2b22dc0d95
commit
3d2d2fdbff
2 changed files with 339 additions and 0 deletions
331
src/components/RulesOfInferencePlayground.tsx
Normal file
331
src/components/RulesOfInferencePlayground.tsx
Normal file
|
|
@ -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 (
|
||||
<div
|
||||
role="button"
|
||||
draggable
|
||||
onDragStart={handle}
|
||||
className="select-none cursor-grab active:cursor-grabbing rounded-md border border-border bg-card px-3 py-2 text-sm text-foreground shadow-sm hover:bg-accent hover:text-accent-foreground transition-colors"
|
||||
aria-label={label}
|
||||
title={label}
|
||||
>
|
||||
{label}
|
||||
</div>
|
||||
);
|
||||
}
|
||||
|
||||
function DropZone({ children, onDrop, className }: { children?: React.ReactNode; onDrop: (e: React.DragEvent) => void; className?: string }) {
|
||||
return (
|
||||
<div
|
||||
onDragOver={(e) => e.preventDefault()}
|
||||
onDrop={onDrop}
|
||||
className={
|
||||
"min-h-12 rounded-md border border-dashed border-border bg-background/60 p-2 " +
|
||||
(className ?? "")
|
||||
}
|
||||
>
|
||||
{children}
|
||||
</div>
|
||||
);
|
||||
}
|
||||
|
||||
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<Line[]>(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 (
|
||||
<div className="min-h-[70vh] space-y-4">
|
||||
{/* Top controls */}
|
||||
<div className="flex items-center gap-3">
|
||||
<Select value={exampleId} onValueChange={setExampleId}>
|
||||
<SelectTrigger className="w-[360px]">
|
||||
<SelectValue placeholder="Choose example" />
|
||||
</SelectTrigger>
|
||||
<SelectContent>
|
||||
{EXAMPLES.map((ex) => (
|
||||
<SelectItem key={ex.id} value={ex.id}>
|
||||
{ex.title}
|
||||
</SelectItem>
|
||||
))}
|
||||
</SelectContent>
|
||||
</Select>
|
||||
<div className="ml-auto flex items-center gap-2">
|
||||
{reachedTarget && (
|
||||
<span className="text-sm text-muted-foreground">Nice! You derived the target.</span>
|
||||
)}
|
||||
<Button variant="secondary" onClick={reset}>
|
||||
Reset
|
||||
</Button>
|
||||
</div>
|
||||
</div>
|
||||
|
||||
{/* Arena */}
|
||||
<div className="grid grid-cols-1 gap-4 md:grid-cols-3">
|
||||
{/* Left: Premises */}
|
||||
<section aria-label="Premises" className="space-y-2">
|
||||
<h2 className="text-sm font-medium text-muted-foreground">Premises</h2>
|
||||
<div className="space-y-2">
|
||||
{example.premises.map((p) => (
|
||||
<DraggableChip
|
||||
key={p}
|
||||
label={p}
|
||||
onDragStart={(e) => onDragStart(e, "premise", p)}
|
||||
/>
|
||||
))}
|
||||
</div>
|
||||
</section>
|
||||
|
||||
{/* Center: Notepad lines with rule margin */}
|
||||
<section aria-label="Workspace" className="relative">
|
||||
<div className="rounded-lg border border-border bg-card p-2">
|
||||
<div className="grid grid-rows-6 gap-2">
|
||||
{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 (
|
||||
<div key={i} className="grid grid-cols-[1fr_112px] items-stretch gap-2">
|
||||
{/* statement area (left) */}
|
||||
<DropZone
|
||||
onDrop={(e) => handleStatementDrop(i, e)}
|
||||
className={"bg-background min-h-12 flex items-center " + ringCls}
|
||||
>
|
||||
<div className="px-2 text-sm text-foreground">
|
||||
{line.statement ? (
|
||||
<span>{line.statement}</span>
|
||||
) : (
|
||||
<span className="text-muted-foreground">Drop a statement or premise here</span>
|
||||
)}
|
||||
</div>
|
||||
</DropZone>
|
||||
|
||||
{/* rule margin (right) */}
|
||||
<DropZone onDrop={(e) => handleRuleDrop(i, e)}>
|
||||
<div className="flex h-full items-center justify-center rounded-md bg-muted/30 text-xs text-muted-foreground">
|
||||
{line.rule ? <span>{line.rule}</span> : <span>Drop rule</span>}
|
||||
</div>
|
||||
</DropZone>
|
||||
</div>
|
||||
);
|
||||
})}
|
||||
</div>
|
||||
|
||||
{/* Target below last line */}
|
||||
<div className="mt-3 rounded-md border border-border bg-background p-2 text-sm">
|
||||
Target conclusion: <span className="font-medium text-foreground">{example.conclusion}</span>
|
||||
</div>
|
||||
</div>
|
||||
</section>
|
||||
|
||||
{/* Right: Rules */}
|
||||
<section aria-label="Rules" className="space-y-2">
|
||||
<h2 className="text-sm font-medium text-muted-foreground">Rules</h2>
|
||||
<div className="space-y-2">
|
||||
{example.rules.map((r) => (
|
||||
<div key={r.id} className="space-y-1">
|
||||
<DraggableChip
|
||||
label={r.id}
|
||||
onDragStart={(e) => onDragStart(e, "rule", r.id)}
|
||||
/>
|
||||
{r.help && (
|
||||
<p className="text-xs text-muted-foreground pl-1">{r.help}</p>
|
||||
)}
|
||||
</div>
|
||||
))}
|
||||
</div>
|
||||
</section>
|
||||
</div>
|
||||
|
||||
{/* Pool */}
|
||||
<section aria-label="Statements Pool" className="space-y-2">
|
||||
<h2 className="text-sm font-medium text-muted-foreground">Intermediate statements</h2>
|
||||
<div className="grid grid-cols-2 gap-2 md:grid-cols-4">
|
||||
{example.pool.map((s) => (
|
||||
<DraggableChip key={s} label={s} onDragStart={(e) => onDragStart(e, "statement", s)} />
|
||||
))}
|
||||
</div>
|
||||
</section>
|
||||
</div>
|
||||
);
|
||||
}
|
||||
|
|
@ -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("");
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue