Prover9 와 Mace4 를 사용한 자동화 일차 논리 추론을 위한 MCP 서버

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

• 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

하이퍼시퀀스 contingency 계산 (HCC): Eugenio Orlandelli, Giannandrea Pulcini, Achille C. Varzi (2024) 의 "A Hypersequent Calculus for Classical Contingencies" 논리 프레임워크를 기반으로 함.