Chaos and Order

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

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

Intro — Why look at logic programming again in May 2026

"Prolog is a 1972 language. Why bother in the 21st century?" Five years ago that was a fair question. In spring 2026 the answer is concrete on three fronts. First, LLM agents are reaching for symbolic backends they can verify, and Prolog and ASP are quietly being wired in as reasoning engines. Second, Souffle Datalog has earned an industrial-grade reputation through GitHub CodeQL's lineage and Meta-scale static analysis pipelines. Third, Rocq (the renamed Coq) and Lean 4 have exploded in mathematics and formal verification, normalizing the view that "theorem prover = functional + dependently-typed logic language".

This piece is not a marketing brochure. It groups the logic programming tools that are actually alive in May 2026 by family, says where they are used, and where they have stalled.

The four big families of logic programming

We need a map before a comparison. Logic programming is not one language but the union of four families.

1. **The Prolog family** — Horn clauses with SLD resolution and backtracking. SWI-Prolog, Scryer, Trealla, Tau, Mercury, and ECLiPSe live here.

2. **The Datalog family** — Prolog without function symbols, restricted to safe rules. Termination and efficient bottom-up evaluation in exchange for expressive power. Souffle, DDlog, CozoDB, Datomic, and XTDB.

3. **Answer Set Programming (ASP)** — built on stable model semantics; enumerate every solution. Clingo, DLV, and WASP cover essentially the field.

4. **Embedded relational languages** — miniKanren, core.logic, microKanren: tiny relational DSLs hosted inside Scheme, Clojure, or Racket.

A fifth strand we cover for completeness is proof assistants (Coq/Rocq, Lean 4, Isabelle, Agda, F\*), which connect to logic programming through the Curry-Howard correspondence between programs and proofs.

At a glance — the May 2026 lineup

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

| ASP | Clingo | MIT | De facto ASP standard |

| ASP | DLV | Academic | Disjunctive logic programming |

| CP | MiniZinc | MPL | Modeling lingua franca |

| CP | Choco-solver | BSD-4 | Java constraints |

| CP | Gecode | MIT | C++ constraints |

| SAT/SMT | Z3 | MIT | De facto SMT |

| SAT/SMT | CVC5 | BSD | Academic SMT |

Each row is taken from the projects' May 2026 GitHub README files and ICLP/JICSLP notes — not from press kits.

SWI-Prolog 9.x — the de facto Prolog

SWI-Prolog began in 1986 with Jan Wielemaker in the Netherlands and ships, as of 2026, a stable 9.x line under a BSD-2 license. Out of the box you get an HTTP server library (`http_server/2`), constraint logic programming over finite domains and reals (CLP(FD), CLP(R)), SSL, JSON, Unicode, threads, modules, and ODBC.

A typical SWI-Prolog program looks like this.

:- 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 strikes the best balance of "ISO Prolog plus pragmatic libraries". Most undergraduate logic programming courses in Korea and Japan assume SWI.

Scryer Prolog — a modern ISO Prolog in Rust

Scryer, started by Mark Thom, is an ISO-standard Prolog implementation written in Rust. Where SWI optimizes for pragmatism, Scryer optimizes for correctness. The 0.9.x line is under active development in May 2026, and Markus Triska's book "The Power of Prolog" is validated against Scryer.

Scryer ships attribute variables and CLP(B/Z/FD) in the standard distribution and follows Triska's manifesto of minimal side effects and pure Prolog by default.

Trealla Prolog — a tiny embeddable Prolog in C

Andrew Davison's Trealla is an MIT-licensed C implementation that is small enough to embed. Its WebAssembly build is solid, making it a natural companion to Tau Prolog for browser-side reasoning.

Tau Prolog — pure JavaScript Prolog

Tau Prolog by Jose Antonio Riaza is a pure JavaScript Prolog implementation that runs on Node.js and in the browser, exposing the DOM as Prolog predicates. It is popular for educational demos and static-site reasoning widgets.

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 — the older giants

- **GNU Prolog** — Daniel Diaz, 1996, GPL. Compiles to native binaries and ships a finite-domain constraint solver.

