Skip to main content
Glama

MCP-Logic

MIT License
20
  • Linux
  • Apple

MCP-로직

AI 시스템에 Prover9/Mace4를 사용하여 자동 추론 기능을 제공하는 MCP 서버입니다. 이 서버는 깔끔한 MCP 인터페이스를 통해 논리 정리 증명 및 논리 모델 검증을 지원합니다.

디자인 철학

MCP-Logic은 Prover9/Mace4에 대한 강력한 인터페이스를 제공하여 AI 시스템과 형식 논리 간의 간극을 메웁니다. MCP-Logic의 특별한 점은 다음과 같습니다.

  • AI 우선 설계 : AI 시스템이 자동 추론을 수행하도록 특별히 제작됨
  • 지식 검증 : 지식 표현과 논리적 의미에 대한 공식적인 검증을 가능하게 합니다.
  • 깔끔한 통합 : MCP(Model Context Protocol) 생태계와의 원활한 통합
  • 심층 추론 : 중첩된 양화사와 다중 전제를 사용한 복잡한 논리적 증명 지원
  • 실제 세계 응용 프로그램 : 특히 AI 지식 모델 및 추론 체인을 검증하는 데 유용합니다.

특징

  • 자동화된 정리 증명을 위한 Prover9와의 원활한 통합
  • 복잡한 논리 공식 및 증명 지원
  • 내장된 구문 검증
  • MCP 서버 인터페이스 정리
  • 광범위한 오류 처리 및 로깅
  • AI 시스템에 대한 지식 표현 및 추론 지원

빠른 예

영상

지엑스피1

영상

설치

필수 조건

  • 파이썬 3.10+
  • UV 패키지 관리자
  • 저장소 복제를 위한 Git
  • CMake 및 빌드 도구(LADR/Prover9 빌드용)

설정

이 저장소를 복제하세요

git clone https://github.com/angrysky56/mcp-logic cd mcp-logic

설치 스크립트를 실행합니다. Windows 실행:

windows-setup-mcp-logic.bat

리눅스/macOS:

chmod +x linux-setup-script.sh ./linux-setup-script.sh

설정 스크립트:

  • 종속성 확인(git, cmake, 빌드 도구)
  • 외부 저장소 laitep/LADR 에서 LADR(Prover9/Mace4)을 다운로드합니다.
  • ladr/bin 디렉토리에 Prover9 바이너리를 생성하기 위해 LADR 라이브러리를 빌드합니다.
  • Python 가상 환경을 생성합니다
  • Docker를 사용하거나 사용하지 않고 실행하기 위한 구성 파일을 설정합니다.

중요: LADR 디렉토리는 저장소 자체에 포함되지 않으며 설치 스크립트나 수동으로 설치됩니다.

Docker 사용 - 이것이 제대로 작동하는지 알 수 없음, 주로 Claude Desktop과 직접 사용하도록 설계됨

Docker로 실행하려면 다음 스크립트를 사용하세요.

  • 사용 가능한 포트를 찾습니다
  • 가상 환경을 활성화합니다
  • 설치된 Prover9에 대한 올바른 경로로 서버를 실행합니다.
# Linux/macOS ./run-mcp-logic.sh
# Windows run-mcp-logic.bat

이 스크립트는 필요한 환경으로 Docker 컨테이너를 빌드하고 실행합니다.

Claude 데스크톱 통합

Claude Desktop과 함께 MCP-Logic을 사용하려면 다음 구성을 사용하세요.

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

"/path/to/mcp-logic"를 실제 저장소 경로로 바꾸세요.

사용 가능한 도구

영상

입증하다

Prover9를 사용하여 논리적 증명을 실행합니다.

{ "tool": "prove", "arguments": { "premises": [ "all x (man(x) -> mortal(x))", "man(socrates)" ], "conclusion": "mortal(socrates)" } }

잘 형성된 체크

논리적 문장 구문 검증:

{ "tool": "check-well-formed", "arguments": { "statements": [ "all x (man(x) -> mortal(x))", "man(socrates)" ] } }

선적 서류 비치

자세한 분석과 예시는 문서 폴더를 참조하세요.

프로젝트 구조

mcp-logic/ ├── src/ │ └── mcp_logic/ │ └── server.py # Main MCP server implementation ├── tests/ │ ├── test_proofs.py # Core functionality tests │ └── test_debug.py # Debug utilities ├── Documents/ # Analysis and documentation ├── pyproject.toml # Python package config ├── setup-script.sh # Setup script (installs LADR & dependencies) ├── run-mcp-logic.sh # Docker-based run script (Linux/macOS) ├── run-mcp-logic.bat # Docker-based run script (Windows) ├── run-mcp-logic-local.sh # Local run script (no Docker) └── README.md # This file

참고: setup-script.sh를 실행한 후 Prover9 바이너리를 포함하는 "ladr" 디렉토리가 생성되지만, 이 디렉토리는 저장소 자체에 포함되지 않습니다.

개발

테스트 실행:

uv pip install pytest uv run pytest

특허

MIT

-
security - not tested
A
license - permissive license
-
quality - not tested

hybrid server

The server is able to function both locally and remotely, depending on the configuration or use case.

MCP-Logic은 AI 시스템에 자동 추론 기능을 제공하는 서버로, 깔끔한 MCP 인터페이스를 통해 Prover9/Mace4를 사용하여 논리적 정리 증명과 모델 검증을 가능하게 합니다.

  1. 디자인 철학
    1. 특징
      1. 빠른 예
        1. 설치
          1. 필수 조건
          2. 설정
          3. Docker 사용 - 이것이 제대로 작동하는지 알 수 없음, 주로 Claude Desktop과 직접 사용하도록 설계됨
          4. Claude 데스크톱 통합
        2. 사용 가능한 도구
          1. 입증하다
          2. 잘 형성된 체크
        3. 선적 서류 비치
          1. 프로젝트 구조
            1. 개발
              1. 특허

                Related MCP Servers

                • A
                  security
                  F
                  license
                  A
                  quality
                  Provides reasoning content to MCP-enabled AI clients by interfacing with Deepseek's API or a local Ollama server, enabling focused reasoning and thought process visualization.
                  Last updated -
                  1
                  54
                  24
                  JavaScript
                • -
                  security
                  A
                  license
                  -
                  quality
                  A minimal MCP Server that provides Claude AI models with the 'think' tool capability, enabling better performance on complex reasoning tasks by allowing the model to pause during response generation for additional thinking steps.
                  Last updated -
                  525
                  1
                  TypeScript
                  MIT License
                  • Apple
                • -
                  security
                  F
                  license
                  -
                  quality
                  An MCP server that allows AI assistants to programmatically manage Unleash feature flags through natural language, enabling operations like creating, updating, and retrieving feature flags across projects.
                  Last updated -
                  5
                  2
                  TypeScript
                • -
                  security
                  -
                  license
                  -
                  quality
                  An MCP server that provides a "think" tool enabling structured reasoning for AI agents, allowing them to pause and record explicit thoughts during complex tasks or multi-step tool use.
                  Last updated -
                  1
                  Python
                  MIT License

                View all related MCP servers

                MCP directory API

                We provide all the information about MCP servers via our MCP API.

                curl -X GET 'https://glama.ai/api/mcp/v1/servers/angrysky56/mcp-logic'

                If you have feedback or need assistance with the MCP directory API, please join our Discord server