Prover9 와 Mace4 를 사용하여 자동화된 일차 논리 (first-order logic) 추론을 수행하는 MCP 서버입니다.
명제 증명- Prover9 로 논리적 명제를 증명합니다.모델 탐색- Mace4 로 유한 모델을 찾습니다.반례 찾기- 명제가 성립하지 않는 이유를 보여줍니다.문법 검증- 유용한 오류 메시지를 포함하여 공식을 사전에 검증합니다.분류론적 추론- 카테고리 이론 증명에 대한 내장 지원명제적 조건부- 빠른 명제적 검증을 위한 순수 분석형 HCC (Hypersequent Contingency Calculus) 증명기역추론- 변분 자유 에너지 (VFE, Variational Free Energy) 를 사용하여 가설을 순위화합니다.자율성- 모든 의존성이 자동으로 설치됩니다
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-app-config.json 파일).
Claude Desktop MCP 설정에 추가하세요 (생성된 claude-app-config.json 파일을 참조):
{
"mcpServers": {
"mcp-logic": {
...
중요: /absolute/path/to/mcp-logic 를 실제 저장소 경로로 교체하세요.
| 도구 | 목적 |
|---|
| prove | Prover9 를 사용하여 명제를 증명합니다. |
| check-well-formed | 상세한 오류 메시지를 포함하여 공식 문법을 검증합니다. |
| find_model | 전제 조건을 만족하는 유한 모델을 찾습니다. |
| find_counterexample | 명제가 성립하지 않는 반례를 찾습니다. |
| verify_commutativity | 카테고리 다이어그램의 교환법칙을 증명하기 위해 일차 논리 (FOL) 를 생성합니다. |
| get_category_axioms | 카테고리/함수사/군/모노이드에 대한 공리를 가져옵니다. |
| check_contingency | HCC 증명기를 사용하여 진리 기능적 조건부성을 확인합니다. |
| abductive_explain | 관찰에 대한 VFE 최소화 설명을 찾습니다. |
mcp-logic prove 도구를 사용하세요:
premises: ["all x (man(x) -> mortal(x))", "man(socrates)"]
conclusion: "mortal(socrates)"
결과: ✓ 명제가 증명되었습니다.
mcp-logic check_contingency 도구를 사용하세요:
formula: "(p -> q) | (q -> p)"
결과: 공식이 비조건부 **우연성 (tautology)**임을 식별하고, 증명 추적을 반환합니다.
mcp-logic find-counterexample 도구를 사용하세요:
premises: ["P(a)"]
conclusion: "P(b)"
결과: P(a) 가 참이지만 P(b) 가 거짓인 모델이 발견되어, 결론이 성립하지 않는다는 것을 증명합니다.
mcp-logic verify-commutativity 도구를 사용하세요:
path_a: ["f", "g"]
path_b: ["h"]
...
결과: f∘g = h 를 증명하기 위한 일차 논리 (FOL) 전제 조건과 결론을 생성합니다.
Claude Desktop 대신 서버를 직접 실행하세요:
Linux/macOS:
./run_mcp_logic.sh
Windows:
run_mcp_logic.bat
mcp-logic/
├── src/mcp_logic/
│ ├── server.py # 메인 MCP 서버 (8 개 도구)
...
인지 구조 개선 사항:
- ✅ 하이섹퀀스 조건부 계산법 (HCC, Hypersequent Contingency Calculus): 무작위 모델링 없이 일차 논리 공식의 조건부성을 즉시 평가하는 엄밀한 추론 검출기를 추가했습니다.
- ✅ 변분 자유 에너지 (VFE) 엔진: 오카姆의 날을 만족하기 위해 비독단적인 Cournot-Gaifman 선형식을 사용하여 가설을 순위화하는 역추론을 구현했습니다.
- ✅ 스마트 증명 라우팅:
prove 도구는 순수 명제적 쿼리를 HCC 엔진으로, 일차 논리 쿼리를 Prover9 로 자동으로 라우팅합니다.
- ✅ 설정 가능한 모델 찾기:
find_model 과 find_counterexample 는 이제 커스텀 타임아웃과 구조화된 술어/함수 추출을 지원합니다.
개선된 기능:
✅ Mace4 모델 찾기 및 반례 감지
✅ 위치별 오류를 포함한 상세 문법 검증
✅ 범주론 공리 및 교환 법칙 확인을 위한 카테고리적 추론 지원
✅ 모든 도구에서 구조화된 JSON 출력
✅ 자체 설치 (수동 경로 설정 불필요)
테스트 실행:
source .venv/bin/activate
pytest tests/ -v
테스트 컴포넌트 직접 실행:
python tests/test_enhancements.py
ENHANCEMENTS.md
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
하이퍼시퀀스 contingency 계산 (HCC): Eugenio Orlandelli, Giannandrea Pulcini, Achille C. Varzi (2024) 의 "A Hypersequent Calculus for Classical Contingencies" 논리 프레임워크를 기반으로 함.