MCP-Logic

Ein MCP-Server für automatisierte Logik erster Stufe unter Verwendung von Prover9 und Mace4.

Funktionen

• Theorembeweis - Beweisen Sie logische Aussagen mit Prover9

• Modellsuche - Finden Sie endliche Modelle mit Mace4

• Gegenbeispielsuche - Zeigen Sie, warum Aussagen nicht folgen

• Syntaxvalidierung - Vorab-Validierung von Formeln mit hilfreichen Fehlermeldungen

• Kategoriales Schließen - Integrierte Unterstützung für Beweise der Kategorientheorie

• Aussagenlogische Kontingenz - Rein analytischer HCC-Beweiser für schnelle aussagenlogische Prüfungen

• Abduktives Schließen - Rangfolge von Hypothesen mittels Variational Free Energy (VFE)

• In sich geschlossen - Alle Abhängigkeiten werden automatisch installiert

Related MCP server: warrant-mcp

Schnellstart

Installation

Linux/macOS:

git clone https://github.com/angrysky56/mcp-logic
cd mcp-logic
./linux-setup-script.sh

Windows:

git clone https://github.com/angrysky56/mcp-logic
cd mcp-logic
windows-setup-mcp-logic.bat

Das Setup-Skript führt automatisch folgende Schritte aus:

• Herunterladen und Erstellen von LADR (Prover9 + Mace4)

• Erstellen einer Python-virtuellen Umgebung

• Installation aller Abhängigkeiten

• Generierung der Claude Desktop-Konfiguration

Claude Desktop-Integration

Fügen Sie dies zu Ihrer Claude Desktop MCP-Konfiguration hinzu (automatisch generiert unter claude-app-config.json):

{
  "mcpServers": {
    "mcp-logic": {
      "command": "uv",
      "args": [
        "--directory",
        "/absolute/path/to/mcp-logic/src/mcp_logic",
        "run",
        "mcp_logic",
        "--prover-path",
        "/absolute/path/to/mcp-logic/ladr/bin"
      ]
    }
  }
}

Wichtig: Ersetzen Sie /absolute/path/to/mcp-logic durch Ihren tatsächlichen Repository-Pfad.

Verfügbare Tools

Beispielanwendung

Ein Theorem beweisen

Use the mcp-logic prove tool with:
premises: ["all x (man(x) -> mortal(x))", "man(socrates)"]
conclusion: "mortal(socrates)"

Ergebnis: ✓ THEOREM BEWIESEN

Aussagenlogische Kontingenz analysieren

Use the mcp-logic check_contingency tool with:
formula: "(p -> q) | (q -> p)"

Ergebnis: Identifiziert, dass die Formel eine nicht-kontingente Tautologie ist, und gibt den Beweisverlauf zurück.

Ein Gegenbeispiel finden

Use the mcp-logic find-counterexample tool with:
premises: ["P(a)"]
conclusion: "P(b)"

Ergebnis: Modell gefunden, in dem P(a) wahr, aber P(b) falsch ist, was beweist, dass die Schlussfolgerung nicht folgt.

Kategoriales Diagramm verifizieren

Use the mcp-logic verify-commutativity tool with:
path_a: ["f", "g"]
path_b: ["h"]
object_start: "A"
object_end: "C"

Ergebnis: FOL-Prämissen und Schlussfolgerung zum Beweis, dass f∘g = h.

Lokal ausführen

Anstatt Claude Desktop, führen Sie den Server direkt aus:

Linux/macOS:

./run_mcp_logic.sh

Windows:

run_mcp_logic.bat

Projektstruktur

mcp-logic/
├── src/mcp_logic/
│   ├── server.py              # Main MCP server (8 tools)
│   ├── mace4_wrapper.py       # Mace4 model finder
│   ├── syntax_validator.py    # Formula syntax validation
│   ├── categorical_helpers.py # Category theory utilities
│   ├── hcc_prover.py          # Hypersequent Contingency Calculus prover
│   ├── vfe_engine.py          # Variational Free Energy abductive engine
│   └── formula_ast.py         # Propositional logic AST and parser
├── ladr/                      # Auto-installed Prover9/Mace4 binaries
│   └── bin/
│       ├── prover9
│       └── mace4
├── tests/                     # Test suite
├── linux-setup-script.sh      # Linux/macOS setup
├── windows-setup-mcp-logic.bat # Windows setup
├── run_mcp_logic.sh           # Linux/macOS run script
└── run_mcp_logic.bat          # Windows run script

Was ist neu in v0.3.0

Verbesserungen der kognitiven Architektur:

• ✅ Hypersequent Contingency Calculus (HCC): Hinzufügen eines rigorosen deduktiven Prüfers zur sofortigen Bewertung von aussagenlogischen Formelkontingenzen ohne Brute-Force-Modellierung.

• ✅ Variational Free Energy (VFE) Engine: Implementierung abduktiven Schließens, das Hypothesen mittels eines nicht-dogmatischen Cournot-Gaifman-Priors einstuft, um Ockhams Rasiermesser elegant zu erfüllen.

• ✅ Intelligentes Beweiser-Routing: Das prove-Tool leitet rein aussagenlogische Abfragen automatisch an die HCC-Engine und Anfragen erster Stufe an Prover9 weiter.

• ✅ Konfigurierbare Modellsuche: find_model und find_counterexample unterstützen jetzt benutzerdefinierte Timeouts und die Extraktion strukturierter Prädikate/Funktionen.

Was ist neu in v0.2.0

Erweiterte Funktionen:

• ✅ Mace4-Modellsuche und Erkennung von Gegenbeispielen

• ✅ Detaillierte Syntaxvalidierung mit positionsbezogenen Fehlern

• ✅ Unterstützung für kategoriales Schließen (Axiome der Kategorientheorie, Verifizierung der Kommutativität)

• ✅ Strukturierte JSON-Ausgabe aller Tools

• ✅ In sich geschlossene Installation (keine manuelle Pfadkonfiguration)

Entwicklung

Tests ausführen:

source .venv/bin/activate
pytest tests/ -v

Komponenten direkt testen:

python tests/test_enhancements.py

Dokumentation

• ENHANCEMENTS.md - Kurze Referenz für v0.2.0-Funktionen

• Documents/ - Detaillierte Analyse und Beispiele

• walkthrough.md - Implementierungsdetails (in Artefakten)

Fehlerbehebung

Fehler "Prover9 not found":

• Führen Sie das Setup-Skript aus: ./linux-setup-script.sh oder windows-setup-mcp-logic.bat

• Überprüfen Sie, ob ladr/bin/prover9 und ladr/bin/mace4 existieren

Server aktualisiert nicht:

• Starten Sie den Server nach Codeänderungen neu

• Überprüfen Sie die Protokolle auf Syntaxfehler

Warnungen zur Syntaxvalidierung:

• Verwenden Sie Kleinbuchstaben für Prädikate/Funktionen (z. B. man(x) nicht Man(x))

• Setzen Sie zur besseren Lesbarkeit Leerzeichen um Operatoren

• Schließen Sie alle Klammern