Chaos and Order

💡 왼쪽 원문을 읽으면서 오른쪽에 따라 써보세요. Tab 키로 힌트를 받을 수 있습니다.

원문 렌더가 준비되기 전까지 텍스트 가이드로 표시합니다.

들어가며 — 2026년 5월, 왜 다시 로직 프로그래밍인가

"Prolog는 1972년 언어다. 21세기에 왜 다시 보는가." 5년 전이라면 합리적인 의문이었다. 그러나 2026년 봄, 로직 프로그래밍은 세 갈래에서 동시에 부활하고 있다. 첫째, LLM 에이전트가 "기호적으로 검증 가능한 추론(symbolic reasoning)"을 요구하면서 Prolog와 ASP가 다시 백엔드 추론기로 호출되고 있다. 둘째, Souffle Datalog가 GitHub CodeQL과 Meta 정적 분석 파이프라인을 거치며 산업 표준급 정적 분석 엔진으로 자리잡았다. 셋째, Rocq(전 Coq)와 Lean 4가 수학·검증 분야에서 폭발적으로 채용되며 "정리 증명기 = 함수형 + 의존타입 로직 언어"라는 시야가 일반화됐다.

이 글은 마케팅 문서가 아니다. 2026년 5월 시점에서 실제로 살아 움직이는 로직 프로그래밍 도구를 가족 단위로 묶고, 어디에 쓰이고, 어디에서 멈췄는지를 적는다.

로직 프로그래밍의 4가지 큰 가족

비교에 앞서 큰 그림이 필요하다. 로직 프로그래밍은 한 언어가 아니라 네 가족의 합집합이다.

1. **Prolog 가족** — Horn 절(Horn clause) 위에 SLD 해소(SLD resolution)와 백트래킹을 얹은 고전 패러다임. SWI-Prolog · Scryer · Trealla · Tau · Mercury · ECLiPSe가 여기 속한다.

2. **Datalog 가족** — Prolog의 비결정성과 함수기호를 떼어내 종료성과 효율을 얻은 변종. Souffle · DDlog · CozoDB · Datomic · XTDB가 대표 주자.

3. **ASP(Answer Set Programming)** — 안정 모델 시맨틱스(stable model semantics) 위에서 모든 가능한 해를 열거한다. Clingo · DLV · WASP가 사실상 전부다.

4. **관계형 임베디드 언어** — miniKanren / core.logic / microKanren처럼 호스트 언어(Scheme · Clojure · Racket) 안에 박힌 관계형 DSL.

여기에 정리 증명기(Coq · Lean · Isabelle · Agda · F\*)는 "프로그램 = 증명"이라는 커리-하워드 동형사상을 통해 로직 프로그래밍과 깊게 연결된다. 본 글은 5번째 줄기로 묶어 다룬다.

한눈에 보기 — 2026년 5월 로직 프로그래밍 라인업

| 가족 | 대표 도구 | 라이선스 | 1차 강점 |

| --- | --- | --- | --- |

| ASP | Clingo | MIT | 사실상 ASP 표준 |

| ASP | DLV | 학술 | 분리 논리(disjunctive) |

| 증명기 | Isabelle/HOL | BSD | seL4 검증 · ML 기반 |

| 증명기 | Agda | MIT | 의존타입 학술 |

| 증명기 | F\* | Apache 2.0 | MS Research · 검증 |

| 제약 | MiniZinc | MPL | 모델링 표준 |

| 제약 | Choco-solver | BSD-4 | Java 제약 |

| 제약 | Gecode | MIT | C++ 제약 |

| SAT/SMT | Z3 | MIT | 사실상 SMT 표준 |

| SAT/SMT | CVC5 | BSD | 학술 SMT |

각 도구는 마케팅 페이지가 아니라 2026년 5월 현재의 GitHub README와 ICLP/JICSLP 발표 노트에서 정리했다.

SWI-Prolog 9.x — 사실상의 표준 Prolog

