MCP-Logic

Fornece raciocínio automatizado para sistemas de IA usando os provadores de teoremas Prover9 e Mace4.

Documentação

MCP-Logic

Um servidor MCP para raciocínio automatizado em lógica de primeira ordem usando Prover9, Mace4 e um LLM de raciocínio integrado.

Recursos

Prova de Teoremas - Prove declarações lógicas com Prover9
Busca de Modelos - Encontre modelos finitos com Mace4
Busca de Contrarrelógios - Mostre por que declarações não são consequências
Validação de Sintaxe - Pré-valide fórmulas com mensagens de erro úteis
Raciocínio Categórico - Suporte integrado para provas em teoria das categorias
Contingência Proposicional - Provador HCC puramente analítico para verificações proposicionais rápidas
Raciocínio Abdutivo - Classifique hipóteses usando Energia Livre Variacional (VFE)
🤖 Consultor de Lógica (NOVO) - LLM de raciocínio TwIL-LM3 integrado que resolve problemas de lógica de ponta a ponta: basta fazer uma pergunta em inglês simples
Autocontido - Todas as dependências são instaladas automaticamente

Início Rápido

Instalação

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

O script de configuração automaticamente:

Baixa e compila LADR (Prover9 + Mace4)
Cria ambiente virtual Python
Instala todas as dependências
Gera configuração do Claude Desktop

Habilitar o Consultor de Lógica (Opcional)

O consultor de lógica integrado usa um LLM local de 3B parâmetros (TwIL-LM3 Q8) para resolver problemas de lógica de ponta a ponta. Execute o script de configuração para instalá-lo:

Linux/macOS:

./setup-advisor.sh

Windows:

setup-advisor.bat

O script automaticamente:

Detecta sua GPU — CUDA em NVIDIA (Linux/Windows), Metal em Apple Silicon (macOS), ou usa CPU como fallback
Compila llama-cpp-python com o backend de aceleração correto
Baixa o modelo (~3,3 GB, uma única vez) para ~/.cache/mcp-logic/models/

Sem necessidade de ativar o venv — os scripts de configuração usam uv que gerencia o ambiente virtual automaticamente. Todos os comandos uv run e uv pip install --directory têm como alvo o .venv do projeto sem que você precise ativá-lo primeiro.

Instalação Manual (Avançado)

Se você preferir instalar manualmente em vez de usar o script de configuração:

Linux (GPU NVIDIA):

CMAKE_ARGS="-DGGML_CUDA=on" uv pip install --directory . "llama-cpp-python>=0.3.0"
uv pip install --directory . "huggingface-hub>=0.24.0"

macOS (Apple Silicon):

CMAKE_ARGS="-DGGML_METAL=on" uv pip install --directory . "llama-cpp-python>=0.3.0"
uv pip install --directory . "huggingface-hub>=0.24.0"

Windows (GPU NVIDIA, PowerShell):

$env:CMAKE_ARGS="-DGGML_CUDA=on"
uv pip install --directory . "llama-cpp-python>=0.3.0"
uv pip install --directory . "huggingface-hub>=0.24.0"

Somente CPU (qualquer plataforma):

uv pip install --directory . "llama-cpp-python>=0.3.0"
uv pip install --directory . "huggingface-hub>=0.24.0"

O modelo é baixado automaticamente no primeiro uso, ou você pode baixá-lo manualmente:

uv run --directory . python -c "
from huggingface_hub import hf_hub_download
hf_hub_download('webAI-Official/TwIL-LM3', 'TwIL-LM3-Q8_0.gguf',
                revision='5d90f3a3251e142fc5cc6b42a62b175fdb0d4ccd',
                local_dir='$HOME/.cache/mcp-logic/models',
                local_dir_use_symlinks=False)
"

Compatibilidade de Plataforma