- **SICStus Prolog** — commercial Prolog out of the Swedish Institute of Computer Science, led by Mats Carlsson. Used in mission-critical aerospace, logistics, and telecoms systems.

- **ECLiPSe** — IC-Parc's MPL-licensed constraint logic programming system; the most polished experimental playground for CHR (Constraint Handling Rules).

Mercury — strongly typed Prolog descendant

Mercury, started in the 1990s by Zoltan Somogyi at the University of Melbourne, answered the criticism that Prolog's declarative semantics are excellent but its mode and side-effect story prevent scaling. Mercury demands.

- **Mode declarations**: each argument is `in` or `out`.

- **Determinism declarations**: `det`, `semidet`, `multi`, `nondet`.

- **Type classes** in the Haskell tradition.

- **Pure functions**: I/O threaded through an `io` state variable.

:- module hello.

:- interface.

:- import_module io.

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

:- implementation.

main(!IO) :-

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

Mercury survives in large-scale static analysis and compiler backends, and is a steady presence at ICFP/ICLP.

The Datalog family — Prolog's terminating cousin

Datalog is the subset of Prolog without function symbols, with safe variables only. The trade is termination and efficient bottom-up semi-naive evaluation. By May 2026, three Datalog branches are alive.

- **Static-analysis Datalog**: Souffle, Doop.

- **Incremental Datalog**: DDlog.

- **Embeddable Datalog DBs**: CozoDB, Datomic, XTDB.

Souffle — Datalog as a static-analysis backend

Souffle, originating at the University of Sydney, compiles Datalog programs to multi-threaded C++. Its main niche is static program analysis: Doop's Java points-to analysis, the academic relatives of CodeQL, and many security consultancies' internal pipelines run on Souffle.

.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).

Stable 2.5.x is actively maintained on GitHub in May 2026 under the Universal Permissive License (UPL) 1.0, which is friendly to commercial use.

DDlog, CozoDB, Datomic, XTDB

- **DDlog** — VMware Research's incremental Datalog. When inputs change, only the deltas are recomputed. Used inside network control-plane verification.

- **CozoDB** — open-source Datalog database started in China. Rust embeddable, unifies time-series, graph, and vector search queries under one Datalog dialect.

- **Datomic / XTDB** — temporal databases in the Clojure ecosystem whose query language is a Datalog dialect. Covered in our Clojure deep dive.

Answer Set Programming — Clingo's era

ASP is a nondeterministic logic programming paradigm built on the stable model semantics. Where Prolog finds a single solution by backtracking, ASP enumerates every answer set and supports weights, optimization, and aggregates on top of that.

The de facto standard ASP system in May 2026 is **Clingo** out of the University of Potsdam in Germany, driven by Roland Kaminski, Torsten Schaub, and Martin Gebser. The 5.7.x line is stable and the license is MIT.

% Graph coloring: assign 3 colors such that no neighbors share one

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.

Alternative ASP systems include Italy's **DLV** (disjunctive logic) and Australia's **WASP**. Clingo wins on optimization, ASP-Core-2 standard compliance, a clean Python API (`clingo` package), and the gringo + clasp split build.

Industrial use today: scheduling (hospital rosters, aircraft assignment), decision-support systems, system configuration (Linux package dependency resolution — for example openSUSE Build Service).

miniKanren — relational DSL embedded in a host language

miniKanren, started by Daniel Friedman and William Byrd at Indiana University, is a small relational programming language. With five core operators (`==`, `fresh`, `conde`, `run`, `run*`) it supports Prolog-style relational reasoning, embedded into Scheme, Racket, Clojure, Python, or JavaScript.

"The Reasoned Schemer" (MIT Press, third edition 2018) is the canonical text. microKanren is a roughly 39-line Scheme implementation of the core.