SWI-Prolog는 1986년 Jan Wielemaker가 시작한 네덜란드의 오픈소스 Prolog로, 2026년 시점 9.x 라인이 안정판이다. 라이선스는 BSD-2로 풀려 있고, 웹 서버 라이브러리(`http_server/2`), 제약 논리(CLP(FD), CLP(R)), SSL, JSON, 유니코드, 스레드, 모듈, ODBC를 모두 표준 배포로 제공한다.

전형적인 SWI-Prolog 8/9 스타일은 다음과 같다.

:- use_module(library(clpfd)).

% N-Queens 문제

queens(N, Qs) :-

length(Qs, N),

Qs ins 1..N,

all_distinct(Qs),

safe_queens(Qs).

safe_queens([]).

safe_queens([Q|Qs]) :-

safe_queens(Qs, Q, 1),

safe_queens(Qs).

safe_queens([], _, _).

safe_queens([Q|Qs], Q0, D0) :-

Q0 #\= Q,

abs(Q0 - Q) #\= D0,

D1 #= D0 + 1,

safe_queens(Qs, Q0, D1).

SWI는 "표준 ISO Prolog + 실용 라이브러리" 비율에서 가장 균형이 좋다. 한국·일본 대학 강의의 8할은 SWI를 가정한다.

Scryer Prolog — 모던 ISO Prolog, Rust로 다시 쓰다

Scryer는 Mark Thom이 시작한 ISO 표준 Prolog 구현이다. Rust로 작성됐고, ISO 호환성과 클린한 구현을 목표한다. SWI가 "실용성 우선"이라면 Scryer는 "정확성 우선"이다. 2026년 5월 시점 0.9.x 라인이 활발히 개발 중이고, 도서 "The Power of Prolog"(Markus Triska)의 코드가 Scryer로 검증된다.

특히 Scryer는 attribute variables, CLP(B/Z/FD)를 표준 배포로 포함하며, Triska의 매니패스토대로 "side-effect 최소 · 순수 Prolog 권장" 노선을 따른다.

Trealla Prolog — C로 쓴 임베디드 Prolog

Trealla(Andrew Davison)는 MIT 라이선스 C 구현으로, 단일 바이너리가 작고 임베디드 시스템에 박기 좋다. WebAssembly 빌드도 안정적이라 Tau와 함께 "브라우저용 Prolog" 옵션이다.

Tau Prolog — 순수 JS Prolog

Tau Prolog는 José Antonio Riaza가 만든 순수 JavaScript Prolog 구현이다. Node.js · 브라우저 어디서나 동작하고, DOM API를 Prolog 술어로 노출한다. 교육용 데모와 정적 사이트 기반 추론 위젯에 인기다.

const pl = require('tau-prolog')

const session = pl.create()

