axiom-embed

Embeddable Fitch-style proof editor Web Components for formal logic education. Provides client-side validation of natural deduction proofs with SCORM compatibility for LMS integration.

Features

- Web Components - Works with any framework (React, Vue, plain HTML)
- Two Modes - Exercise mode (fixed goal) and Sandbox mode (free exploration)
- Configurable Rules - Enable propositional, FOL, or custom rule subsets
- SCORM 1.2/2004 - Full LMS integration with suspend_data and scoring
- Smart Editing - Auto-indent, symbol conversion, rule autocomplete
- Fully Themeable - CSS custom properties for complete visual customization

Installation

$3

``bash
npm install axiom-embed
`

$3

`html

`

Building from Source

`bash


Install dependencies

npm install

Development build with watch mode

npm run dev

Production build

npm run build

Generate TypeScript declarations

npm run build:types

Clean dist directory

npm run clean

Run tests

npm test

Full release build (clean + build + types)

npm run prepublishOnly
`

$3

| File | Format | Description |
|------|--------|-------------|
| dist/axiom-embed.js | ESM | ES module (requires fitch-js as peer dependency) |
| dist/axiom-embed.umd.js | UMD | Standalone bundle (includes fitch-js, auto-injects styles) |
| dist/axiom-embed.css | CSS | Extracted styles (for ESM usage) |
| dist/index.d.ts | TypeScript | Type declarations |

Usage

$3

The UMD bundle auto-initializes and injects styles. Just include the script and use the component:

`html






mode="exercise"
premises='["P", "P -> Q"]'
goal="Q"
rules="propositional"
>


`

$3

When using as an ES module, you must initialize fitch-js manually and import the CSS:

`javascript
import * as AxiomEmbed from 'axiom-embed';
import 'axiom-embed/css';
import * as fitchJS from 'fitch-js';

// Initialize before using components
AxiomEmbed.init(fitchJS);
`

`html
mode="exercise"
premises='["P", "P -> Q"]'
goal="Q"
>
`

$3

`javascript
// main.js
import * as AxiomEmbed from 'axiom-embed';
import 'axiom-embed/css';
import * as fitchJS from 'fitch-js';

AxiomEmbed.init(fitchJS);
`

$3

`jsx
import { useEffect, useRef } from 'react';
import * as AxiomEmbed from 'axiom-embed';
import 'axiom-embed/css';
import * as fitchJS from 'fitch-js';

// Initialize once at app startup
AxiomEmbed.init(fitchJS);

function ProofEditor({ premises, goal, onComplete }) {
const ref = useRef(null);

useEffect(() => {
const el = ref.current;
const handleComplete = (e) => onComplete?.(e.detail);
el?.addEventListener('axiom:complete', handleComplete);
return () => el?.removeEventListener('axiom:complete', handleComplete);
}, [onComplete]);

return (
ref={ref}
mode="exercise"
premises={JSON.stringify(premises)}
goal={goal}
rules="propositional"
/>
);
}
`

Component API

$3

| Attribute | Type | Default | Description |
|-----------|------|---------|-------------|
| mode | "exercise" \| "sandbox" | "sandbox" | Exercise validates against a goal; sandbox is freeform |
| premises | JSON array or CSV | [] | Premises for the proof, e.g. '["P", "P -> Q"]' |
| goal | string | null | Target conclusion for exercise mode |
| rules | preset, JSON array, or CSV | all rules | Allowed proof rules (see Rule Sets) |
| theme | "light" \| "dark" | "light" | Color theme |
| readonly | boolean | false | Disable editing |
| show-toolbar | boolean | false | Show symbol insertion toolbar |
| problem-id | string | "default" | Unique ID for persistence |
| prefill-premises | "true" \| "false" | "true" | Auto-fill premises in editor |
| scoring | preset or JSON | "completion" | Scoring configuration (see Scoring) |
| scorm | boolean | false | Enable SCORM integration |

$3

`javascript
const proof = document.querySelector('axiom-proof');

// Get/set content
proof.getValue(); // Returns current proof text
proof.setValue(content); // Set proof text