Plataforma	Aceleração de GPU	Observações
Linux (x86_64)	✅ CUDA (NVIDIA)	Requer CUDA Toolkit + `nvidia-smi`
macOS (Apple Silicon)	✅ Metal	Python ARM64 nativo recomendado
macOS (Intel)	⚠️ Metal (limitado)	Funciona, mas mais lento que Apple Silicon
Windows (x86_64)	✅ CUDA (NVIDIA)	Requer CUDA Toolkit + Visual Studio Build Tools
Qualquer plataforma	✅ CPU	Sempre funciona, mais lento (~10-20s por consulta para modelo 3B)

Integração com Claude Desktop

Adicione à sua configuração MCP do Claude Desktop (gerada automaticamente em claude-app-config.json):

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

Importante: Substitua /absolute/path/to/mcp-logic pelo caminho real do seu repositório.

Adicione "--no-advisor" para testes determinísticos somente com solvers ou quando as dependências opcionais do consultor não estiverem instaladas. O modelo é carregado de forma preguiçosa, então chamadas normais de prove e find_model não consomem memória GPU.

Integração com Codex

Registre o servidor stdio globalmente com caminhos absolutos:

codex mcp add mcp-logic -- \
  /absolute/path/to/mcp-logic/.venv/bin/mcp_logic \
  --prover-path /absolute/path/to/mcp-logic/ladr/bin

Confirme o comando salvo com codex mcp get mcp-logic. Reinicie o Codex após adicionar ou alterar o servidor para que suas ferramentas sejam carregadas na próxima sessão.

Ferramentas Disponíveis

Ferramenta	Propósito
ask_logic_advisor 🤖	Resolva problemas de lógica em inglês simples (ponta a ponta)
prove	Prove declarações usando Prover9
check_well_formed	Valide a sintaxe de fórmulas com erros detalhados
find_model	Encontre modelos finitos que satisfaçam as premissas
find_counterexample	Encontre contrarrelógios mostrando que declarações não são consequências
verify_commutativity	Gere FOL para comutatividade de diagramas categóricos
get_category_axioms	Obtenha axiomas para categoria/funtor/grupo/monoide
check_contingency	Verifique contingência verofuncional via provador HCC
abductive_explain	Encontre a explicação que minimiza VFE para uma observação

Exemplo de Uso

Pergunte ao Consultor de Lógica (Mais Fácil)

Basta fazer uma pergunta em linguagem natural — o consultor formaliza, executa o solver e explica o resultado:

Use ask_logic_advisor with:
question: "Is it true that if all humans are mortal and Socrates is human,
           then Socrates is mortal?"

Resultado: O consultor traduz para FOL, prova o teorema com Prover9 e retorna:

"Sim, Sócrates é mortal. A prova segue da premissa universal de que todos os humanos são mortais, combinada com o fato de que Sócrates é humano."

A resposta também inclui a formalização usada e a saída bruta do solver para transparência.

Prove um Teorema (Direto)

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

Resultado: ✓ TEOREMA PROVADO

Analise Contingência Proposicional

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

Resultado: Identifica que a fórmula é uma tautologia não contingente, retornando o rastro da prova.

Encontre um Contrarrelógio

Use the find_counterexample tool with:
premises: ["P(a)"]
conclusion: "P(b)"

Resultado: Modelo encontrado onde P(a) é verdadeiro mas P(b) é falso, provando que a conclusão não é consequência.

Verifique Diagrama Categórico

Use the verify_commutativity tool with:
path_a: ["f", "g"]
path_b: ["h"]
object_start: "A"
object_end: "C"

Resultado: Premissas e conclusão em FOL para provar que f∘g = h.

Executando Localmente

Em vez do Claude Desktop, execute o servidor diretamente:

Linux/macOS:

./run_mcp_logic.sh

Windows:

run_mcp_logic.bat

Estrutura do Projeto