session.consult(`

parent(tom, bob).

parent(bob, alice).

grandparent(X, Z) :- parent(X, Y), parent(Y, Z).

session.query('grandparent(tom, Who).')

session.answer((answer) => {

console.log(pl.format_answer(answer))

})

GNU Prolog · SICStus · ECLiPSe — 옛 거인들

- **GNU Prolog**: Daniel Diaz가 1996년 시작한 GPL Prolog. 컴파일 결과를 네이티브 바이너리로 떨어뜨릴 수 있고 finite-domain 제약 솔버가 포함돼 있다.

- **SICStus Prolog**: 스웨덴 SICS에서 시작한 상용 Prolog. Mats Carlsson이 주도하며, 항공·물류·통신 산업의 미션 크리티컬 시스템에 들어가 있다. 라이선스는 상용.

- **ECLiPSe**: IC-Parc(임페리얼 칼리지)에서 만든 제약 논리 프로그래밍 시스템. MPL 라이선스로 풀려 있고, CHR(Constraint Handling Rules)의 실험판이 가장 정교하다.

Mercury — 강타입 · 모드 시스템 Prolog의 후예

Mercury는 호주 멜버른 대학의 Zoltan Somogyi가 1990년대에 시작한 언어로, "Prolog의 선언적 의미는 좋은데, 부작용과 모드가 흐트러져 큰 시스템에 못 쓴다"는 비판에 답하려 했다. Mercury는 다음을 강제한다.

- **모드(mode) 선언**: 인자가 `in` 또는 `out`인지 명시.

- **결정성(determinism) 선언**: `det` / `semidet` / `multi` / `nondet`.

- **타입 클래스**: Haskell 스타일.

- **순수성**: I/O는 `io` 상태 변수로만.

:- module hello.

:- interface.

:- import_module io.

:- pred main(io::di, io::uo) is det.

:- implementation.

main(!IO) :-

io.write_string("Hello, Mercury!\n", !IO).

대규모 프로그램 정적 분석과 컴파일러 백엔드 분야에서 살아남았고, ICFP/ICLP에서 꾸준히 발표된다.

Datalog 가족 — 종료성을 얻은 Prolog의 사촌

Datalog는 함수 기호를 빼고 절을 평탄하게 만든 Prolog의 부분집합이다. 그 결과 평가가 종료되고, bottom-up semi-naive evaluation으로 효율적인 평가가 가능하다. 2026년 5월 시점, Datalog는 세 갈래 가족으로 굳었다.

- **정적 분석용 Datalog**: Souffle, Doop

- **증분 Datalog**: DDlog

- **임베디드 Datalog DB**: CozoDB, Datomic, XTDB

Souffle — 정적 분석의 표준 Datalog

Souffle(Sydney 대학에서 시작)는 Datalog 프로그램을 C++로 컴파일해 멀티스레드로 평가한다. 핵심 사용처는 정적 프로그램 분석으로, Doop(자바 포인터 분석), CodeQL의 학술적 친척, 보안 컨설팅 회사의 내부 분석 파이프라인 등에 들어가 있다.

.decl edge(x:number, y:number)

.decl path(x:number, y:number)

.input edge

.output path

path(X, Y) :- edge(X, Y).

path(X, Y) :- edge(X, Z), path(Z, Y).

2026년 시점 2.5.x 안정판이 GitHub에서 활발히 유지된다. UPL(Universal Permissive License) 1.0으로 풀려 있어 상업 사용도 자유롭다.

DDlog · CozoDB · Datomic · XTDB

- **DDlog**: VMware Research가 시작한 증분 Datalog. 입력이 바뀌면 변경된 결과만 재계산. 네트워크 컨트롤 플레인 검증에 쓰였다.

- **CozoDB**: 중국에서 시작한 오픈소스 Datalog 데이터베이스. Rust 임베디드, 시계열·그래프·임베딩 검색을 Datalog 질의로 통합한다.

- **Datomic / XTDB**: Clojure 생태계의 시간 인식 데이터베이스. 질의 언어가 Datalog의 변종이다. 별도 Clojure 글에서 깊게 다뤘다.

Answer Set Programming — Clingo의 시대

ASP는 안정 모델 시맨틱스(stable model semantics)를 토대로 한 비결정성 로직 프로그래밍이다. Prolog가 한 해를 찾는 반면 ASP는 모든 해(answer set)를 열거하고, 그 위에 가중치·최적화·집계를 얹는다.

2026년 5월 시점 ASP의 사실상 표준 시스템은 독일 포츠담 대학의 **Clingo**다. Roland Kaminski · Torsten Schaub · Martin Gebser 팀이 주도하며 5.7.x 라인이 안정판이다. MIT 라이선스로 풀려 있다.

% 그래프 색칠 문제: 3가지 색으로 인접 정점을 다르게.

node(1..5).

edge(1,2). edge(2,3). edge(3,4). edge(4,5). edge(5,1).

color(red). color(green). color(blue).

1 { assign(N, C) : color(C) } 1 :- node(N).

:- edge(X, Y), assign(X, C), assign(Y, C).

#show assign/2.

ASP의 대안 시스템으로는 이탈리아의 **DLV**(분리 논리 지원), 호주의 **WASP**가 있다. Clingo는 최적화 ASP, ASP-Core-2 표준 준수, Python API(`clingo` 패키지), gringo+clasp 분리 빌드까지 가장 두텁다.

산업 적용 사례는 스케줄링(병원 근무표, 항공기 배정), 결정 지원 시스템, 시스템 구성(Linux 패키지 의존성 해소 — SUSE Open Build Service 등)이 대표적이다.

miniKanren — 호스트 언어에 박힌 관계형 DSL

miniKanren은 인디애나 대학교의 Daniel Friedman, William Byrd가 시작한 작은 관계형 프로그래밍 언어다. 5개 핵심 연산(`==`, `fresh`, `conde`, `run`, `run*`)만으로 Prolog 류의 관계형 추론을 지원하고, 호스트 언어(Scheme · Racket · Clojure · Python · JavaScript)에 임베드된다.

"The Reasoned Schemer"(MIT Press, 3판 2018)가 표준 교재이고, microKanren은 약 39줄 Scheme로 짠 더 작은 코어다.

(run* (q)

(fresh (a b)

(== `(,a ,b) q)