// Validation
proof.validate(); // Validate and return result
proof.validate(true); // Validate and count as attempt (affects scoring)
proof.isComplete(); // Check if proof is complete

// State management
proof.reset(); // Reset to initial state
proof.getSuspendData(); // Get serialized state for persistence
proof.setSuspendData(data); // Restore from serialized state

// Scoring
proof.getScore(); // Returns { raw, max, min }
`

$3

`javascript
// Fired on each validation
proof.addEventListener('axiom:validate', (e) => {
console.log(e.detail.isValid); // boolean
console.log(e.detail.issues); // string[]
console.log(e.detail.conclusionReached); // boolean
});

// Fired when proof is successfully completed
proof.addEventListener('axiom:complete', (e) => {
console.log(e.detail.score); // number (0-100)
console.log(e.detail.attempts); // number
console.log(e.detail.elapsedMs); // number
});

// Fired on content change
proof.addEventListener('axiom:change', (e) => {
console.log(e.detail.content); // string
console.log(e.detail.isDirty); // boolean
});

// Fired when component is initialized and ready
proof.addEventListener('axiom:ready', () => {
console.log('Component ready');
});
`

CSS Customization

axiom-embed is fully customizable via CSS custom properties. You can style every aspect of the editor without touching source files.

$3

Override these properties on :root, a parent element, or directly on axiom-proof:

`css
:root {
/ ===== Core Colors ===== /
--axiom-bg: #ffffff; / Editor background /
--axiom-fg: #1a1a1a; / Primary text color /
--axiom-bg-secondary: #f5f5f5; / Header/toolbar/status background /
--axiom-border: #e0e0e0; / Border color /
--axiom-border-focus: #3b82f6; / Focus ring color /

/ ===== Gutter (Line Numbers) ===== /
--axiom-gutter-bg: #fafafa; / Gutter background /
--axiom-gutter-fg: #9ca3af; / Line number color /

/ ===== Error Highlighting ===== /
--axiom-line-error-bg: rgba(239, 68, 68, 0.1); / Error line background /
--axiom-line-error-border: #ef4444; / Error line left border /

/ ===== Syntax Highlighting ===== /
--axiom-syn-op: #7c3aed; / Operators: ->, /\, \/, <->, ~, etc. /
--axiom-syn-var: #0891b2; / Variables: P, Q, x, y /
--axiom-syn-pred: #2563eb; / Predicates: F(x), G(x,y) /
--axiom-syn-rule: #059669; / Rule names: ->E, /\I, Hyp, PR /
--axiom-syn-cite: #d97706; / Line citations: 1, 2-4 /
--axiom-syn-comment: #9ca3af; / Comments /
--axiom-syn-depth: #d4d4d4; / Subproof depth markers (|) /
--axiom-syn-paren: #6b7280; / Parentheses /
--axiom-syn-colon: #6b7280; / Colons /

/ ===== Autocomplete Dropdown ===== /
--axiom-dropdown-bg: #ffffff;
--axiom-dropdown-border: #e0e0e0;
--axiom-dropdown-shadow: 0 4px 12px rgba(0, 0, 0, 0.15);
--axiom-dropdown-selected: #eff6ff; / Selected item background /
--axiom-dropdown-hover: #f5f5f5; / Hovered item background /

/ ===== Typography ===== /
--axiom-font-mono: ui-monospace, 'Cascadia Code', 'Source Code Pro', Menlo, Consolas, monospace;
--axiom-font-ui: system-ui, -apple-system, sans-serif;
--axiom-font-size: 14px;
--axiom-line-height: 1.5;

/ ===== Spacing & Shape ===== /
--axiom-padding: 12px;
--axiom-radius: 6px;
}
`

$3

Apply styles to individual proof editors:

`css
/ Target a specific editor by ID /
#my-custom-proof {
--axiom-bg: #1a1a2e;
--axiom-fg: #eaeaea;
--axiom-syn-op: #ff6b6b;
--axiom-font-size: 16px;
}

