Core Concepts
CLP 문제를 SMT-LIB 형식으로 효과적으로 변환하는 방법을 제시한다.
Abstract
이 논문은 CLP(Constraint Logic Programming) 문제를 SMT-LIB 형식으로 변환하는 방법을 제안한다. CLP는 Prolog 언어를 기반으로 하며, 제약 프로그래밍과 논리 프로그래밍의 장점을 결합한다. 한편 SMT-LIB은 다양한 배경 이론을 지원하는 논리 공식 표현 언어로, CHC(Constrained Horn Clauses) 솔버의 표준 입력 형식이다.
논문에서는 Prolog의 주요 특징인 함수, 리스트, 정수 산술을 SMT-LIB으로 모델링하는 방법을 제시한다. 먼저 Prolog 용어를 나타내기 위해 대수적 데이터 타입 U를 정의한다. 이후 Prolog 사실, 규칙, 리스트, 정수 산술 제약을 SMT-LIB 명령어로 변환하는 규칙을 제시한다.
마지막으로 도시 간 경로 찾기 예제를 SMT-LIB으로 인코딩하는 과정을 보여준다. 이를 통해 제안된 변환 방식의 실효성을 확인할 수 있다. 향후 연구 방향으로는 Prolog 의미론을 더 정확히 반영하는 변환 방식, 다양한 배경 이론 지원, CHC 솔버와 CLP 엔진의 성능 비교 등이 있다.
Stats
도시 간 직접 거리:
테헤란-비엔나: 31
비엔나-파리: 10
비엔나-뮌헨: 3
파리-뮌헨: 10
파리-로마: 11
로잔-로마: 6
로잔-뮌헨: 4
테헤란-파리: 42