Skip to main content
Glama

MCP-Logic

MIT License
32
  • 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
                  A
                  license
                  A
                  quality
                  A sophisticated MCP server that provides a multi-dimensional, adaptive reasoning framework for AI assistants, replacing linear reasoning with a graph-based architecture for more nuanced cognitive processes.
                  Last updated -
                  1
                  8
                  27
                  MIT License
                  • Apple
                  • Linux
                • A
                  security
                  A
                  license
                  A
                  quality
                  A Model Context Protocol (MCP) server implementation for the Didlogic API. This server allows Large Language Models (LLMs) to interact with Didlogic services through a standardized interface.
                  Last updated -
                  22
                  1
                  MIT License
                • -
                  security
                  F
                  license
                  -
                  quality
                  An advanced MCP server that implements sophisticated sequential thinking using a coordinated team of specialized AI agents (Planner, Researcher, Analyzer, Critic, Synthesizer) to deeply analyze problems and provide high-quality, structured reasoning.
                  Last updated -
                  246
                  • Linux
                  • Apple
                • A
                  security
                  F
                  license
                  A
                  quality
                  An intelligent MCP server that orchestrates multiple MCP servers with AI-enhanced workflow automation and production-ready context engine capabilities for codebase analysis.
                  Last updated -
                  3

                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