Logic-Thinking MCP Server
Model Context Protocol server for formal logical reasoning, mathematical problem-solving, verification, and proof construction.
Features
- 11 logic systems: Syllogistic, Propositional, Predicate, Mathematical, Modal, Temporal, Fuzzy, Deontic, SMT, Probabilistic, ASP
- External solver integration: Z3 for constraint solving, ProbLog for probabilistic reasoning, Clingo for answer set programming
- Proof library with persistent storage and full-text search
- Assumption extraction for detecting hidden assumptions
- Argument scoring with detailed analysis
- Batch processing for multiple concurrent requests
- Cross-system translation between logic systems
- Contradiction detection
- Automatic system detection from input
- Natural language processing with enhanced parsers
- Visualizations: truth tables, Venn diagrams, Kripke frames, parse trees
Installation
git clone https://github.com/quanticsoul4772/logic-thinking.git
cd logic-thinking
npm install
npm run build
External Solver Dependencies
Three external solvers are used for advanced reasoning capabilities:
- Z3 SMT Solver - Install via pip:
pip install z3-solver
- ProbLog - Install via pip:
pip install problog
- Clingo - Install via pip:
pip install clingo
The server will attempt to use Python from pyenv if available, otherwise falling back to system Python. Ensure your Python environment has these packages installed.
Claude Desktop Integration
Add to your Claude Desktop configuration file:
macOS: ~/Library/Application Support/Claude/claude_desktop_config.json
{
"mcpServers": {
"logic-thinking": {
"command": "node",
"args": [
"--max-old-space-size=4096",
"--expose-gc",
"--max-semi-space-size=64",
"/absolute/path/to/logic-thinking/dist/index.js"
]
}
}
}
MCP Tools
The server provides 10 tools:
- logic-thinking - Core operations (validate, formalize, visualize, solve, score)
- logic-batch - Batch processing
- logic-translate - Cross-system translation
- logic-contradiction - Detect contradictions
- logic-proof-save - Save proofs
- logic-proof-search - Search proofs
- logic-proof-get - Retrieve proof by ID
- logic-proof-list - List proofs
- logic-proof-stats - Library statistics
- logic-extract-assumptions - Extract assumptions
Logic Systems
Syllogistic Logic
Traditional Aristotelian categorical logic.
Propositional Logic
Truth-functional reasoning with logical connectives.
Predicate Logic
First-order logic with quantified statements.
Mathematical Logic
Equation solving, sequence detection, pattern recognition.
Modal Logic
Necessity and possibility with Kripke semantics. Systems: K, T, D, B, K4, KB, S4, S5, KD45
Temporal Logic
Time-based reasoning about sequences and processes.
Fuzzy Logic
Reasoning with degrees of truth and linguistic hedges.
Deontic Logic
Normative reasoning about obligations and permissions.
SMT Logic
Constraint satisfaction and optimization using Z3 theorem prover. Supports integer, real, boolean, and bitvector variables with optimization objectives.
Probabilistic Logic
Probabilistic reasoning using ProbLog. Supports probabilistic facts, rules, evidence-based inference, and probability queries.
ASP (Answer Set Programming)
Non-monotonic reasoning using Clingo. Supports choice rules, constraints, optimization, default reasoning, and stable model enumeration.
License
MIT License - see LICENSE file for details
Author
quanticsoul4772