# LOGICAFFEINE

> Debug your thoughts. Turn everyday English into rigorous First-Order Logic.

## What is LOGICAFFEINE?

LOGICAFFEINE is an English-to-First-Order-Logic transpiler and full programming language. It parses natural language sentences and outputs formal logic formulas in Unicode or LaTeX notation, and extends into a complete imperative language with CRDT-based distributed systems, formal verification, and more.

The tool helps users:
- Debug arguments and reasoning with formal logic
- Learn formal logic interactively through a gamified curriculum
- Prove logical structures with a pure-Rust, kernel-certified prover (runs in the browser, no Z3 required; Z3-backed static verification is available natively)
- Translate between natural language and formal notation
- Write full programs in English that compile to Rust/WASM and run at 2.5x the speed of C (2.544x geometric-mean speedup vs C, fastest in an 11-language benchmark suite — see /benchmarks)

## Key Features

### Natural Language to Logic
Parse English sentences into First-Order Logic (FOL). Handles 53+ linguistic phenomena including quantifiers, connectives, predicates, tense, aspect, modal logic, and more.

Example:
- Input: "All humans are mortal"
- Output: ∀x(Human(x) → Mortal(x))

### Multiple Output Formats
- Unicode symbols (∀, ∃, →, ∧, ∨, ¬)
- LaTeX notation (\forall, \exists, \rightarrow)
- Simple FOL representation

### Interactive Learning Platform
Progressive curriculum from basic syllogisms to advanced modal logic. Gamified with XP, streaks, achievements, and adaptive difficulty. Four eras covering 20+ modules.

### Studio Playground
Real-time translation with four modes:
- **Logic Mode**: English to FOL with AST visualization
- **Code Mode**: Imperative LOGOS programs with REPL and Rust codegen
- **Math Mode**: Vernacular theorem proving with tactic guidance
- **Hardware Mode**: English hardware specs to SystemVerilog Assertions (SVA + PSL + Rust monitors) with in-browser, Z3-free certified proving, BMC/k-induction, and counterexample waveforms

### Full Programming Language
LOGOS extends beyond logic into a complete language with:
- Functions, structs, enums, pattern matching
- Refinement types and generics
- Channels, actors, structured concurrency
- CRDTs for distributed systems
- Capability-based security with English policy blocks
- Curry-Howard proof assistant with Z3 verification

### Package Registry
Community-contributed logic modules and packages. GitHub OAuth for publishing.

## Main Pages

### / (Homepage)
Marketing landing page with interactive demos, feature highlights, and FAQ. Showcases Logic, Code, and Math modes with live examples.

### /studio
Interactive three-panel IDE:
- File browser with example files
- Live editor with syntax highlighting
- Context-sensitive output (FOL formulas, AST trees, REPL, proofs)
Free to use, no account required.

### /learn
Gamified curriculum for learning First-Order Logic:
- Era 1: First Steps (Introduction, Syllogistic Logic, Fallacies)
- Era 2: Building Blocks (Propositional Logic, Proofs)
- Era 3: Expanding Horizons (Quantificational, Modal, Deontic, Belief Logic)
- Era 4: Mastery (Ethics, Metalogic, History, Deviant Logic, Philosophy)
Features XP system, streaks, achievements, spaced repetition, and adaptive hints.

### /guide
Comprehensive documentation with 22 interactive sections covering:
- LOGICAFFEINE syntax and grammar
- Lexicon configuration
- First-Order Logic concepts
- Code examples with Run/Copy/Reset

### /pricing
Commercial licensing. Free for individuals and organizations under 25 employees. Paid tiers: Supporter ($5/mo), Pro ($10/mo), Premium ($25/mo), Enterprise (custom). Lifetime license available.

### /crates
Technical documentation for Rust crates:
- logicaffeine-base: Foundation types and utilities
- logicaffeine-lexicon: Vocabulary database with 2000+ entries
- logicaffeine-kernel: Dependent type theory proof kernel
- logicaffeine-data: Content and curriculum engine
- logicaffeine-system: Platform abstraction (VFS, persistence)
- logicaffeine-language: Parser, transpiler, and compiler
- logicaffeine-proof: Backward chaining proof engine
- logicaffeine-compile: Full compilation pipeline