(run* (q)

(fresh (a b)

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

(conde

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

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

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

In the Clojure ecosystem, David Nolen's **core.logic** ports miniKanren and sits close to the standard library in status.

Flora-2 — a living F-Logic implementation

Flora-2, led by Michael Kifer at Stony Brook, implements F-Logic, unifying object-oriented and logic paradigms in a single language. HiLog, transactional logic, and deontic logic extensions are all there. It survives in academic semantic web reasoning and policy expression, and continues commercially through ErgoAI by Coherent Knowledge.

Theorem provers — Rocq, Lean 4, Isabelle, Agda, F\*

Proof assistants are siblings of logic programming. In June 2024, Inria renamed Coq to **Rocq**, and 9.0 was the first major release under the new name. Dependent types, the Gallina specification language, and machine-checked mathematics (CompCert, the Four Color Theorem) all run on Rocq.

**Lean 4**, led by Leonardo de Moura after he left Microsoft Research, is a dependently typed functional language with first-class metaprogramming. Mathlib4 crossed a million lines somewhere between 2024 and 2025 and is now arguably the largest machine-checked mathematics library. In spring 2026, some of Terence Tao's research is being formalized in Lean, accelerating academic adoption.

**Isabelle/HOL** is the classical Cambridge / TU Munich proof assistant, the backbone of the seL4 microkernel functional-correctness proof. Standard ML based, BSD licensed.

**Agda** out of Chalmers is a dependently typed functional language and proof assistant, standard in dependent-types pedagogy. **F\*** (F-star, MS Research) uses refinement types and an effect system to verify distributed systems and cryptographic protocols. **HOL Light** (John Harrison) and **HOL4** (the Cambridge line) are more minimal HOL implementations, used for academic verification and library certification.

-- Lean 4 — commutativity of natural-number addition

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 — the next generation of dependent types

**Idris** by Edwin Brady at St. Andrews is a Haskell-friendly dependently typed functional language. Idris 2 reworked the core around Quantitative Type Theory, making linearity first class. **Cedille** by Aaron Stump at Iowa is a more minimal dependently typed core, primarily a research project with substantial academic influence.

Constraint programming — MiniZinc, OR-Tools, Choco, Gecode

A close sibling of logic programming is constraint programming (CP). The most active tools in 2026 are.

- **MiniZinc** — the Monash-led constraint modeling lingua franca. A model can be dispatched to Gecode, Chuffed, OR-Tools, or other solvers.

- **OR-Tools** — Google's C++/Python constraint, LP, and routing library. The CP-SAT solver has effectively become an industry standard.

- **Choco-solver** — French IMT Atlantique's Java constraint solver under BSD-4.

- **Gecode** — the C++ constraint solver out of KTH/Saarland, MIT licensed.

% 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 and SMT solvers — Z3, CVC5, CaDiCaL, MiniSat

The engines behind symbolic reasoning are SAT (Boolean satisfiability) and SMT (SAT modulo theories) solvers. The 2026 lineup.

- **Z3** (Microsoft Research): Leonardo de Moura and Nikolaj Bjorner. De facto SMT standard. MIT.

- **CVC5** (Stanford and Iowa): the academic alternative to Z3, BSD licensed.

- **Yices** (SRI International): used in industry and research alike.

- **MiniSat / Glucose**: the academic SAT classics.

- **Lingeling / CaDiCaL**: led by Armin Biere. CaDiCaL has been a regular top finisher in the SAT competition.

Z3's Python binding (`z3-solver`) is what almost every LLM agent assumes when it "calls out to an SMT solver".

Probabilistic logic — PRISM, ProbLog, Pyro, Stan, PyMC

Probabilistic logic adds probability distributions on top of logic programming. **PRISM** out of Sato Taisuke's group in Japan, and **ProbLog** from KU Leuven's Luc De Raedt group, are the canonical academic systems. Industrial uptake leans on the Bayesian side: **Stan** by Andrew Gelman's group, **PyMC** in Python, and **Pyro** from Uber AI Labs on top of PyTorch.

Knowledge graphs and the semantic web — Neo4j, GraphDB, Stardog, TerminusDB, TigerGraph

A sister field is knowledge graphs (KG). The 2026 lineup.

- **Neo4j** — de facto graph database with Cypher.

- **GraphDB** (Ontotext) — RDF/SPARQL semantic reasoning.

- **AllegroGraph** (Franz Inc) — Lisp-flavored RDF triple store.

- **Stardog** — commercial SPARQL with SHACL and reasoning.

- **TerminusDB** — open-source graph database written in Prolog with the Datalog dialect WOQL.

- **TigerGraph** — high-performance graph database with GSQL.

The RDF/SPARQL/OWL stack remains a W3C standard, and RDF 1.2 was recommended in 2025. Even with the cooling of the broader semantic-web pitch, pharma and life-sciences data integration and government data catalogs still ride on RDF.

Real-world deployments — Watson, CodeQL, seL4, package solvers

A few real, non-marketing deployments.

- **IBM Watson** — by IBM's own account, the 2011 Jeopardy champion's backend used Prolog for parts of its natural-language analysis pipeline.

- **GitHub CodeQL** — Semmle's pre-acquisition academic relative, SemmleQL, was Datalog-inspired. CodeQL is the heart of GitHub Security in 2026.

- **seL4** — the functional-correctness proof of the seL4 microkernel was completed in Isabelle/HOL (2014, with subsequent strengthening).

- **SUSE / openSUSE package dependency resolution** — libsolv uses a SAT solver; ASP shows up as a frequently compared academic alternative.

- **Erlang origins** — by Joe Armstrong's recollection, the earliest Erlang prototypes at Ericsson were written in Prolog, which is why pattern matching and single-assignment feel Prolog-flavored.

Logic programming in the LLM era — neuro-symbolic again

The big-picture story of 2025-2026 is "outsource what LLMs cannot verify to a logic engine". Three patterns dominate.

1. **LLM → Z3**: the LLM converts natural-language constraints into Z3 formulas and a solver verifies them. Reports keep accumulating that OpenAI's and Anthropic's reasoning models internalize SMT/SAT calls.

2. **LLM → Prolog/ASP**: natural-language rules become ASP encodings, and Clingo enumerates answer sets. Scheduling, system configuration, legal reasoning.

3. **Neuro-symbolic fine-tuning**: groups such as DeepMind's Pearl Lab embed mini Prolog interpreters inside LLMs to improve multi-step reasoning.

Logic programming in Korea — KAIST, SNU, and industry

In Korea, logic programming took root at KAIST AI Lab and Seoul National University's CS department in the 1990s and 2000s. As of 2026, the active Korean groups are roughly.

- **KAIST AI** — neuro-symbolic integration and automated reasoning.

- **Seoul National University PLLab** — proof assistants and static analysis (Coq, Rocq, CodeQL).

- **POSTECH PL Lab** — type theory and dependent types.

- **Kakao and Naver security teams** — reports of CodeQL/Souffle adoption for static analysis.

Undergraduate courses tend to assume SWI-Prolog and Coq/Rocq. Korean contributions to Lean Mathlib became visible in 2025.

Logic programming in Japan — NII and the ICOT legacy

Japan made the largest industrial bet on Prolog through the Fifth Generation Computer Project (ICOT, 1982-1992). The outcome was mixed, but the legacy is still visible at NEC, Fujitsu, and Tohoku University. The current lineup.

- **NII (National Institute of Informatics)** — active research line in stable model semantics and ASP applications.

- **Sato Taisuke's group** — PRISM's home, professor emeritus at the University of Tokyo.

- **JIST (Joint International Semantic Technology Conference)** and **PRoCon** — Japan's logic programming community meetings.

- **Logica Programming Tokyo** — an informal Prolog/Lean user group in Tokyo, with Lean Together Tokyo branching off in 2024.

Books and courses — where to start

- **"The Reasoned Schemer"** (Friedman, Byrd, Kiselyov, MIT Press, third edition): the miniKanren canon.

- **"The Power of Prolog"** (Markus Triska): modern ISO Prolog. Friendly to Scryer.

- **"Prolog Programming for Artificial Intelligence"** (Ivan Bratko): the classic Prolog textbook, fourth edition.

- **"Logic, Programming and Prolog"** (Nilsson and Maluszynski): the standard academic textbook. Free PDF.

- **"Concepts of Programming Languages"** (Robert Sebesta): a general PL textbook with strong chapters on Prolog and logic paradigms.

- **"Software Foundations"** (Pierce et al.): the canonical Coq/Rocq learning material. Free online.

- **"Theorem Proving in Lean 4"** (de Moura et al.): the official Lean 4 introduction.

- **"Concrete Semantics"** (Nipkow): program semantics through Isabelle/HOL.

A learning path — one month, one quarter, one year

A practical study plan.

1. **Week 1**: install SWI-Prolog 9.x. Read "The Power of Prolog" chapters 1-5. Write N-Queens and graph search yourself.

2. **Week 2**: switch to Scryer Prolog to feel ISO compliance. Use CLP(FD) for constraint problems.

3. **Week 3**: Clingo 5.7. Graph coloring, scheduling, N-Queens. Get a feel for ASP's nondeterminism and optimization.

4. **Week 4**: miniKanren (via "The Reasoned Schemer" or core.logic). Embedded relational logic in a host language.

5. **Per quarter**: build a small static analysis with Souffle. Walk through Lean 4 / Mathlib tutorials.

6. **Per year**: verify a small compiler or data structure with Rocq. Follow one ICLP/CICM paper end to end.

FAQ

**Q1. Isn't Prolog a dead language?**

A. No. Its market share is small but it survives in aerospace, logistics, decision support, static analysis, formal verification, and the neuro-symbolic backends behind LLMs. Prolog re-entered the TIOBE top 30 in 2024-2025.

**Q2. Is Clingo all I need for ASP?**

A. For mainstream ASP, yes. DLV has stronger disjunctive logic support, but outside academia Clingo is the de facto default.

**Q3. How do I combine Prolog with an LLM?**

A. Three patterns: the LLM generates Prolog code which a server executes and returns the result, the LLM's tool-calling interface invokes a Prolog query, or Prolog rules are injected as retrieval-augmented context.

**Q4. Is Datalog a subset of Prolog?**

A. Semantically, yes. It drops function symbols and negation by default, and every variable must be safe. In return you get guaranteed termination and efficient evaluation.

**Q5. Should I start with Rocq or Lean 4?**

A. For an active mathematics and verification library, Lean 4 plus Mathlib4 is the fastest on-ramp. For industrial compiler verification and historical material, Rocq (Coq) is deeper.

**Q6. How does miniKanren differ from Prolog?**

A. miniKanren is a five-operator mini-core embedded in a host language. It exposes SLD-style resolution as a definable search strategy, has no cut, and uses interleaving search by default rather than depth-first.

**Q7. Are these tools free for commercial use?**

A. SWI-Prolog, Scryer, Trealla, Tau, Souffle, Clingo, Z3, CVC5, Rocq, Lean 4, Isabelle, Agda, F\*, Pyro, MiniZinc, CozoDB, and core.logic are all under commercial-friendly open-source licenses. SICStus and some ECLiPSe modules need a commercial license.

**Q8. Where do I start writing a static analyzer in Datalog?**

A. Souffle's official tutorial has the steepest learning curve. After that, study Doop's source for Java points-to analysis and compare with public CodeQL queries.

**Q9. What industrial problems can ASP solve?**

A. Hospital rosters, aircraft gate assignment, system configuration (openSUSE Build Service), school timetables, decision support, and genome reasoning. The ICLP/ASP-Comp industrial track is full of case studies.

**Q10. Are there industrial deployments in Korea or Japan?**

A. Public case studies are limited, but Korean security teams are increasingly adopting CodeQL/Souffle. In Japan, Fujitsu and NEC maintain automated reasoning R&D as part of the ICOT legacy, with NII the most visible academic hub.

References

- 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 constraint system: https://eclipseclp.org/

- Mercury language: 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 system: 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 (formerly Coq): https://rocq-prover.org/

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

- Isabelle proof assistant: 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 solver: https://github.com/Z3Prover/z3

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

- CaDiCaL SAT solver: 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/