MCP-Logic

Prover9 및 Mace4를 사용하는 자동 1차 논리 추론을 위한 MCP 서버입니다.

기능

• 정리 증명 - 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 통합

Claude Desktop MCP 설정(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임을 증명하기 위한 FOL 전제 및 결론.

로컬 실행

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) 엔진: 오컴의 면도날을 우아하게 만족시키기 위해 비독단적인 Cournot-Gaifman 사전 확률을 사용하여 가설 순위를 매기는 가추적 추론 구현.

• ✅ 스마트 증명기 라우팅: prove 도구가 순수 명제 쿼리는 HCC 엔진으로, 1차 논리 쿼리는 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: William McCune의 LADR 라이브러리

• LADR 저장소: laitep/ladr

• 초순차 우연성 계산(HCC): Eugenio Orlandelli, Giannandrea Pulcini, Achille C. Varzi(2024)의 "A Hypersequent Calculus for Classical Contingencies" 논리 프레임워크 기반.