mcp-logic/
├── src/mcp_logic/
│   ├── server.py              # Main MCP server (9 tools)
│   ├── logic_advisor.py       # Onboard TwIL-LM3 agentic solver
│   ├── 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
│   └── fol_ast.py             # First-order AST, parser, and transformations
├── ladr/                      # Auto-installed Prover9/Mace4 binaries
│   └── bin/
│       ├── prover9
│       └── mace4
├── tests/                     # Unit, solver integration, and MCP stdio tests
├── linux-setup-script.sh      # Linux/macOS core setup
├── windows-setup-mcp-logic.bat # Windows core setup
├── setup-advisor.sh           # Linux/macOS advisor setup
├── setup-advisor.bat          # Windows advisor setup
├── run_mcp_logic.sh           # Linux/macOS run script
└── run_mcp_logic.bat          # Windows run script

Detalhes do Consultor de Lógica

A ferramenta ask_logic_advisor usa um pipeline agêntico de 3 fases:

  Natural Language Question
         │
         ▼
  ┌─────────────────────┐
  │ 1. FORMALIZE        │  TwIL-LM3 translates to FOL
  │    (LLM call)       │  → {"tool":"prove", "premises":[...], ...}
  └────────┬────────────┘
           ▼
  ┌─────────────────────┐
  │ 2. EXECUTE          │  Runs actual Prover9/Mace4/HCC
  │    (Solver call)    │  → {"result":"proved", "proof":...}
  └────────┬────────────┘
           ▼
  ┌─────────────────────┐
  │ 3. INTERPRET        │  TwIL-LM3 explains the result
  │    (LLM call)       │  → Plain English answer
  └─────────────────────┘

Modelo: TwIL-LM3 (3B parâmetros, ajustado para raciocínio formal)
Quantização: Q8_0 GGUF (~3,3 GB em disco, ~3,5 GB VRAM)
Carregamento preguiçoso: O modelo é carregado na primeira consulta, não na inicialização do servidor
Licença: webAI Non-Commercial License v1.0 (somente uso não comercial)

Requisitos de Recursos

Cenário	VRAM	Velocidade de Inferência
GPU NVIDIA (CUDA)	~3,5 GB	~1-3s por chamada LLM
Apple Silicon (Metal)	~3,5 GB	~2-5s por chamada LLM
Somente CPU	0 (usa RAM)	~10-20s por chamada LLM

Novidades na v0.4.0

Consultor de Lógica Integrado:

✅ Ferramenta ask_logic_advisor: Resolva problemas de lógica em inglês simples — o LLM TwIL-LM3 integrado formaliza, executa o solver e interpreta resultados automaticamente
✅ Configuração de GPU multiplataforma: Detecta automaticamente CUDA (NVIDIA) ou Metal (Apple Silicon) e compila de acordo
✅ Carregamento preguiçoso do modelo: Sem uso de VRAM até que o consultor seja chamado pela primeira vez
✅ Download automático: O modelo é baixado do HuggingFace no primeiro uso

Novidades na v0.3.0

Melhorias na Arquitetura Cognitiva:

✅ Cálculo de Contingência por Hipersequentes (HCC): Adicionado um verificador dedutivo rigoroso para avaliar contingências de fórmulas proposicionais instantaneamente, sem modelagem por força bruta.
✅ Motor de Energia Livre Variacional (VFE): Implementado raciocínio abdutivo que classifica hipóteses usando um prior Cournot-Gaifman não dogmático para satisfazer elegantemente a Navalha de Ockham.
✅ Roteamento Inteligente de Provadores: A ferramenta prove roteia automaticamente consultas proposicionais puras para o motor HCC e consultas de primeira ordem para o Prover9.
✅ Buscador de Modelos Configurável: find_model e find_counterexample agora suportam timeouts personalizados e extração estruturada de predicados/funções.
✅ Busca em Fragmentos Decidíveis: Teorias BSR e monádicas limitadas com segurança recebem uma busca completa de 1..model_bound. Uma resposta de no_model_found é absoluta somente com um status de PROVED ou REFUTED licenciado pelo contexto; uma resposta de BOUNDED_NO_MODEL mantém a ressalva de limite finito.
✅ Roteamento do Consultor Ciente da Teoria: A seleção do solver segue a estrutura da fórmula analisada, incluindo aritmética mista e predicados não interpretados, em vez de correspondência de palavras-chave em inglês.
✅ Lint de Escopo de Variáveis: check_well_formed avisa sobre quantificação universal implícita e ligadores não usados, sem rejeitar fórmulas Prover9 legais.