/ Target all editors in a container /
.proof-container axiom-proof {
--axiom-radius: 12px;
--axiom-border: #333;
}
`

$3

#### High Contrast Theme

`css
.high-contrast axiom-proof {
--axiom-bg: #000000;
--axiom-fg: #ffffff;
--axiom-bg-secondary: #1a1a1a;
--axiom-border: #ffffff;
--axiom-border-focus: #ffff00;
--axiom-gutter-bg: #0a0a0a;
--axiom-gutter-fg: #cccccc;
--axiom-syn-op: #ff6b6b;
--axiom-syn-var: #4ecdc4;
--axiom-syn-pred: #45b7d1;
--axiom-syn-rule: #95e1d3;
--axiom-syn-cite: #f9ca24;
--axiom-line-error-bg: rgba(255, 0, 0, 0.3);
--axiom-line-error-border: #ff0000;
--axiom-dropdown-bg: #1a1a1a;
--axiom-dropdown-selected: #333333;
}
`

#### Solarized Light Theme

`css
.solarized-light axiom-proof {
--axiom-bg: #fdf6e3;
--axiom-fg: #657b83;
--axiom-bg-secondary: #eee8d5;
--axiom-border: #93a1a1;
--axiom-gutter-bg: #eee8d5;
--axiom-gutter-fg: #93a1a1;
--axiom-syn-op: #cb4b16;
--axiom-syn-var: #268bd2;
--axiom-syn-pred: #2aa198;
--axiom-syn-rule: #859900;
--axiom-syn-cite: #b58900;
--axiom-dropdown-bg: #fdf6e3;
--axiom-dropdown-selected: #eee8d5;
}
`

#### Nord Theme

`css
.nord axiom-proof {
--axiom-bg: #2e3440;
--axiom-fg: #eceff4;
--axiom-bg-secondary: #3b4252;
--axiom-border: #4c566a;
--axiom-border-focus: #88c0d0;
--axiom-gutter-bg: #3b4252;
--axiom-gutter-fg: #4c566a;
--axiom-syn-op: #b48ead;
--axiom-syn-var: #88c0d0;
--axiom-syn-pred: #81a1c1;
--axiom-syn-rule: #a3be8c;
--axiom-syn-cite: #ebcb8b;
--axiom-syn-depth: #4c566a;
--axiom-dropdown-bg: #3b4252;
--axiom-dropdown-border: #4c566a;
--axiom-dropdown-selected: #434c5e;
--axiom-dropdown-hover: #434c5e;
}
`

#### Monokai Theme

`css
.monokai axiom-proof {
--axiom-bg: #272822;
--axiom-fg: #f8f8f2;
--axiom-bg-secondary: #3e3d32;
--axiom-border: #49483e;
--axiom-border-focus: #a6e22e;
--axiom-gutter-bg: #3e3d32;
--axiom-gutter-fg: #75715e;
--axiom-syn-op: #f92672;
--axiom-syn-var: #66d9ef;
--axiom-syn-pred: #a6e22e;
--axiom-syn-rule: #e6db74;
--axiom-syn-cite: #fd971f;
--axiom-syn-comment: #75715e;
}
`

$3

Use the theme="dark" attribute:

`html

`

Or apply programmatically:

`javascript
proof.setAttribute('theme', 'dark');
`

$3

`javascript
function setTheme(themeName) {
const proof = document.querySelector('axiom-proof');
proof.setAttribute('theme', themeName);
}

// Or using CSS classes
function applyCustomTheme(className) {
document.body.className = className; // e.g., 'nord', 'monokai'
}
`

$3

`css
/ Smaller font on mobile /
@media (max-width: 768px) {
axiom-proof {
--axiom-font-size: 12px;
--axiom-padding: 8px;
}
}

/ Larger font for accessibility /
@media (prefers-reduced-motion: reduce) {
axiom-proof {
--axiom-font-size: 18px;
}
}
`

Rule Sets

$3

| Preset | Rules Included |
|--------|---------------|
| propositional | PR, Hyp, R, ∧I, ∧E, ∨I, ∨E, →I, →E, ↔I, ↔E, ¬I, ¬E, ⊥I, ⊥E |
| fol | All propositional + ∀I, ∀E, ∃I, ∃E, =I, =E, LEM |
| structural | PR, Hyp, R |

$3

`html