(conde

((== a 'apple) (== b 'pie))

((== a 'banana) (== b 'split)))))

;; => ((apple pie) (banana split))

Clojure 진영의 **core.logic**(David Nolen)은 miniKanren을 Clojure로 포팅한 라이브러리로 클로저 표준 라이브러리에 가까운 위상을 가진다.

Flora-2 — F-Logic의 살아있는 구현체

Flora-2는 Michael Kifer가 주도한 F-Logic 구현체로, "객체 지향 + 로직" 패러다임을 한 언어 안에서 통합한다. HiLog · 트랜잭션 로직 · 의무 논리(deontic logic) 확장까지 지원한다. 학술적 시맨틱 웹 추론과 정책 표현에서 살아남았고, 2026년 시점에도 ErgoAI(Coherent Knowledge가 만든 상용 후신)로 명맥을 잇는다.

정리 증명기 — Rocq · Lean 4 · Isabelle · Agda · F\*

증명 보조기는 로직 프로그래밍의 형제 분야다. 2024년 6월 Coq는 INRIA 발표로 공식 명칭을 **Rocq**로 바꿨고, 9.0이 그 첫 메이저 릴리스다. 의존타입과 Gallina 명세 언어, 머신 검증된 수학(CompCert 컴파일러, Four Color Theorem)을 모두 Rocq가 떠받친다.

**Lean 4**는 Microsoft Research를 떠난 Leonardo de Moura가 이끄는 의존타입 함수형 + 메타프로그래밍 언어다. Mathlib4가 2024-2025년 사이 100만 줄을 넘기며 사실상 가장 큰 머신 검증된 수학 라이브러리가 됐다. 2026년 봄 시점 Terence Tao의 일부 연구가 Lean으로 형식화되는 등 학계 전이가 가속화됐다.

**Isabelle/HOL**은 케임브리지 · 뮌헨공대 라인의 고전적 증명 보조기로, seL4 마이크로커널의 기능 정확성 증명을 떠받쳤다. Standard ML 기반이며 BSD 라이선스다.

**Agda**(채머스 대학)는 의존타입 함수형 언어이자 증명기로, 의존타입 강의의 표준 교재 언어다. **F\***(F-star, MS Research)는 의존정제(refinement) 타입과 효과 시스템으로 분산 시스템·암호 프로토콜 검증에 쓰인다. **HOL Light**(John Harrison)와 **HOL4**(케임브리지 라인)는 더 미니멀한 HOL 구현체로 학술 검증과 표준 라이브러리 검증에 쓰인다.

-- Lean 4 — 자연수 덧셈의 교환법칙

theorem add_comm : ∀ (m n : Nat), m + n = n + m := by

intro m n

induction m with

| zero => simp

| succ m ih => simp [Nat.succ_add, ih]

Idris · Idris 2 · Cedille — 의존타입의 차세대

