Chaos and Order

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

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

はじめに — 2026年5月、なぜ今あらためて論理プログラミングか

「Prologは1972年の言語だ。21世紀になぜ振り返るのか」。5年前なら正当な疑問だった。しかし2026年春、論理プログラミングは三つの戦線で同時に復活している。第一に、LLMエージェントが記号的に検証可能な推論を求めるなかで、PrologとASPが推論バックエンドとして静かに呼び戻されている。第二に、Souffle DatalogがGitHub CodeQLの学術的系譜とMeta規模の静的解析パイプラインを経て、業界水準の静的解析エンジンとして定着した。第三に、Rocq(改称前のCoq)とLean 4が数学・検証領域で爆発的に採用され、「定理証明器 = 関数型 + 依存型を持つ論理言語」という見方が一般化した。

本稿はマーケティング資料ではない。2026年5月時点で実際に動いている論理プログラミングのツールをファミリーごとにまとめ、どこで使われ、どこで止まったかを書く。

論理プログラミングの4つの大ファミリー

比較の前に地図がいる。論理プログラミングは単一の言語ではなく、四つのファミリーの和集合だ。

1. **Prologファミリー** — Horn節の上にSLD導出とバックトラックを乗せた古典的パラダイム。SWI-Prolog · Scryer · Trealla · Tau · Mercury · ECLiPSeがここに属する。

2. **Datalogファミリー** — Prologから関数記号と非決定性を抜き、停止性と効率性を得た部分集合。Souffle · DDlog · CozoDB · Datomic · XTDBが代表。

3. **Answer Set Programming(ASP)** — 安定モデル意味論(stable model semantics)に基づき、可能な解を網羅列挙する。Clingo · DLV · WASPがほぼすべてを占める。

4. **関係的埋め込み言語** — miniKanren / core.logic / microKanrenのように、ホスト言語(Scheme · Clojure · Racket)に埋め込まれた関係的DSL。

さらに5番目の縦糸として、定理証明器(Coq · Lean · Isabelle · Agda · F\*)はCurry-Howard対応を通じて論理プログラミングと深く接続する。本稿では1つの幹として扱う。

一覧 — 2026年5月の論理プログラミング・ラインナップ

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

| ASP | Clingo | MIT | 事実上のASP標準 |

| ASP | DLV | 学術 | 選言論理プログラミング |

| 証明器 | Isabelle/HOL | BSD | seL4検証 · ML基盤 |

| 証明器 | Agda | MIT | 依存型の学術系譜 |

| 証明器 | F\* | Apache 2.0 | MSR · 検証 |

| CP | MiniZinc | MPL | モデリング標準 |

| CP | Choco-solver | BSD-4 | Java制約 |

| CP | 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サーバ(`http_server/2`)、制約論理(CLP(FD), CLP(R))、SSL、JSON、Unicode、スレッド、モジュール、ODBCを標準配布で揃える。

典型的なSWI-Prologのコードは次のような形になる。

:- 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 — Rustで書き直された現代的なISO Prolog

ScryerはMark Thomが始めたISO標準PrologのRust実装だ。SWIが実用性を優先するなら、Scryerは正確性を優先する。2026年5月時点で0.9.x系が活発に開発中で、Markus Triska著の「The Power of Prolog」のコードはScryerで検証されている。

Scryerは属性変数(attribute variables)とCLP(B/Z/FD)を標準配布で含み、Triskaのマニフェストに従って「副作用を最小化し、純粋Prologを推奨する」路線を取る。

Trealla Prolog — Cで書かれた組込み向けProlog

Trealla(Andrew Davison)はMITライセンスのC実装で、単一バイナリが小さく組込みシステムに埋め込みやすい。WebAssemblyビルドも安定しており、Tauと並ぶブラウザ用Prologの選択肢だ。

Tau Prolog — 純粋JavaScriptのProlog

Tau PrologはJose Antonio Riazaが作った純粋JavaScript実装で、Node.jsでもブラウザでも動作し、DOMを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。コンパイル結果をネイティブバイナリとして落とせ、有限領域制約ソルバを含む。

- **SICStus Prolog**: スウェーデンのSICSが始めた商用Prolog。Mats Carlssonが主導し、航空・物流・通信のミッションクリティカル系で使われる。ライセンスは商用。

- **ECLiPSe**: IC-Parc(Imperial College)発の制約論理プログラミング系。MPLでオープン化されており、CHR(Constraint Handling Rules)の実験版がもっとも洗練されている。

Mercury — 強い型と決定性宣言を持つPrologの後裔

Mercuryはオーストラリアのメルボルン大学のZoltan Somogyiが1990年代に開始した言語で、「Prologの宣言的意味論はよいが、副作用とモードが乱れて大規模に使えない」という批判に答えた。Mercuryは次を要求する。

