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
External Solver Dependencies
Three external solvers are used for advanced reasoning capabilities:
Z3 SMT Solver - Install via pip:
ProbLog - Install via pip:
Clingo - Install via pip:
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
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
GitHub: https://github.com/quanticsoul4772