**Idris**(Edwin Brady, 세인트앤드루스)는 Haskell 친화적 문법의 의존타입 함수형 언어다. Idris 2는 코어를 Quantitative Type Theory로 재설계해 선형성을 1급 시민으로 만들었다. **Cedille**(Aaron Stump, Iowa)는 보다 미니멀한 의존타입 코어 언어 연구 프로젝트로, 학술 영향력이 크다.

제약 프로그래밍 — MiniZinc · OR-Tools · Choco · Gecode

로직 프로그래밍의 형제로 제약 프로그래밍(CP) 분야가 있다. 2026년 시점 가장 활발한 도구는 다음과 같다.

- **MiniZinc**: 뉴질랜드 모나시 라인이 만든 제약 모델링 표준 언어. 모델을 Gecode, Chuffed, OR-Tools 등 다양한 솔버로 보낼 수 있다.

- **OR-Tools**: 구글이 만든 C++/Python 제약·LP·라우팅 라이브러리. CP-SAT 솔버는 사실상 산업 표준이다.

- **Choco-solver**: 프랑스 IMT 아틀란틱이 주도하는 Java 제약 솔버. BSD-4.

- **Gecode**: 스웨덴 KTH·독일 잘란트 라인의 C++ 제약 솔버. MIT.

% MiniZinc — N-Queens

int: n = 8;

array[1..n] of var 1..n: q;

constraint forall (i, j in 1..n where i < j) (

q[i] != q[j] /\

q[i] + i != q[j] + j /\

q[i] - i != q[j] - j

);

solve satisfy;

SAT/SMT 솔버 — Z3 · CVC5 · CaDiCaL · MiniSat

기호 추론의 엔진은 SAT(불 만족성)과 SMT(이론을 더한 SAT) 솔버다. 2026년 시점 라인업.

- **Z3**(Microsoft Research): Leonardo de Moura · Nikolaj Bjørner. 사실상 SMT 표준. MIT.

- **CVC5**(스탠포드 · 아이오와): Z3의 학술 대안. BSD.

- **Yices**(SRI International): 산업·연구 양쪽에서 쓰이는 SMT 솔버.

- **MiniSat / Glucose**: 학술 SAT 솔버의 고전.

- **Lingeling / CaDiCaL**: Armin Biere가 주도한 SAT 솔버. CaDiCaL이 최근 SAT 컴페티션 상위권 단골이다.

Z3는 Python 바인딩(`z3-solver`)이 평균적이며, 대부분의 LLM 에이전트가 "외부 SMT 검증"을 호출할 때 Z3를 가정한다.

확률 로직 프로그래밍 — PRISM · ProbLog · Pyro · Stan · PyMC

확률 로직은 로직 프로그래밍에 확률 분포를 더한 줄기다. **PRISM**(David Poole · 사토 다이스케 라인)과 **ProbLog**(KU Leuven, Luc De Raedt 라인)가 대표 학술 시스템이다. 산업 채택은 Bayesian 진영의 **Stan**(Andrew Gelman), **PyMC**(Python), **Pyro**(Uber AI Labs, PyTorch 기반)가 더 두텁다.

지식 그래프 + 시맨틱 웹 — Neo4j · GraphDB · Stardog · TerminusDB · TigerGraph

로직 프로그래밍의 자매 분야로 지식 그래프(KG)가 있다. 2026년 시점 주요 시스템.

- **Neo4j**: 사실상 그래프 DB 표준. Cypher 질의 언어.

- **GraphDB**(Ontotext): RDF/SPARQL 시맨틱 추론.

- **AllegroGraph**(Franz Inc): Lisp 기반 RDF 트리플 스토어.

- **Stardog**: SPARQL + SHACL + 추론. 상용.

- **TerminusDB**: Prolog로 짠 오픈소스 그래프 DB. Datalog 변종 WOQL.

- **TigerGraph**: 고성능 그래프 DB. GSQL 질의.

RDF/SPARQL/OWL 스택은 W3C 표준으로 RDF 1.2가 2025년 권고됐다. 시맨틱 웹의 약속이 식어들었어도, 의약·생명과학 데이터 통합과 정부 데이터 카탈로그는 여전히 RDF로 굴러간다.

