MCP-Logic

MCP-сервер для автоматизированного рассуждения в логике первого порядка с использованием Prover9 и Mace4.

Возможности

• Доказательство теорем — доказательство логических утверждений с помощью Prover9

• Поиск моделей — поиск конечных моделей с помощью Mace4

• Поиск контрпримеров — демонстрация того, почему утверждения не следуют из посылок

• Проверка синтаксиса — предварительная проверка формул с полезными сообщениями об ошибках

• Категориальное рассуждение — встроенная поддержка доказательств в теории категорий

• Пропозициональная контингентность — чисто аналитический HCC-проверщик для быстрой проверки высказываний

• Абдуктивное рассуждение — ранжирование гипотез с использованием вариационной свободной энергии (VFE)

• Автономность — все зависимости устанавливаются автоматически

Related MCP server: warrant-mcp

Быстрый старт

Установка

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

Скрипт установки автоматически:

• Скачивает и собирает LADR (Prover9 + Mace4)

• Создает виртуальное окружение Python

• Устанавливает все зависимости

• Генерирует конфигурацию для Claude Desktop

Интеграция с Claude Desktop

Добавьте в конфигурацию MCP для Claude Desktop (автоматически генерируется в 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"
      ]
    }
  }
}

Важно: Замените /absolute/path/to/mcp-logic на ваш фактический путь к репозиторию.

Доступные инструменты

Примеры использования

Доказательство теоремы

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

Результат: ✓ ТЕОРЕМА ДОКАЗАНА

Анализ пропозициональной контингентности

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

Результат: Определяет, что формула является неконтингентной тавтологией, возвращая трассировку доказательства.

Поиск контрпримера

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

Результат: Найдена модель, где P(a) истинно, а P(b) ложно, что доказывает, что вывод не следует из посылок.

Верификация категориальной диаграммы

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

Результат: Посылки и вывод в логике первого порядка для доказательства того, что f∘g = h.

Локальный запуск

Вместо Claude Desktop можно запустить сервер напрямую:

Linux/macOS:

./run_mcp_logic.sh

Windows:

run_mcp_logic.bat

Структура проекта

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

Что нового в версии v0.3.0

Улучшения когнитивной архитектуры:

• ✅ Исчисление гиперсеквентной контингентности (HCC): Добавлен строгий дедуктивный проверщик для мгновенной оценки контингентности пропозициональных формул без перебора моделей.

• ✅ Движок вариационной свободной энергии (VFE): Реализовано абдуктивное рассуждение, которое ранжирует гипотезы с использованием априорного распределения Курно-Гайфмана для элегантного соблюдения бритвы Оккама.

• ✅ Умная маршрутизация доказательств: Инструмент prove автоматически направляет чисто пропозициональные запросы в движок HCC, а запросы первого порядка — в Prover9.

• ✅ Настраиваемый поиск моделей: find_model и find_counterexample теперь поддерживают пользовательские тайм-ауты и структурированное извлечение предикатов/функций.

Что нового в версии v0.2.0

Расширенные возможности:

• ✅ Поиск моделей и обнаружение контрпримеров с помощью Mace4

• ✅ Подробная проверка синтаксиса с указанием позиции ошибки

• ✅ Поддержка категориальных рассуждений (аксиомы теории категорий, верификация коммутативности)

• ✅ Структурированный вывод JSON для всех инструментов

• ✅ Автономная установка (без ручной настройки путей)

Разработка

Запуск тестов:

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

Тестирование компонентов напрямую:

python tests/test_enhancements.py

Документация

• ENHANCEMENTS.md — Краткий справочник по функциям v0.2.0

• Documents/ — Подробный анализ и примеры

• walkthrough.md — Детали реализации (в артефактах)

Устранение неполадок

Ошибка "Prover9 not found":

• Запустите скрипт установки: ./linux-setup-script.sh или windows-setup-mcp-logic.bat

• Убедитесь, что ladr/bin/prover9 и ladr/bin/mace4 существуют

Сервер не обновляется:

• Перезапустите сервер после внесения изменений в код

• Проверьте логи на наличие синтаксических ошибок

Предупреждения о проверке синтаксиса:

• Используйте строчные буквы для предикатов/функций (например, man(x), а не Man(x))

• Для ясности добавляйте пробелы вокруг операторов

• Проверяйте баланс всех скобок

Лицензия

MIT

Авторы

• Prover9/Mace4: Библиотека LADR Уильяма Маккьюна

• Репозиторий LADR: laitep/ladr

• Исчисление гиперсеквентной контингентности (HCC): Основано на логической структуре из работы "A Hypersequent Calculus for Classical Contingencies" Эудженио Орланделли, Джаннандреа Пульчини и Акилле К. Варци (2024).