### /roadmap
Development roadmap with 9 milestones:
1. Core Transpiler (Complete) - 53+ linguistic phenomena
2. Web Platform (Complete) - Interactive learning and studio
3. Imperative Language (Complete) - Functions, structs, enums, I/O
4. Type System (Complete) - Refinement types, generics, inference
5. Concurrency & Actors (Complete) - Channels, agents, async/await
6. Distributed Systems (Complete) - CRDTs, P2P, conflict resolution
7. Security & Policies (Complete) - Capability-based security
8. Proof Assistant (Complete) - Curry-Howard, Z3 verification
9. Universal Compilation (In Progress) - WASM target, Live Codex IDE

### /benchmarks
Live benchmark results with full methodology: 32 programs across 11 languages (C, C++, Rust, Zig, Go, Java, JavaScript, Python, Ruby, Nim, LOGOS), the certified-solver-vs-the-field comparison (Z3, Kissat, SaDiCaL, CaDiCaL, CryptoMiniSat), and the wire-codec head-to-head (Protobuf, Cap'n Proto, MessagePack, bincode, postcard, CBOR, Arrow, JSON). Every number links to raw JSON and reproducible harnesses.

### /registry
Package registry for community-contributed logic modules. Search, browse, and publish packages with GitHub authentication.

### /news
Release notes, tutorials, and announcements — one article per release with engineering deep-dives (each article is statically served at /news/<slug>; the full list is in /sitemap.xml).

### /profile
User profile with XP, level, streaks, module progress, and achievements.

### /privacy
Privacy policy.

### /terms
Terms of service. Business Source License (BUSL-1.1).

## Technical Details

### Supported Logic Systems
- Classical propositional logic
- First-order predicate logic
- Modal logic (necessity, possibility)
- Deontic logic (obligation, permission)
- Epistemic logic (belief, knowledge)
- Temporal logic (past, future, always)

### Architecture
- **Frontend**: Dioxus 0.7 (Rust) compiled to WebAssembly; content pages are statically prerendered for crawlers
- **Backend**: Rust with arena-allocated AST, symbol interning
- **Logic pipeline**: Input → Lexer → Parser → AST → Transpiler → FOL Output
- **Imperative pipeline**: five execution tiers — tree-walking interpreter, register bytecode VM, copy-and-patch JIT, AOT-to-Rust, and a direct WASM backend
- **Proof Engine**: pure-Rust certified prover (SAT/CDCL, GF(2)/GF(p) algebraic routes, SR symmetry proofs) checked by a CoC proof kernel; Z3 powers the optional native static-verification tier

### Performance
Measured by the open benchmark suite (32 programs x 11 languages, results at /benchmarks):
- LOGOS release binaries: 2.544x geometric-mean speedup vs C — faster than Rust (1.21x), Zig (1.157x), and C++ (1.033x) on the same suite
- The certified solver beats Z3, Kissat, CaDiCaL, and CryptoMiniSat by orders of magnitude on structured UNSAT families (pigeonhole, Tseitin parity, mod-p counting)
- The wire codec produces the smallest encoding on every fair workload vs Protobuf, Cap'n Proto, MessagePack, bincode, postcard, and CBOR

### Lexicon System
Vocabulary database (lexicon.json) defining:
- Verbs with Vendler class and transitivity
- Nouns with animacy, gender, and number
- Adjectives with intersective/subsective properties
- 2000+ vocabulary entries

## Links

- Website: https://logicaffeine.com
- GitHub: https://github.com/Brahmastra-Labs/logicaffeine
- X (Twitter): https://x.com/logicaffeine
- Documentation: https://logicaffeine.com/guide
- API Crates: https://logicaffeine.com/crates
- Studio: https://logicaffeine.com/studio
- Learn: https://logicaffeine.com/learn
- Benchmarks: https://logicaffeine.com/benchmarks
- News: https://logicaffeine.com/news
- All indexable pages: https://logicaffeine.com/sitemap.xml

## Contact

- Email: tristen@brahmastra-labs.com
- Support: https://logicaffeine.com/pricing
- Discord: https://discord.gg/logicaffeine

## Full documentation in one file

The complete curriculum — quickguide, every topical guide, and the error
catalog — is served as one file for LLM ingestion at /llms-full.txt.
Machine-readable companions: /errors.json (every diagnostic code with its
Socratic explanation) and /examples.json (the runtime-verified example
corpus with expected outputs). The toolchain itself is an MCP server:
`claude mcp add logos -- largo mcp`.

## Organization

LOGICAFFEINE is developed by Datacenter.Dev.

## License

Business Source License 1.1 (BUSL-1.1). Free for individuals and organizations under 25 employees. Commercial licenses available at https://logicaffeine.com/pricing.

---

This file is optimized for AI search engines and LLM indexing. For human-readable documentation, visit https://logicaffeine.com/guide