- **モード宣言**: 各引数が`in`か`out`かを明示。

- **決定性宣言**: `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).

Mercuryは大規模プログラムの静的解析やコンパイラバックエンドで生き残っており、ICFP/ICLPで継続的に発表されている。

Datalogファミリー — 停止性を獲得したPrologの従兄弟

DatalogはPrologから関数記号を取り除き、節を平坦にした部分集合だ。その結果、評価は停止し、bottom-upのsemi-naive評価により効率的に計算できる。2026年5月時点では三つの分岐が定着している。

- **静的解析向けDatalog**: Souffle, Doop

- **差分Datalog**: DDlog

- **埋込みDatalog DB**: CozoDB, Datomic, XTDB

Souffle — 静的解析の標準Datalog

Souffle(シドニー大学発)はDatalogプログラムをC++にコンパイルし、マルチスレッドで評価する。中心的な用途は静的プログラム解析で、Doop(Javaポインタ解析)、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で活発に維持されている。Universal Permissive License (UPL) 1.0で公開されており、商用利用も自由だ。

DDlog · CozoDB · Datomic · XTDB

- **DDlog**: VMware Research発の差分Datalog。入力が変わると差分のみ再計算する。ネットワーク制御プレーンの検証で利用。

- **CozoDB**: 中国発のオープンソースDatalogデータベース。Rust組込み、時系列・グラフ・ベクター検索の問い合わせを単一のDatalog方言で統合する。

- **Datomic / XTDB**: Clojure生態系の時間認識データベース。問い合わせ言語はDatalogの方言。別途Clojure記事で深掘りした。

Answer Set Programming — Clingoの時代

ASPは安定モデル意味論をベースとする非決定的論理プログラミングだ。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パッケージ依存関係解決 — 例えばopenSUSE 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側ではDavid Nolenの**core.logic**がminiKanrenを移植し、Clojure標準ライブラリに近い位置を占めている。

Flora-2 — F-Logicの生きた実装

Flora-2はストーニーブルックのMichael Kiferが主導するF-Logic実装で、オブジェクト指向と論理を一つの言語で統合する。HiLog、トランザクション論理、義務論理(deontic logic)拡張まで含む。学術的セマンティックウェブ推論や政策表現で生き残っており、商用後継としてCoherent KnowledgeのErgoAIに継承されている。

定理証明器 — Rocq · Lean 4 · Isabelle · Agda · F\*

証明補助器は論理プログラミングの兄弟分野だ。2024年6月にInriaがCoqを**Rocq**に改称し、9.0が新名称下での最初のメジャーリリースとなった。依存型、Gallina仕様言語、機械検証済みの数学(CompCertコンパイラ、四色定理)はすべて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, MSR)は精密型(refinement type)と効果システムによって、分散システムや暗号プロトコルの検証に使われる。**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で再設計し、線形性を第一級にした。**Cedille**(Aaron Stump、アイオワ大学)はよりミニマルな依存型コア言語の研究プロジェクトで、学術的影響が大きい。

制約プログラミング — MiniZinc · OR-Tools · Choco · Gecode

論理プログラミングの兄弟分野が制約プログラミング(CP)だ。2026年時点でもっとも活発なツールは以下。

- **MiniZinc**: ニュージーランド・モナシュ系列が作る制約モデリングの共通言語。モデルをGecode, Chuffed, OR-Toolsなど複数のソルバに送れる。

- **OR-Tools**: Googleが作るC++/Pythonの制約・LP・ルーティングライブラリ。CP-SATソルバは事実上の業界標準。

- **Choco-solver**: フランスIMT AtlantiqueのJava制約ソルバ。BSD-4。

- **Gecode**: スウェーデンKTH・ドイツSaarlandの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 Bjorner。事実上のSMT標準。MIT。

- **CVC5**(スタンフォード · アイオワ): Z3の学術代替。BSD。

- **Yices**(SRI International): 産業と研究の両方で利用される。

- **MiniSat / Glucose**: 学術SATソルバの古典。

- **Lingeling / CaDiCaL**: Armin Biereが牽引するSATソルバ。CaDiCaLは近年SATコンペティションの上位常連だ。

Z3のPythonバインディング(`z3-solver`)が、ほぼすべてのLLMエージェントが外部SMTソルバを呼び出す際に想定する標準である。

確率的論理プログラミング — PRISM · ProbLog · Pyro · Stan · PyMC

確率的論理は論理プログラミングに確率分布を加える系譜だ。**PRISM**(東京大学の佐藤泰介らの系譜)と**ProbLog**(KU LeuvenのLuc De Raedtチーム)が代表的な学術システム。産業採用ではベイズ寄りの**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は、IBM自身の発表によれば自然言語解析パイプラインの一部にPrologを使っていた。

- **GitHub CodeQL**: 買収前のSemmleが作った学術的従兄弟SemmleQLはDatalog由来。2026年時点でCodeQLはGitHub Securityの中核だ。

- **seL4**: seL4マイクロカーネルの機能正確性証明はIsabelle/HOLで完成された(2014、以降強化)。

- **SUSE / openSUSEのパッケージ依存解決**: libsolvがSATソルバで解決する。ASPは学術代替として頻繁に比較される。

- **Erlangの起源**: エリクソンのJoe Armstrong回顧録によれば、Erlangの初期プロトタイプはPrologで書かれていた。パターンマッチや単一代入がPrologっぽいのはそのためだ。

LLM時代の論理プログラミング — ニューロシンボリックの再来

2025-2026年の大きな絵は「LLMが検証できない部分を論理エンジンに外注する」流れだ。三つのパターンが目立つ。

1. **LLM → Z3**: LLMが自然言語の制約をZ3式に変換し、ソルバが検証する。OpenAI · Anthropicの推論モデルが内部でSMT/SAT呼び出しを学習しているとの報告が増えている。

2. **LLM → Prolog/ASP**: 自然言語規則をASPエンコーディングに変換し、Clingoが答え集合を列挙する。スケジューリング、システム構成、法的推論。

3. **ニューロシンボリックなファインチューニング**: DeepMindのPearl Lab発表などで、LLMの中にミニPrologインタプリタを埋め込み、多段推論を改善する系譜。

韓国の論理プログラミング — KAIST · ソウル大 · そして産業

韓国では1990-2000年代にKAIST AI研究室とソウル大学コンピュータ工学科を中心に論理プログラミングが定着した。2026年時点で活動的な韓国グループは次の通り。

- **KAIST AI**: ニューロシンボリック統合と自動推論。

- **ソウル大PLLab**: 定理証明と静的解析(Coq · Rocq · CodeQL)。

- **POSTECH PL Lab**: 型理論と依存型の系譜。

- **KakaoとNaverのセキュリティチーム**: CodeQL/Souffleを静的解析に採用する報告。

学部講義はSWI-PrologとCoq/Rocqを標準ツールとして想定することが多い。韓国の貢献としてLean Mathlibへのコミットが2025年から目立つようになった。

日本の論理プログラミング — NIIとICOTの遺産

日本は1980年代の第五世代コンピュータプロジェクト(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をインストール。「The 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の論文を1本通読する。

よくある質問

**Q1. Prologは死んだ言語ではないか?**

A. 死んでいない。市場シェアは小さいが、航空 · 物流 · 意思決定支援 · 静的解析 · 形式検証 · LLMのニューロシンボリック・バックエンドで生きている。TIOBEで2024-2025年に上位30入りに戻った。

**Q2. ASPはClingoだけ知っていれば十分か?**

A. 主流ASPなら事実上十分。DLVは選言論理のサポートが強いが、学術以外ではClingoが事実上のデファクトだ。

**Q3. PrologをLLMとどう組み合わせるか?**

A. パターンセット: (1) LLMがPrologコードを生成しサーバが実行して結果を返す、(2) LLMのツール呼び出しでPrologクエリを通す、(3) Prolog規則をRAGの文脈として注入する。

**Q4. DatalogはPrologの部分集合か?**

A. 意味論的にはそうだ。関数記号と既定の否定を捨て、すべての変数が安全(safe)でなければならない。代わりに停止保証と効率的評価を得る。

**Q5. RocqとLean 4のどちらを始めればよいか?**

A. 数学・検証ライブラリのアクティビティを求めるならLean 4 + Mathlib4が最速の入口。産業コンパイラ検証や歴史的資料ならRocq(Coq)が厚い。

**Q6. miniKanrenはPrologと何が違うのか?**

A. miniKanrenはホスト言語に埋め込まれた5演算子のミニコアで、SLD導出を定義可能な探索戦略として公開する。cutを持たず、深さ優先ではなくインタリーブ探索を既定とする。

**Q7. 商用利用は自由か?**

A. SWI-Prolog · Scryer · Trealla · Tau · Souffle · Clingo · Z3 · CVC5 · Rocq · Lean 4 · Isabelle · Agda · F\* · Pyro · MiniZinc · CozoDB · core.logicはいずれも商用フレンドリーなOSS。SICStusと一部のECLiPSeモジュールは商用ライセンスが必要だ。

**Q8. Datalogで静的解析を書くにはどこから?**

A. Souffleの公式チュートリアルが最も急な学習坂。続いてDoopのソース(Javaポインタ解析)と公開CodeQLクエリを並べて読むとよい。

**Q9. ASPで解ける産業問題は?**

A. 病院シフト · 航空機ゲート割当 · システム構成(openSUSE 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/