산업 적용 사례 — Watson · CodeQL · seL4 · 패키지 해소

마케팅이 아닌 실제 배포 사례 몇 가지.

- **IBM Watson**: 2011년 제퍼디 챔피언으로 등장한 Watson은 백엔드에 Prolog를 썼다(IBM의 공식 발표). 자연어 분석 파이프라인의 일부였다.

- **GitHub CodeQL**: 인수합병 전 Semmle이 만든 학술적 친척 SemmleQL은 Datalog 영감을 받은 질의 언어다. 2026년 시점 CodeQL은 GitHub 보안 분석의 핵심.

- **seL4**: 정밀 마이크로커널의 기능 정확성 증명을 Isabelle/HOL로 마쳤다(2014, 이후 보강).

- **SUSE / openSUSE 패키지 의존성**: libsolv가 SAT 솔버로 해소를 수행. ASP가 학술적 대안으로 자주 비교된다.

- **Erlang 기원**: 에릭손의 Joe Armstrong 회고록에 따르면, Erlang 초기 프로토타입은 Prolog로 작성됐다. 그래서 패턴 매칭과 단일 할당이 Prolog 향이다.

LLM 시대의 로직 프로그래밍 — Neuro-Symbolic의 부활

2025-2026년의 큰 그림은 "LLM이 못 하는 검증을 로직 시스템에 외주"하는 흐름이다. 패턴은 세 가지다.

1. **LLM → Z3**: 자연어 제약을 LLM이 Z3 식으로 변환 → 솔버가 검증. OpenAI · Anthropic의 추론 모델이 내부적으로 SMT/SAT 호출을 학습하는 보고가 누적.

2. **LLM → Prolog/ASP**: 자연어 규칙을 ASP 인코딩으로 변환 → Clingo가 답 집합을 열거. 일정 짜기, 시스템 구성, 법무 추론.

3. **Neuro-symbolic 미세조정**: DeepMind의 Pearl Lab 발표 등, LLM에 미니 Prolog 인터프리터를 임베드해 multi-step 추론을 향상시키는 라인.

한국의 로직 프로그래밍 — KAIST · SNU · 그리고 산업

한국에서 로직 프로그래밍은 1990-2000년대에 KAIST AI 연구실과 서울대 컴퓨터공학과를 중심으로 자리 잡았다. 2026년 시점 액티브한 한국 그룹은 다음과 같다.

- **KAIST AI**: 신경-기호 결합과 자동 추론.

- **서울대 PLLab**: 정리 증명과 정적 분석 (Coq · Rocq · CodeQL).

- **POSTECH PL Lab**: 타입 이론 · 의존타입 라인.

- **카카오 · 네이버 보안팀**: 정적 분석에 CodeQL/Souffle 채용 보고.

학부 강의는 SWI-Prolog와 Coq/Rocq를 표준 도구로 가정하는 경우가 많다. 한국 정리 증명 진영은 2025년부터 Lean Mathlib 기여가 가시화되기 시작했다.

일본의 로직 프로그래밍 — NII · ICOT의 유산

일본은 1980년대 5세대 컴퓨터 프로젝트(ICOT, 1982-1992)로 Prolog의 가장 야심찬 산업 베팅을 했다. 결과는 혼합 평가였지만, 그 유산은 NEC, 후지쯔, 도호쿠 대학에 깊게 남았다. 현재 라인업.

- **NII(국립정보학연구소)**: 안정 모델 시맨틱스 · ASP 응용 라인이 활발.

- **사토 다이스케 그룹**: PRISM의 본가, 도쿄대 명예교수.

- **JIST(Joint International Semantic Technology Conference)** · **PRoCon**: 일본 로직 프로그래밍 커뮤니티의 정기 모임.

- **Logica Programming Tokyo**: 도쿄의 비공식 Prolog/Lean 사용자 모임. 2024년부터 Lean Together Tokyo로 분기.

책 · 강의 · 무엇으로 시작할까

