axiom-embed

v0.1.0

Published

4 months ago

Embeddable Fitch-style proof editor Web Components

0High
0Medium
0Low

lagomorph_labs

logic proof fitch natural-deduction education scorm web-components

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

npm

npm install axiom-embed

CDN / Script Tag

<script src="https://unpkg.com/axiom-embed/dist/axiom-embed.umd.js"></script>

Building from Source

# 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

Build Outputs

| 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

UMD Bundle (Simplest)

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

<!DOCTYPE html>
<html>
<head>
  <script src="axiom-embed.umd.js"></script>
</head>
<body>
  <axiom-proof
    mode="exercise"
    premises='["P", "P -> Q"]'
    goal="Q"
    rules="propositional"
  ></axiom-proof>
</body>
</html>

ESM Module

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

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

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

<axiom-proof
  mode="exercise"
  premises='["P", "P -> Q"]'
  goal="Q"
></axiom-proof>

With Bundlers (Vite, Webpack, etc.)

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

AxiomEmbed.init(fitchJS);

With React

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 (
    <axiom-proof
      ref={ref}
      mode="exercise"
      premises={JSON.stringify(premises)}
      goal={goal}
      rules="propositional"
    />
  );
}

Component API

`<axiom-proof>` Attributes

| 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 |

JavaScript API

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 }

Events

// 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.

CSS Custom Properties Reference

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

: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;
}

Styling Specific Instances

Apply styles to individual proof editors:

/* 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;
}

Complete Theme Examples

High Contrast Theme

.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

.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

.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

.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;
}

Built-in Dark Theme

Use the theme="dark" attribute:

<axiom-proof theme="dark" mode="sandbox"></axiom-proof>

Or apply programmatically:

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

Dynamic Theme Switching

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'
}

Responsive Styling

/* 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

Presets

| 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 |

Custom Rule Sets

<!-- Use a preset -->
<axiom-proof rules="propositional"></axiom-proof>

<!-- JSON array of specific rules -->
<axiom-proof rules='["PR", "Hyp", "∧I", "∧E", "→I", "→E"]'></axiom-proof>

<!-- Comma-separated (ASCII symbols work too) -->
<axiom-proof rules="PR, Hyp, /\I, /\E, ->I, ->E"></axiom-proof>

Available Rules

| 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

Modes

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

Configuration

<!-- Simple mode -->
<axiom-proof scoring="attempts"></axiom-proof>
<axiom-proof scoring="completion"></axiom-proof>
<axiom-proof scoring="none"></axiom-proof>

<!-- Full configuration -->
<axiom-proof scoring='{
  "mode": "attempts",
  "baseScore": 100,
  "attemptPenalty": 10,
  "maxPenalty": 50
}'></axiom-proof>

Scoring Parameters

| 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:

<axiom-proof
  scorm
  problem-id="lesson1-problem1"
  mode="exercise"
  premises='["P"]'
  goal="P ∨ Q"
></axiom-proof>

SCORM Features

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

Multiple Problems with SCORM

<axiom-proof scorm problem-id="q1" premises='["P"]' goal="P ∨ Q"></axiom-proof>
<axiom-proof scorm problem-id="q2" premises='["P ∧ Q"]' goal="Q"></axiom-proof>
<axiom-proof scorm problem-id="q3" premises='["P → Q", "P"]' goal="Q"></axiom-proof>

Symbol Input

Toolbar

Enable the symbol toolbar with show-toolbar:

<axiom-proof show-toolbar></axiom-proof>

Keyboard Auto-Conversion

Type ASCII sequences that auto-convert to Unicode symbols:

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

Rule Autocomplete

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

Proof Format

Each line follows the format:

<formula> :<rule> <citations>

Subproofs use leading pipe characters for indentation:

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

Citation Formats

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

Examples

Basic Modus Ponens

<axiom-proof
  mode="exercise"
  premises='["P", "P → Q"]'
  goal="Q"
  rules="propositional"
  show-toolbar
></axiom-proof>

Sandbox Mode

<axiom-proof
  mode="sandbox"
  rules="fol"
  show-toolbar
></axiom-proof>

Dark Theme with Custom Scoring

<axiom-proof
  mode="exercise"
  premises='["P ∧ Q"]'
  goal="Q ∧ P"
  theme="dark"
  scoring='{"mode": "attempts", "attemptPenalty": 5}'
></axiom-proof>

Custom Styled

<style>
  .my-proof {
    --axiom-syn-op: #e91e63;
    --axiom-syn-rule: #4caf50;
    --axiom-font-size: 16px;
    --axiom-radius: 0;
  }
</style>

<axiom-proof class="my-proof" mode="sandbox"></axiom-proof>

With Event Handling

<axiom-proof id="proof1" mode="exercise" premises='["P"]' goal="P ∨ Q"></axiom-proof>
<div id="status"></div>

<script>
  const proof = document.getElementById('proof1');
  const status = document.getElementById('status');

  proof.addEventListener('axiom:validate', (e) => {
    if (e.detail.isValid) {
      status.textContent = 'Valid so far...';
    } else {
      status.textContent = e.detail.issues[0] || 'Keep working...';
    }
  });

  proof.addEventListener('axiom:complete', (e) => {
    status.textContent = `Complete! Score: ${e.detail.score}`;
  });
</script>

TypeScript Support

Full TypeScript support with exported types:

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

Published

Vulnerabilities

Links

Maintainers

Keywords

Readme

axiom-embed

Features

Installation

npm

CDN / Script Tag

Building from Source

Build Outputs

Usage

UMD Bundle (Simplest)

ESM Module

With Bundlers (Vite, Webpack, etc.)

With React

Component API

<axiom-proof> Attributes

JavaScript API

Events

CSS Customization

CSS Custom Properties Reference

Styling Specific Instances

Complete Theme Examples

High Contrast Theme

Solarized Light Theme

Nord Theme

Monokai Theme

Built-in Dark Theme

Dynamic Theme Switching

Responsive Styling

Rule Sets

Presets

Custom Rule Sets

Available Rules

Scoring

Modes

Configuration

Scoring Parameters

SCORM Integration

SCORM Features

Multiple Problems with SCORM

Symbol Input

Toolbar

Keyboard Auto-Conversion

Rule Autocomplete

Proof Format

Citation Formats

Examples

Basic Modus Ponens

Sandbox Mode

Dark Theme with Custom Scoring

Custom Styled

With Event Handling

TypeScript Support

Browser Support

License

`<axiom-proof>` Attributes