Novidades na v0.2.0

Recursos Aprimorados:

✅ Busca de modelos e detecção de contrarrelógios com Mace4
✅ Validação de sintaxe detalhada com erros específicos de posição
✅ Suporte a raciocínio categórico (axiomas de teoria das categorias, verificação de comutatividade)
✅ Saída JSON estruturada de todas as ferramentas
✅ Instalação autocontida (sem configuração manual de caminhos)

Desenvolvimento

As fixtures de teste descobrem automaticamente o ladr/bin/prover9 e ladr/bin/mace4 incluídos; nenhum LADR_PATH é necessário para um checkout normal.

Execute a suíte completa:

.venv/bin/python -m pytest tests/ -q

Execute apenas o teste MCP stdio de ponta a ponta, que inicia o servidor e exercita tanto Prover9 quanto Mace4 por meio de chamadas de ferramentas MCP:

.venv/bin/python -m pytest tests/test_mcp_stdio_integration.py -q

Sandboxes de processo restritos podem permitir que os binários LADR iniciem enquanto impedem que eles progridam, produzindo timeouts enganosos de 30/60 segundos. Execute testes baseados em solver fora desse sandbox; não compense aumentando o timeout do solver.

Documentação

mcp_logic_agent.md - Guia do agente (referência de ferramentas + fluxos de trabalho)
ENHANCEMENTS.md - Referência rápida para recursos da v0.2.0
Documents/ - Análise detalhada e exemplos

Solução de Problemas

Erro "Prover9 not found":

Execute o script de configuração: ./linux-setup-script.sh ou windows-setup-mcp-logic.bat
Verifique se ladr/bin/prover9 e ladr/bin/mace4 existem

Consultor de lógica não funciona:

Execute a configuração do consultor: ./setup-advisor.sh ou setup-advisor.bat
Verifique a detecção de GPU: nvidia-smi (Linux/Windows) ou system_profiler SPDisplaysDataType (macOS)
Force o modo CPU: ./setup-advisor.sh --cpu
Verifique se o modelo existe: ls ~/.cache/mcp-logic/models/TwIL-LM3-Q8_0.gguf
Desative se não for necessário: adicione --no-advisor aos argumentos do servidor

Falha na compilação de "llama-cpp-python":

Linux: Instale ferramentas de compilação: sudo apt-get install build-essential cmake
macOS: Instale ferramentas Xcode: xcode-select --install
Windows: Instale Visual Studio Build Tools com a carga de trabalho "Desktop development with C++"
CUDA: Certifique-se de que o CUDA Toolkit esteja instalado e nvcc esteja no PATH

Servidor não atualiza:

Reinicie o servidor após alterações de código
Verifique os logs para erros de sintaxe

Avisos de validação de sintaxe:

Use minúsculas para predicados/funções (por exemplo, man(x) não Man(x))
Adicione espaços ao redor dos operadores para clareza
Equilibre todos os parênteses

Licença

MIT (servidor mcp-logic)

Nota: O modelo TwIL-LM3 usado pelo consultor de lógica é licenciado sob a webAI Non-Commercial License v1.0. Isso restringe o recurso do consultor a uso não comercial. O servidor mcp-logic principal (prove, find_model, etc.) permanece licenciado sob MIT e pode ser usado comercialmente sem o consultor.

Créditos

Prover9/Mace4: Biblioteca LADR de William McCune
Repositório LADR: laitep/ladr
TwIL-LM3: webAI — modelo de raciocínio de 3B ajustado para lógica formal
Cálculo de Contingência por Hipersequentes (HCC): Baseado em "A Hypersequent Calculus for Classical Contingencies" de Eugenio Orlandelli, Giannandrea Pulcini e Achille C. Varzi (2024).