- **"The Reasoned Schemer"**(Friedman · Byrd · Kiselyov, MIT Press 3판): miniKanren의 정전.

- **"The Power of Prolog"**(Markus Triska): 모던 ISO Prolog 학습서. Scryer Prolog 친화적.

- **"Prolog Programming for Artificial Intelligence"**(Ivan Bratko): Prolog 교과서의 고전 4판.

- **"Logic, Programming and Prolog"**(Nilsson · Maluszynski): 학술 표준 교과서. 무료 PDF.

- **"Concepts of Programming Languages"**(Robert Sebesta): 일반 PL 교과서지만 Prolog와 로직 패러다임 장이 견고하다.

- **"Software Foundations"**(Pierce 외): Coq/Rocq 학습의 정전. 무료 온라인.

- **"Theorem Proving in Lean 4"**(de Moura 외): Lean 4 공식 입문서.

- **"Concrete Semantics"**(Nipkow): Isabelle/HOL로 본 프로그램 시맨틱스.

학습 경로 — 한 달, 분기, 1년

한 달 계획부터 본격적인 1년 계획까지 정리한다.

1. **1주 차**: SWI-Prolog 9.x 설치, "Power of Prolog" 1-5장. N-Queens · 그래프 탐색 직접 짠다.

2. **2주 차**: Scryer Prolog로 옮겨 ISO 호환성 감각 익히고, CLP(FD)로 제약 문제.

3. **3주 차**: Clingo 5.7로 그래프 색칠 · 스케줄 · n-Queens. ASP의 비결정성과 최적화 감각.

4. **4주 차**: miniKanren("The Reasoned Schemer" 또는 core.logic). 호스트 임베디드 로직.

5. **분기 단위**: Souffle Datalog로 작은 정적 분석. Lean 4 · Mathlib 튜토리얼.

6. **1년 단위**: Rocq로 작은 컴파일러 또는 자료구조 검증. ICLP/CICM 페이퍼 한 편 따라가기.

자주 묻는 질문

**Q1. Prolog는 죽은 언어 아닌가요?**

A. 죽지 않았습니다. 산업 점유는 작지만, 항공·물류·결정 지원 · 정적 분석 · 형식 검증 · 신경-기호 LLM 백엔드로 살아 있습니다. TIOBE에서 2024-2025년 사이 30위권 내로 다시 들어왔습니다.

**Q2. Clingo만 알면 ASP는 충분한가요?**

A. 표준 ASP는 사실상 충분합니다. DLV는 분리 논리 확장이 강하지만, 학술 외에서는 Clingo가 사실상 표준입니다.

**Q3. Prolog로 LLM과 어떻게 결합하나요?**

A. 패턴 셋: (1) LLM이 Prolog 코드를 생성 → 서버에서 실행해 결과를 회신, (2) LLM의 도구 호출로 Prolog 쿼리를 통과, (3) Prolog 규칙을 retrieval-augmented context로 주입.

**Q4. Datalog는 Prolog의 부분집합인가요?**

A. 의미론적으로 그렇습니다. 함수 기호와 부정을 빼고, 모든 변수가 안전(safe)해야 합니다. 그 대신 종료 보장과 효율적 평가를 얻습니다.

**Q5. Rocq와 Lean 4 중 무엇을 시작해야 하나요?**

A. 수학·검증 라이브러리의 활성도라면 Lean 4 + Mathlib4가 가장 빠릅니다. 산업 컴파일러 검증·역사적 자료라면 Rocq(Coq)가 두텁습니다.

**Q6. miniKanren은 Prolog와 무엇이 다른가요?**

A. miniKanren은 호스트 언어에 임베드된 5개 연산자 미니 코어로, Prolog의 SLD 해소를 정의 가능한 검색 전략으로 노출합니다. cut이 없고 깊이 우선 대신 인터리브 검색을 기본으로 합니다.

**Q7. 학생 라이선스 외에 산업 사용이 자유로운가요?**