`

$3

| Symbol | ASCII | Name | Category |
|--------|-------|------|----------|
| PR | - | Premise | Structural |
| Hyp | - | Hypothesis (starts subproof) | Structural |
| R | - | Reiteration | Structural |
| ∧I | /\I | And Introduction | Propositional |
| ∧E | /\E | And Elimination | Propositional |
| ∨I | \/I | Or Introduction | Propositional |
| ∨E | \/E | Or Elimination | Propositional |
| →I | ->I | Conditional Introduction | Propositional |
| →E | ->E | Modus Ponens | Propositional |
| ↔I | <->I | Biconditional Introduction | Propositional |
| ↔E | <->E | Biconditional Elimination | Propositional |
| ¬I | ~I | Negation Introduction | Propositional |
| ¬E | ~E | Negation Elimination | Propositional |
| ⊥I | !?I | Contradiction Introduction | Propositional |
| ⊥E | !?E | Explosion (Ex Falso) | Propositional |
| ∀I | !AI | Universal Introduction | FOL |
| ∀E | !AE | Universal Elimination | FOL |
| ∃I | !EI | Existential Introduction | FOL |
| ∃E | !EE | Existential Elimination | FOL |
| =I | - | Identity Introduction | FOL |
| =E | - | Identity Elimination | FOL |
| LEM | - | Law of Excluded Middle | Meta |

Scoring

$3

| Mode | Description |
|------|-------------|
| completion | 100 points on completion, 0 otherwise (default) |
| attempts | Base score minus penalty per attempt after first |
| none | Scoring disabled |

$3

`html







`

$3

| Parameter | Default | Description |
|-----------|---------|-------------|
| mode | "completion" | Scoring mode |
| baseScore | 100 | Maximum score |
| attemptPenalty | 5 | Points deducted per attempt (attempts mode) |
| maxPenalty | 20 | Maximum total penalty (attempts mode) |

SCORM Integration

Enable SCORM for LMS integration:

`html
scorm
problem-id="lesson1-problem1"
mode="exercise"
premises='["P"]'
goal="P ∨ Q"
>
`

$3

- Auto-detects SCORM 1.2 or 2004 API
- Saves/restores student progress via suspend_data
- Reports scores on completion
- Updates completion and success status
- Falls back to localStorage when no LMS detected

$3

`html



`

Symbol Input

$3

Enable the symbol toolbar with show-toolbar:

`html

`

$3

Type ASCII sequences that auto-convert to Unicode symbols:

| Type | Get |
|------|-----|
| -> | → |
| /\ | ∧ |
| \/ | ∨ |
| <-> | ↔ |
| ~ | ¬ |
| _\|_ | ⊥ |
| @ | ∀ |
| $ | ∃ |

$3

Type : after a formula to trigger rule autocomplete. Navigate with arrow keys, select with Enter/Tab.

Proof Format

Each line follows the format:

`
:
`

Subproofs use leading pipe characters for indentation:

`
P → Q :PR
P :PR
| P :Hyp
| Q :→E 1 2
P → Q :→I 3-4
`

$3

- Single line: 1, 5
- Multiple lines: 1 3, 2 5
- Line range (for subproofs): 3-7

Examples

$3

`html
mode="exercise"
premises='["P", "P → Q"]'
goal="Q"
rules="propositional"
show-toolbar
>
`

$3

`html
mode="sandbox"
rules="fol"
show-toolbar
>
`

$3

`html
mode="exercise"
premises='["P ∧ Q"]'
goal="Q ∧ P"
theme="dark"
scoring='{"mode": "attempts", "attemptPenalty": 5}'
>
`

$3

`html



`

$3

`html




`

TypeScript Support

Full TypeScript support with exported types:

`typescript
import type {
ProofState,
ValidationResult,
SuspendData,
ProofRule,
ScoringConfig,
Theme,
Mode,
CursorPosition,
EditorOptions,
AxiomEvents,
} from 'axiom-embed';
``

Browser Support

- Chrome/Edge 88+
- Firefox 78+
- Safari 14+

Requires native Custom Elements v1 and Shadow DOM support.

License

MIT