Logic-Thinking MCP Server

# CLAUDE.md This file provides guidance to Claude Code (claude.ai/code) when working with code in this repository. ## Project Overview This is an MCP (Model Context Protocol) server that provides formal logical reasoning, verification, and proof construction capabilities. It supports 11 logic systems (8 internal + 3 external) and operates via JSON-RPC 2.0 over stdin/stdout. **Version:** 0.4.0 ## Build & Test Commands - Build: `npm run build` (compiles TypeScript and copies Python bridge scripts) - Watch mode: `npm run watch` - Start server: `npm run start` - Run all tests: `npm test` - Run specific test: `npm test -- -t "test name pattern"` - Watch tests: `npm test:watch` - Lint: `npm run lint` Note: The start command uses Node.js memory flags: `--max-old-space-size=4096 --expose-gc --max-semi-space-size=64` ### External Dependencies Three Python packages required for external solvers: - `pip install z3-solver` - SMT constraint solving - `pip install problog` - Probabilistic reasoning - `pip install clingo` - Answer set programming The server uses pyenv Python (`/Users/russellsmith/.pyenv/shims/python3`) by default, falling back to system Python. ## Architecture ### Core Components **Entry Point:** `src/index.ts` - Handles JSON-RPC 2.0 communication via stdin/stdout - Implements MCP protocol (initialize, tools/list, tools/call) - Routes to `LogicManager` for logic operations **Logic Manager:** `src/logicManager.ts` - Central router for all logic operations - Auto-detects logical systems from input (see `detectSystem()` methods) - Implements performance caching via `logicCache` - Routes to one of 11 system implementations in `src/systems/` **Command Handler:** `src/commandHandler.ts` - Processes special commands (help, listSystems, cacheStats, etc.) - Contains extensive help content and examples for all systems/operations **Advanced Features:** - Proof Library (`src/proofLibrary.ts`): SQLite database with FTS5 search, lemmas, usage tracking - Assumption Extractor (`src/assumptionExtractor.ts`): Detects 6 types of hidden assumptions with confidence scoring - Argument Scorer (`src/argumentScorer.ts`): 6-component scoring system (0-100 with A-F grades) - Batch Processor (`src/batchProcessor.ts`): Concurrent/sequential execution with 50-request safety limit - Logic Translator (`src/logicTranslator.ts`): Cross-system translation with lossiness tracking - Contradiction Detector (`src/contradictionDetector.ts`): Multi-level contradiction detection with severity levels ### Logic System Implementations All systems extend from `src/systems/base.ts` and implement: - `process(operation, input, format)` method - Four core operations: `validate`, `formalize`, `visualize`, `solve` **Internal Systems** (8): 1. `syllogistic.ts` - Term-based categorical reasoning 2. `propositional.ts` - Truth-functional reasoning 3. `predicate.ts` - Quantified statements (first-order logic) 4. `mathematical.ts` - Arithmetic, sequences, patterns 5. `modal.ts` - Necessity and possibility (K, T, S4, S5 systems) 6. `temporal.ts` - Time-based reasoning (G, F, X, U operators) 7. `fuzzy.ts` - Degrees of truth with membership functions 8. `deontic.ts` - Obligations and permissions **External Systems** (3): 9. `smt.ts` - Constraint solving via Z3 (subprocess to `z3Solver.py`) 10. `probabilistic.ts` - Probabilistic reasoning via ProbLog (subprocess to `problogBridge.py`) 11. `asp.ts` - Answer set programming via Clingo (subprocess to `clingoIntegration.ts`) ### Supporting Modules **Parsers** (`src/parsers/`): - Each system has dedicated parser (e.g., `propositionalParser.ts`, `aspParser.ts`) - Handle both natural language and symbolic notation - External system parsers: `constraintParser.ts` (Z3), `probabilisticParser.ts` (ProbLog), `aspParser.ts` (Clingo) **Validators** (`src/validators/`): - Validate logical arguments for correctness - Detect fallacies and provide counterexamples - `modalValidator.ts` - Kripke semantics with bounded model checking **Visualizers** (`src/systems/visualization/`): - Generate visual representations (truth tables, Venn diagrams, Kripke frames, etc.) - Each system has specialized visualizers including `smt/`, `probabilistic/`, `asp/` **Proof Generation** (`src/proof/`): - Natural deduction proof generators - Support for syllogistic, propositional, predicate, modal systems - `modalProofGenerator.ts` - System-specific axiom applications (K, T, D, B, 4, 5) **External Solver Integration:** - `src/systems/smt/z3Integration.ts` - Spawns Python subprocess, sends JSON via stdin, receives results via stdout - `src/systems/probabilistic/problogIntegration.ts` - Manages persistent Python process, line-buffered JSON communication - `src/systems/asp/clingoIntegration.ts` - Direct Clingo execution via TypeScript **Logging:** - Use Winston logger (`src/utils/logger.ts`) for all logging - NEVER use `console.log/error/warn` as it interferes with MCP JSON-RPC protocol on stdout/stderr - Logger instances: `Loggers.manager`, `Loggers.smt`, `Loggers.probabilistic`, `Loggers.asp` ## Key Type Definitions Located in `src/types.ts`: - `LogicalSystem` - Union type of 11 systems + 'auto' - `Operation` - 'validate' | 'formalize' | 'visualize' | 'solve' - `LogicResult` - Standard result interface with status, message, details - System-specific types: `PropositionalFormula`, `ModalFormula`, `SMTConstraint`, `ProbabilisticProgram`, `ASPProgram` - Feature types: `SavedProof`, `Lemma`, `ProofSearchOptions`, `ExtractedAssumption`, `ArgumentScore` ## System Detection Logic The `LogicManager` can auto-detect systems from input (see `detectSystem()` in `src/logicManager.ts`): 1. First tries NLP processing via `NaturalLanguageProcessor` 2. Falls back to pattern matching (quantifiers, operators, mathematical symbols) 3. Defaults to propositional logic if uncertain Key detection patterns: - **ASP**: "answer set", "stable model", "choice rule", "find all", "typically", "unless", `{...}` syntax, `:- ` rules - **Probabilistic**: "probability", "likely", "uncertain", "belief", `P(X|Y)` notation, `0.7::fact` syntax, "% chance" - **SMT**: "constraint", "satisf", "optimize", "maximize", "minimize", "subject to", "find...where" - **Mathematical**: number sequences, arithmetic operators, "sequence", "pattern" - **Modal**: box, diamond, "necessary", "possible" - **Temporal**: G, F, X, U, "always", "eventually" - **Fuzzy**: "very", "somewhat", membership degrees - **Deontic**: O, P, F operators, "obligatory", "permitted" - **Predicate**: for-all, exists, predicates like P(x) - **Syllogistic**: "All", "Some", "No" without quantifier symbols ## Code Style - 2-space indentation - ES modules (use .js in imports) - TypeScript strict mode - Explicit return types required - JSDoc comments for public methods - Naming: snake_case files, camelCase variables/functions, PascalCase classes/interfaces ## Error Handling Located in `src/errorHandler.ts`: - Use `createCommandError()`, `createUnsupportedOperationError()` helpers - Provide suggestions and examples with errors - Try/catch blocks with detailed error messages ## Performance - Caching implemented via `src/utils/cache.ts` (node-cache) - Cache key based on: system + operation + input + format + additionalContext - Use `cacheStats` command to monitor performance - Only successful results are cached - Modal logic uses bounded model checking (prevents combinatorial explosion) ## Testing - Jest with ts-jest preset - ES modules configuration in `jest.config.js` - Test files should use `.test.ts` extension - Run specific tests: `npm test -- -t "pattern"` - External solver tests: `src/systems/smt.test.ts`, `src/systems/asp.test.ts`, `src/systems/probabilistic/problogIntegration.test.ts` ## Important Notes **Console Output:** - NEVER use `console.log`, `console.error`, or `console.warn` in the codebase - These write to stdout/stderr which interferes with MCP JSON-RPC protocol - Always use Winston logger: `import { Loggers } from './utils/logger.js'` - Example: `logger.debug('message', { context })` instead of `console.log('message')` **Python Subprocess Communication:** - External solvers communicate via JSON over stdin/stdout - Z3: Single request/response per subprocess spawn - ProbLog: Persistent process with line-buffered JSON (one request per line) - Clingo: Direct execution via subprocess **Build Process:** - TypeScript compiles `src/` to `dist/` - Python scripts copied from `src/systems/*/` to `dist/systems/*/` via `copy-python` script - Both TypeScript and Python files must exist in `dist/` for external solvers to work