A. SWI-Prolog · Scryer · Trealla · Tau · Souffle · Clingo · Z3 · CVC5 · Rocq · Lean 4 · Isabelle · Agda · F\* · Pyro · MiniZinc · CozoDB · core.logic은 모두 상용 호환 오픈소스입니다. SICStus와 일부 ECLiPSe 모듈은 상용 라이선스가 필요합니다.

**Q8. 정적 분석을 Datalog로 짜려면 어디서 시작하나요?**

A. Souffle 공식 튜토리얼이 가장 가파릅니다. 그 다음 Doop 소스(자바 포인터 분석)와 GitHub의 CodeQL 공개 쿼리 모음을 비교 학습하면 됩니다.

**Q9. ASP로 어떤 산업 문제를 풀 수 있나요?**

A. 병원 근무표 · 항공기 게이트 배정 · 시스템 구성(SUSE Open Build Service) · 학교 시간표 · 결정 지원 시스템 · 게놈 추론. ICLP/ASP-Comp 산업 트랙 사례가 풍부합니다.

**Q10. 한국·일본에 산업 적용 사례가 있나요?**

A. 공개된 케이스는 제한적이지만, 한국은 보안 진영에서 CodeQL/Souffle 채택이 확산 중이고, 일본은 후지쯔·NEC가 ICOT 라인의 유산으로 자동 추론 R&D를 유지합니다. NII가 가장 가시적인 학술 허브입니다.

참고 자료

- SWI-Prolog 공식 사이트: https://www.swi-prolog.org/

- Scryer Prolog: https://www.scryer.pl/ , https://github.com/mthom/scryer-prolog

- Trealla Prolog: https://github.com/trealla-prolog/trealla

- Tau Prolog: http://tau-prolog.org/

- GNU Prolog: http://www.gprolog.org/

- SICStus Prolog: https://sicstus.sics.se/

- ECLiPSe 제약 시스템: https://eclipseclp.org/

- Mercury 언어: https://mercurylang.org/

- Souffle Datalog: https://souffle-lang.github.io/

- DDlog: https://github.com/vmware/differential-datalog

- CozoDB: https://www.cozodb.org/

- Clingo (Potassco): https://potassco.org/clingo/

- DLV ASP 시스템: http://www.dlvsystem.com/

- miniKanren 공식: http://minikanren.org/

- core.logic (Clojure): https://github.com/clojure/core.logic

- Flora-2: http://flora.sourceforge.net/

- Rocq Prover (전 Coq): https://rocq-prover.org/

- Lean 4 + Mathlib4: https://leanprover-community.github.io/

- Isabelle 증명 보조기: https://isabelle.in.tum.de/

- Agda: https://agda.readthedocs.io/

- F\* (F-star): https://www.fstar-lang.org/

- HOL Light: https://www.cl.cam.ac.uk/~jrh13/hol-light/

- HOL4: https://hol-theorem-prover.org/

- Idris 2: https://www.idris-lang.org/

- MiniZinc: https://www.minizinc.org/

- Google OR-Tools: https://developers.google.com/optimization

- Choco-solver: https://choco-solver.org/

- Gecode: https://www.gecode.org/

- Z3 SMT 솔버: https://github.com/Z3Prover/z3

- CVC5: https://cvc5.github.io/

- CaDiCaL SAT 솔버: https://github.com/arminbiere/cadical

- ProbLog: https://dtai.cs.kuleuven.be/problog/

- Stan: https://mc-stan.org/

- PyMC: https://www.pymc.io/

- Pyro: https://pyro.ai/

- Neo4j: https://neo4j.com/

- TerminusDB: https://terminusdb.com/

- Markus Triska, "The Power of Prolog": https://www.metalevel.at/prolog

- "The Reasoned Schemer" (MIT Press): https://mitpress.mit.edu/9780262535519/the-reasoned-schemer/

- "Software Foundations": https://softwarefoundations.cis.upenn.edu/

- ICLP — International Conference on Logic Programming: https://iclp-conference.github.io/

- ASP Competition: https://www.mat.unical.it/aspcomp2024/