この連載について
本記事は、Dedukti という言語を扱う連載シリーズの 第3回目 です。
全体で何回になるかは決めていません。
| 回 | 扱うこと |
|---|---|
| 初回 | 定理証明支援系が出力した証明項を、翻訳器が .dk ファイルに翻訳し、Dedukti が検査する仕組み |
| 2 回目 | Dedukti の言語そのもの。識別子の宣言と書き換え規則の 2 種類で、論理体系と型理論を記述する |
| 3 回目（本記事） | Logical Framework という考え方。Edinburgh LF、Twelf、Isabelle/Pure との関係 |
| 4 回目 | Dedukti の実績と限界。年表、翻訳器、利用者、産業配備 |
初回記事、および前回までの記事はこちらです。
（初回）
- 【Dedukti入門 ①】Lean 4・Rocq・Isabelle が検証した証明を、もう一度別の証明検査器で検査する ── 翻訳器と符号化ファイルの仕組み
（２回目）
- 【Dedukti入門 ②】Lean 4 の型理論も HOL Light の高階論理も、なぜ同じ言語で書けるのか ── Dedukti の言語 λΠ計算 modulo rewriting を、実物のコードで読む
本記事について
初回記事では、翻訳器 と 符号化ファイル の 仕組み に光をあて、続く2 回目の記事では、Dedukti の言語 λΠ計算 modulo rewriting で何が記述できるかを、実物のコードを眺めながら論じました。
2回目の記事の終盤で、Logical Framework という言葉が登場しました。Logical Framework とは、複数の異なる論理体系 の 推論規則 を 記述するための言語 のことであり、このframework が、1987 年の Edinburgh LF まで歴史をさかのぼることができる、歴史の蓄積のある豊かな世界であることを紹介しました。
この Logical Framework は、Edinburgh LF から過去にさかのぼること 20年前、1967年の Automath に、淵源を発する考え方です。
Automath は、オランダの数学者 de Bruijn が作った、数学の証明を記述するための言語と、その証明を検査するプログラムの組（セット） です。
数学の証明を 計算機が読める言語（形式言語）で記述 し、その証明を別のプログラムで検査する 。
この 形式言語と検査手続きを分けるという発想 は、数理論理学によって、すでに見出されていましたが、計算機の上で動く仕組みとして初めて具現化したのが、Automath だった のです。
本稿（第3回目の記事）では、Logical Framework について、向かい合ってみたいと思います。
基本的な発想は、 「論理体系を記述する側」 と 「記述されたものを検査する側」 を分けるという世界観です。
この考え方は、Dedukti が発明したものではありません。
1967 年の Automath に始まり、1987 年の Edinburgh LF で、論理体系を記述するための言語として定式化されました。
Edinburgh LF は、言語の仕様・理論（ルールブック）です。
さまざまな論理体系をどう記述するか、その文法やルールの「決まりごと」を定めたものです。
1987 年に論文として発表された数学的な理論（λΠ計算をベースにした型理論）であり、概念上の存在です。紙の上に書かれた設計図と言えます。
Twelf は、Edinburgh LF の文法に従って定理証明プログラマ（人間です）が書いたテキスト（コード）を実際に読み込み、計算し、検査するソフトウェアです。カーネギーメロン大学の Pfenning と Schürmann によって開発されました。
Twelf は、単に Edinburgh LF のコードを読み込むだけでなく、主に以下のような実務を担います。
-
型検査（証明のチェック）：
定理証明プログラマが Edinburgh LF の文法で書いた「論理のルール」や「証明」が、本当に正しく組み立てられているかを自動で検証します。
-
メタ定理の証明：
記述された論理体系そのものが持つ性質（例：「この論理体系で証明したものは必ず計算が終わるか」など）を証明する機能を持っています。
-
論理プログラミング：
Edinburgh LF で書かれた規則を使って、Prolog のようにプログラムとして実行・探索させることができます。
つまり、「Edinburgh LF というルールを使って、実際に証明のチェックやメタ理論の検証を行ってくれる機械が Twelf」という役割分担になります。
出典
• Pfenning, F., Schürmann, C. "System Description: Twelf — A Meta-Logical Framework for Deductive Systems", CADE-16, 1999. https://www.cs.cmu.edu/~fp/papers/cade99.pdf
• Twelf（英語版 Wikipedia）https://en.wikipedia.org/wiki/Twelf
この発想は、Isabelle という広く使われている定理証明支援系の中にも受け継がれており、Deduktiにも引き継がれているのです。
Isabelle の場合、ルールブックにあたるのが Isabelle/Pure という メタ論理 です。
その上に 、高階論理（HOL）や集合論（ZF）が 対象論理として載っています。
読み込む対象論理を差し替えれば、扱える論理体系が変わります。
証明を検査するプログラムの側は、どちらの場合も同じです。
Dedukti の場合、ルールブックにあたるのが λΠ計算 modulo rewriting です。
翻訳器が同梱する符号化ファイル に、Lean 4 の型理論や HOL Light の高階論理が記述されています。読み込む符号化ファイルを差し替えれば、扱える定理証明支援系が変わります。
Dedukti の証明検査器が行うことは、どちらの場合も同じ型検査だけです。
| 名前 | ルールブック（記述する側） | 検査するプログラム | どこで書かれた証明を検査するか |
|---|---|---|---|
| Automath | Automath の言語。数学の証明を記述するための形式言語 | Automath の検査プログラム | Automath の中で書かれた証明 |
| Edinburgh LF | Edinburgh LF の文法（λΠ計算）。論理体系の推論規則を記述する | ── （言語の仕様であり、プログラムではない） | ── |
| Twelf | Edinburgh LF の文法（λΠ計算） | Twelf | Edinburgh LF の文法に従って書かれた証明 |
| Isabelle | Isabelle/Pure というメタ論理。その上に対象論理として HOL・ZF・FOL が載る | Isabelle の証明検査器（LCF 方式） | Isabelle の中で書かれた証明 |
| Dedukti | λΠ計算 modulo rewriting。翻訳器が同梱する符号化ファイルに、Lean 4 の型理論などが記述される | Dedukti の証明検査器 | Lean 4・Rocq など、外部の定理証明支援系が出力した証明項 |
Dedukti は何を受け継ぎ、何を足したのでしょうか？
本稿では、この問いに向き合っていきたいと思います。
なお、本稿は、初回・2 回目を読んでいなくても、本記事だけでお読みいただけるように心がけました。
専門用語は、出てきた場所で説明いたします。
記事末尾にも専門用語のミニ解説を掲載しました。
本記事の流れ
序章 ── 定理証明器を、誰が検査するのか
本連載シリーズの初回記事は、次の問いからスタートしました。
AI が数学の証明を書き、定理証明器がそれを検査する時代に、その定理証明器を、誰が検査するのか？
同じ問いが、AI が生まれるずっと前からありました。
1960 年代末、オランダの数学者 de Bruijn は、数学の証明を計算機で検査する体系 Automath を作りました。着想は 1966 年、開始は 1967 年、プロジェクトの最盛期は 1970 年から 1975 年です。
de Bruijn は、そのとき次の 原則 を立てました。
証明は、小さな独立したプログラムで検査できる形にしておくべきである。
この 原則 は、後に Barendregt によって de Bruijn 基準（de Bruijn criterion） と名づけられました。
Barendregt は この基準 を次のように 定義 しています。
- 定理証明支援系が証明項を生成する。
- その証明項を、懐疑的な利用者が自分で書ける程度の単純なプログラムで、独立に検査できる。
この2つが満たされていることです。
-
証明検査器が小さければ、証明検査器そのものを人間が読んで確かめることができる。
- 証明検査器が独立していれば、証明を作った定理証明支援系のバグが、検査の結論に入り込まない。
出典
Automath の年代について。Eindhoven University of Technology, "About Automath". https://automath.win.tue.nl/aboutautomath.htm
出典：de Bruijn 基準の命名について。H. Barendregt, F. Wiedijk, "The challenge of computer mathematics", Philosophical Transactions of the Royal Society A 363, 2005.
2026 年、この原則の価値が、急に上がりました。
AI（LLM / AI Agent） が証明の候補を書き、定理証明器がそれを検査する場面が増えた からです。
ケプラー予想の形式証明は約 50 万行、奇数位数定理は約 15 万行です。
この長さの証明を、人間が 1 行ずつ読むことはありません。
定理証明器が型検査を通したことが、正しさの根拠になります。
50年前に打ち建てられた原則が、定理証明支援系を専門とする狭いコミュニティの研究者によって共有される問いから、AI の出力を使う世界中の多くの人々や企業・政府・非営利団体などに関わる全員に係わりのある問いに変わりました。
その答えのひとつが、Dedukti です。
1つの論理を組み込んだ定理証明支援系ではなく、さまざまな論理そのものを記述するための言語 ── Logical Framework ── です。
この言語の上に翻訳された証明は、たった 1 つの小さな証明検査器で再検査できます。
本稿の議論の道筋を先に示します。
第1章で、定理証明支援系ごとに論理が違うことと、その分断を見ます。
第2章で、論理を記述する枠組みという発想を扱います。
第 3 章で、Isabelle がすでにその枠組みの上に建っていることを見ます。
あわせて、Isabelle はなぜ Dedukti にならなかったのか、という問いを対話篇で扱います。
最後に、Dedukti 以外の Logical Framework をコラムで並べます。
第 1 章 ── 定理証明支援系は、それぞれ違う論理の上に建っている
定理証明支援系は、それぞれ違う論理の上に建っています。
代表的な定理証明支援系と、その土台を一覧表にまとめたのが、次の表です。
| 定理証明支援系 | 土台の論理・型理論 | 土台の特徴 |
|---|---|---|
| Lean 4 | Calculus of Inductive Constructions（CIC）の変種 | 依存型。帰納型。宇宙の階層。命題の証明どうしを区別しない（proof irrelevance） |
| Rocq（旧 Coq） | CIC | 依存型。帰納型。宇宙の階層。Lean 4 とは細部が異なる |
| Agda | Martin-Löf 型理論の系統 | 依存型。帰納族。依存パターンマッチ。Lean や Rocq より公理が少ない |
| Isabelle/HOL | 高階論理（HOL） | 単純型。古典論理。依存型を持たない |
| HOL Light | 高階論理（HOL） | Isabelle/HOL と同系統。検査の核が数百行と極めて小さい |
| Matita | CIC | Rocq と同系統。小さく作られている |
| PVS | 高階論理＋述語による部分型 | 型検査が決定不能になる強力な型 |
同じ「依存型」でも、Lean 4 と Agda では公理の量が違います。
また、同じ「高階論理」でも、Isabelle/HOL と PVS では型の仕組みが違います。
証明は、土台の論理に依存します。
Lean 4 で書かれた証明は、Lean 4 の論理の中では、正しい証明です。
ところが、その証明を Agda に持っていっても、Agda の論理には Lean 4 の公理がありません。そのままでは、証明として成立しません。
「定理証明器」という 1 つの言葉でまとめられている定理証明支援系は、実際には、論理の数だけ存在する証明器なのです。
過去に公開済みの記事で見てきたとおり、論理はひとつではありません。
📚 過去に公開済みの記事 ── 「論理はひとつではない」の系譜（5 本）
本記事の前提になる過去記事です。未読でも本記事は読めます。
論理はひとつではない ── 圏論論理学がつなぐ量子論理・トポス・圏論的量子力学
https://qiita.com/etale_cohomology/items/24858c3bd7c7d6833eaa
系譜の出発点。古典論理・直観主義論理・量子論理を並べ、推論の規則を取り替えると別の論理が立ち現れることを示します。論理を収める「器」を選べば、その中で成り立つ論理がひとつ決まる、という見方をここで導入しました。
トポスと論理の関係 ── ひとつのトポス（数学の宇宙）を選ぶと、なぜ古典論理か直観主義論理が決まるのか ── そして、トポス以外の「器」たち
https://qiita.com/etale_cohomology/items/5206679c2fd02aea9512
「器」の正体がトポスであることを、真理値の目盛り Ω を軸に説明します。集合の世界では目盛りが 2 つで古典論理、層の世界では目盛りが増えて直観主義論理になる。線形論理・時相論理・量子論理には、トポスとは別の器があることも整理しました。
if 文も SQL も、実は別々の「論理」だった ── 古典論理から量子論理まで、21 の論理体系を 5 人で議論【対話篇】
https://qiita.com/etale_cohomology/items/4fadbda1ebea7a63f68d
高校生・大学院生・エンジニア・弁護士・哲学者の 5 人が、21 の論理体系を 1 つずつ語る対話篇。if 文、SQL の NULL、Rust の所有権、TLA+ が、それぞれ別の論理の上で動いていることを見ます。結章で、論理の最低限の成立要件が圏の公理と一致することに触れています。
量子論理・トポス・圏論的量子力学は何に使うの？ ── 量子コンパイラから量子インターネットまで
https://qiita.com/etale_cohomology/items/8c856d3fff8015e62517
量子の世界を扱う 3 つの枠組みが、どこで実際に使われているかを追った対話篇。量子論理は分配律が破れることを Python のコードで示し、検索エンジンやレコメンドの程度つき論理として働きます。圏論的量子力学から生まれた ZX 計算は、量子回路の最適化と表面符号の格子手術の記述に使われ、商用の量子コンパイラ TKET の中間表現になっています。トポス的量子力学は、量子重力と量子基礎論の側に効いています。
論理公理系の産業応用 全地図 ── 古典・直観主義・線形・様相・時相・記述・量子論理はどこで使われているのか
https://qiita.com/etale_cohomology/items/b7474b548c61304987c0
21 の論理を一覧表にし、それぞれがどの現場のどの言語で動いているかを地図として描いた記事。SQL の NULL は三値論理、Rust の所有権はアフィン論理、VHDL の std_logic は 9 値の多値論理、TLA+ は時相論理、SNOMED CT は記述論理、というように、論理と道具を対応づけます。言語別対応表に、Dedukti が翻訳の相手とする定理証明支援系が並んでいます。
第 1 章の続き ── では、証明を共有できないのか？
同じ定理が、定理証明支援系の数だけ、別々に証明されています。
たとえば フェルマーの小定理 は、Matita で証明され、HOL Light で証明され、Isabelle/HOL で証明され、Rocq で証明され、Lean で証明されています。それぞれ、ゼロから書かれています。
ある定理証明支援系の証明を、別の定理証明支援系で使えるようにする研究 は、proof interoperability（証明の相互運用）と呼ばれています。
この研究領域には、3つのアプローチ が存在します。
1つ目 は、1 対 1 の直接翻訳です。
HOL Light の証明を Isabelle/HOL へ移す翻訳器の精度は、実用に耐える品質です。
ただし、この 2 つは土台が同じ高階論理です。
土台が違う定理証明支援系のあいだでは、構文を移し替えるだけでは足りません。
論理と論理の対応そのものを設計する必要があります。
2つ目 は、同じ系統の中での共通形式です。
OpenTheory は、HOL系の定理証明支援系のあいだで証明を交換する形式です。
系統の外には出られません。
3つ目 は、論理そのものを記述できる共通の言語を作る やり方です。
土台が違う定理証明支援系の証明も、それぞれの論理ごと、その言語の上に写し取るアプローチです。
本記事の主役 Dedukti は、この 3 番目の道です。
📌 もう一つの見方：証明のバベルの塔 ── 分断の物語として読む
本稿は、Dedukti を「証明検査器の信頼をどこに置くか」という問いから紹介しました。同じ Dedukti を、別の物語として読むこともできます。分断の物語です。
形式化された数学は、いま、定理証明支援系ごとの方言に分断されています。
Lean の Mathlib に入っている定理は、Rocq からは使えません。
Rocq で証明された定理は、Agda からは使えません。
同じフェルマーの小定理が、定理証明支援系の数だけ、別々に、ゼロから書かれています。
数学そのものは、ひとつです。
しかし、形式化された数学は、ひとつではありません。
以前の記事「論理はひとつではない」で、論理には複数の体系があることを見ました。
定理証明支援系の分断は、その帰結です。
定理証明支援系ごとに土台の論理が違うから、証明も定理証明支援系ごとに閉じるのです。
では、多様性を認めたうえで、その先はあるのでしょうか。
多様なまま、行き来はできないのか。
この問いに取り組む研究領域が、本文で述べた proof interoperability です。Dedukti は、その行き来のための共通語の候補です。
人類の言語は、バベルの塔の後もひとつに戻りませんでした。
代わりに、翻訳という営みが生まれました。
形式化された数学も、おそらくひとつには戻りません。
Dedukti が目指しているのは、統一ではなく翻訳です。
第 2 章 ── Logical Framework とは何か？
本稿の冒頭で、Logical Framework の淵源が 1967 年の *Automath にあり、1987 年の Edinburgh LF で言語として定式化されたことを述べました。
本章では、その中身に入ります。
-
Automath と Edinburgh LF のあいだに何があったのか。
-
Edinburgh LF は、どうやって論理体系を記述するのか。何のために使われ、何が足りなかったのか。
順に見ていきます。
Automath から Edinburgh LF へ ── あいだの20年間
Automath（1967年） と Edinburgh LF（1987年） のあいだの経緯を、 Edinburgh LF の原論文の記述から補っておきます。
Edinburgh LF の型システムは、Automath の系譜にあります。
原論文は、LFの形式体系が「依存型を持つ型付きラムダ計算に基づいており、Automath の言語のいくつかと密接に関係している」と述べています。
原論文は、Automath との関係を次のようにも述べています。
Automath は、 どの数学基礎論の立場にも肩入れせずに（without foundational prejudice）、伝統的な数学の推論を形式化 することを目指した。この点で Edinburgh LF の目標は Automath と似ており、Edinburgh LF の仕事は Automath の目標を引き継ぐものと見る ことができる。一方、Automath と違うのは、形式体系を計算機の上で 表現する一般理論を作ろうとする点である。
原論文
R. Harper, F. Honsell, G. Plotkin, "A Framework for Defining Logics", Journal of the ACM, Vol. 40, No. 1, January 1993, pp. 143-184.
https://dl.acm.org/doi/10.1145/138027.138060
初出は次のとおりです。
R. Harper, F. Honsell, G. Plotkin, "A Framework for Defining Logics", Proceedings of the Second Annual IEEE Symposium on Logic in Computer Science (LICS 1987), Ithaca, New York, June 1987, pp. 194-204.
Edinburgh LF のもう 1 つの源流が、Martin-Löf です。
原論文の謝辞に、次のように書かれています。
1986 年春にエディンバラで行われた Martin-Löf の講義が、本研究を触発した。
要旨でも、LF の構文の扱いが「Martin-Löf の arity の体系に似た、しかしより一般的な流儀」であると述べています。
次に出てくる判断（judgement）という概念も、Martin-Löf に由来するものです。
judgements as types という原理は、Edinburgh LF の新しさです。
原論文は、この原理を propositions-as-types のメタ理論版として位置づけています。命題を型に写すのが propositions-as-types なら、判断を型に写すのが judgements as types です。
Edinburgh LF の言語は、依存型を持つラムダ計算 ── λΠ計算 ── です。
この小さな計算体系の上に、さまざまな論理を定義します。
では、どうやって定義するのでしょうか。
本稿の冒頭では、Edinburgh LF が「言語の仕様・理論（ルールブック）」であることまでを述べました。 ここからは、そのルールブックの中身に入ります。
論理体系 を Edinburgh LF で 定義する とき、鍵になるのは、論理の側の概念を型の側の概念に置き換える、という発想 です。
論理の「判断」を、型として表す。
ここでいう 判断（judgement）とは、論理体系の中で「これが成り立っている」と述べる言明のことです。命題そのものとは別のものです。
たとえば「A は命題である」は判断です。
A が命題として正しく組み立てられている、と述べているからです。
「A の証明がある」も判断です。A を証明する手続きが存在する、と述べているからです。
Edinburgh LF は、こうした判断のひとつひとつを、型として表します。
「A は命題である」という判断を、型 prop で表します。
「A の証明がある」という判断を、型 Prf A で表します。
推論規則は、その型を持つ定数として宣言します。
すると、証明は項になり、証明の検査は型検査になります 。
この置き換えを実際に行った .dk ファイルを、連載 2 回目の「仕組み 1 ── 推論規則を、識別子の宣言として記述する」に掲載しました。
prop・Prf・imp を宣言し、含意の導入規則 imp_intro と除去規則 imp_elim を識別子として宣言し、「a ならば a」の証明を項として組み立てたものです。
書き換え規則を使っていないので、中身は Edinburgh LF そのものです。
連載 2 回目に掲載したこの .dk ファイルは、筆者の環境の Dedukti で型検査を通りました（検査の詳細は本記事の末尾の「実機検証について」にまとめます）。
この記事の問題意識に照らしたとき、Edinburgh LF の考え方のコアとなる部分は、これで全部です。
整理すると、以下になります。
- 論理の判断を型に置き換え、推論規則を識別子に置き換え、証明を項に置き換える。
- 証明検査器が行うのは、型検査だけである
Edinburgh LF は、何のために使われたのか
ここで、Edinburgh LF の用途 を押さえておきます。
まず、論理体系をひとつ定義 します。
一階述語論理を使いたいなら、一階述語論理の推論規則を記述したファイルを用意します。
次に、その定義の上で証明を書きます。
そして、書いた証明が正しいかを、型検査によって確かめます。
証明の対象は 2 通りあります。それぞれ、証明を検査する目的は異なります。
1つ目の対象は、一階述語論理や高階論理といった論理体系の中の定理です。
一階述語論理の推論規則を記述したファイルを用意したなら、その一階述語論理の上で「A かつ B ならば B かつ A」といった定理を証明します。
この場合に知りたいのは、その定理が、一階述語論理や高階論理といった論理体系の推論規則だけから導けるかどうか です。
導けるなら証明は型検査を通り、導けないなら型検査は失敗します。
たとえば直観主義論理の推論規則を記述したファイルの上で二重否定除去を証明しようとすると、型検査は失敗します。直観主義論理の推論規則からは導けないからです。
この場合の目的は、その定理を導くために、どの推論規則が必要かということであり、一階述語論理や高階論理といった論理体系そのものの性質を深く研究すること です。
一方、古典論理の推論規則を記述したファイルの上では、二重否定除去の型検査を通ります。同じ定理を、一階述語論理、直観主義論理、古典論理と差し替えて試すことで、それぞれの論理体系の境界が分かります。
定理そのものを新しく得ることが目的ではありません。
「A かつ B ならば B かつ A」が成り立つことは、はじめから分かっています。
2 つ目の対象は、一階述語論理や高階論理といった論理体系そのものについての性質です。
「この型システムには型の安全性が成り立つ」
「この体系のこの規則は、他の規則から導ける」
といった定理です。
一階述語論理 の中で証明する のではなく、一階述語論理 について証明します 。
Twelf の論文は、これを メタ理論 と呼んでいます。
この場合に知りたいのは、記述した論理体系そのものが、望ましい性質を持つかどうか です。
プログラミング言語の型システムを記述したなら、 「型の付いたプログラムは実行時にエラーで止まらない」という性質を知りたい。
論理体系を記述したなら、 「矛盾が導けない」という性質を知りたい 。
こうした性質を、証明として書き、型検査で確かめます。
2つ目の用途が、Edinburgh LF の特色 です。
一階述語論理や高階論理といった 論理体系そのものを研究の対象に できます。複数の論理体系を同じ言語の上に記述すれば、体系どうしを比べることもできます。
いずれの場合も、証明を書くのは Edinburgh LF の上です。
Lean 4 や Rocq が出力した証明を持ち込んで検査する、という使い方ではありません。
Edinburgh LF と Dedukti の目的の違い
ここで、本記事の冒頭に掲げた表を再掲します。
| 名前 | ルールブック（記述する側） | 検査するプログラム | どこで書かれた証明を検査するか |
|---|---|---|---|
| Automath | Automath の言語。数学の証明を記述するための形式言語 | Automath の検査プログラム | Automath の中で書かれた証明 |
| Edinburgh LF | Edinburgh LF の文法（λΠ計算）。論理体系の推論規則を記述する | ── （言語の仕様であり、プログラムではない） | ── |
| Twelf | Edinburgh LF の文法（λΠ計算） | Twelf | Edinburgh LF の文法に従って書かれた証明 |
| Isabelle | Isabelle/Pure というメタ論理。その上に対象論理として HOL・ZF・FOL が載る | Isabelle の証明検査器（LCF 方式） | Isabelle の中で書かれた証明 |
| Dedukti | λΠ計算 modulo rewriting。翻訳器が同梱する符号化ファイルに、Lean 4 の型理論などが記述される | Dedukti の証明検査器 | Lean 4・Rocq など、外部の定理証明支援系が出力した証明項 |
いちばん右の列 に注目してください。
Dedukti だけが、外部の定理証明支援系が出力した証明項を検査の対象にしています。
他の 4 つは、いずれも自分の上で書かれた証明を検査します。
この違いは、何に由来するものでしょうか？
Dedukti の 目的 は、定理証明支援系が出力した証明を、別の証明検査器で再検証すること です。だから翻訳器が必要になります。
Edinburgh LF の目的は、そうではありません。
1987 年の論文が扱っているのは、論理体系そのもの です。
一階述語論理や高階論理といった論理体系を、ひとつの言語の上に定義し、比較し、その性質を調べる。これが目的 です。
当時、Lean 4 も Rocq も存在せず、他の定理証明支援系が出力した証明を再検証するという課題は、まだ立っていませんでした 。
Dedukti は、Edinburgh LF の言語 λΠ計算に書き換え規則を足したものです。
言語の系譜としては Edinburgh LF に連なりますが、目的は違います。
Edinburgh LF に足りなかったもの
Edinburgh LF には、書き換え規則がありません。
このため、計算を型検査に組み込んでいる体系 ── Lean 4 や Rocq が立脚する型理論 ── を記述すると、計算の等しさを 1 つずつ定理として証明し、証明項の中で明示的に使うことが必要 となります。結果として、証明項は大きくなり、元の証明とは形が離てしまう のです。
Dedukti は、λΠ計算に書き換え規則を加えました。
その結果、Dedukti は、対象の論理体系や型理論が持つ計算の規則を、書き換え規則として記述できるようになりました。
Deduktiの型検査器が、その書き換えを型検査の中で行います 。
連載 2 回目の「仕組み 2 ── 計算による等しさを、書き換え規則で吸収する」で見たとおりです。
この違いが、Dedukti が Edinburgh LF の系譜に属しながら、Lean 4 や Rocq の型理論まで扱える理由です。
Edinburgh LF は、いまも使われているのか
結論から申し上げると、いまでも使われています。
本稿の冒頭で述べた Twelf が、いまも Linux ディストリビューションのパッケージとして配布 されています。ただし、Twelf 本体の版は 1.7.1 で止まっており、開発が活発とは言えません。
Twelf が実際に何に使われたか、代表的な実績を挙げます。
Standard ML の型安全性の形式化。
Lee・Crary・Harper が 2007 年の国際会議 POPL で報告しました。
Standard ML と同じ表現力を持つ内部言語を定義し、その型安全性の証明を Twelf で機械検査したもの です。半透明モジュール、抽象化、多相、高階の種、参照、例外、再帰型、再帰関数といった、Standard ML の実装に必要な仕組みをすべて含んでいます。
POPLmark チャレンジ。
プログラミング言語の設計 にあたって、その言語のメタ理論を計算機で検査できるようにしよう、という共同の課題 です。2005 年に提案されました。
Twelf による 全問の解答が、カーネギーメロン大学のチームから提出されています。
ML への依存型の導入。
Licata と Harper の研究で、ML系の型システムに依存型の一種を加えたものです。メタ理論の大部分が Twelf で機械化 されています。
いずれも、プログラミング言語そのものの性質を証明する仕事 です。
Lean 4 や Rocq が出力した証明を持ち込んで再検査する、という使い方ではありません。
Twelf については、記事末尾のコラムで、Dedukti との用途の違いをさらに扱います。
出典
- D. Lee, K. Crary, R. Harper, "Towards a mechanized metatheory of Standard ML", POPL 2007. https://dl.acm.org/doi/10.1145/1190216.1190245
- B. Aydemir et al., "Mechanized Metatheory for the Masses: The PoplMark Challenge", TPHOLs 2005. https://www.seas.upenn.edu/~plclub/poplmark/poplmark.pdf
- Twelf 公式サイト「Research projects using Twelf」 https://twelf.org/wiki/research-projects-using-twelf/
第 3 章 ── Isabelle は、実はここにいる
Logical Framework は、新しい発想ではありません。
読者の皆様の多くがご存知の定理証明支援系が、すでにこの発想の上に建っています。
Isabelle がそうです。
Isabelle/HOL という名前は、2 つの部分から成ります。
Isabelle と HOL です。
Isabelle の中核は Isabelle/Pure と呼ばれる小さなメタ論理 で、直観主義の高階論理です。
Pure 自体 は、数学の証明を書くための論理ではありません。
論理を定義するための論理 です。
その上に、object logic（対象論理）が定義されます 。HOL がその 1 つです。
集合論 ZF も、一階論理 FOL も、同じ Pure の上に定義 されています。
利用者（定理証明プログラマ）は、 Isabelle/HOL を使っていて Pure を意識しませんが、HOL は Pure の上の 1 つの定義 なのです。
本稿執筆者が過去に公開済みの記事「依存型を使わない Isabelle/HOL とは何か」（https://qiita.com/etale_cohomology/items/6987c76966a3513cd6e0）で Isabelle/HOL を扱ったとき、この構造には触れました。
本稿は、その構造を Logical Framework の実例として読み直します。
Isabelle と Dedukti は、「特定の対象論理に閉じない」という思想を共有しています。
違うのは、実現の方法 です。
Pure は高階論理をメタ論理に選び、推論を高階の単一化で進めます。
Dedukti は依存型のラムダ計算をメタ論理に選び、そこに書き換え規則を加えます。
なお、Isabelle が証明を検査する部分は、LCF 方式で作られた小さなプログラムです。対象論理が HOL であっても ZF であっても、そのプログラムが行うことは変わりません。この点も、Dedukti と共通します。
記述する側を差し替えられる、という共通点
ここで、本稿の冒頭に掲げた表を、もう一度再掲します。
| 名前 | ルールブック（記述する側） | 検査するプログラム | どこで書かれた証明を検査するか |
|---|---|---|---|
| Automath | Automath の言語。数学の証明を記述するための形式言語 | Automath の検査プログラム | Automath の中で書かれた証明 |
| Edinburgh LF | Edinburgh LF の文法（λΠ計算）。論理体系の推論規則を記述する | ── （言語の仕様であり、プログラムではない） | ── |
| Twelf | Edinburgh LF の文法（λΠ計算） | Twelf | Edinburgh LF の文法に従って書かれた証明 |
| Isabelle | Isabelle/Pure というメタ論理。その上に対象論理として HOL・ZF・FOL が載る | Isabelle の証明検査器（LCF 方式） | Isabelle の中で書かれた証明 |
| Dedukti | λΠ計算 modulo rewriting。翻訳器が同梱する符号化ファイルに、Lean 4 の型理論などが記述される | Dedukti の証明検査器 | Lean 4・Rocq など、外部の定理証明支援系が出力した証明項 |
Twelf、Isabelle、Dedukti の 3 つに共通するのは、ルールブックの側を差し替えられること です。
検査するプログラムの側は、差し替えても変わりません。
Twelf なら、一階述語論理を記述したファイルを読み込むか、高階論理を記述したファイルを読み込むかで、扱える論理体系が変わります。
Isabelle なら、対象論理として HOL を載せるか ZF を載せるかで変わります。
Dedukti なら、読み込む符号化ファイルが Lean 4 用か HOL Light 用かで変わります。
これが Logical Framework という 考え方の中身 です。
対話篇 ── Isabelle はなぜ Dedukti にならなかったのか
タロウくん：
先生、ひとつ引っかかっています。
Isabelle も Dedukti も、論理体系を記述する側と、検査する側を分けています。
同じ考え方なら、Isabelle でもよかったのではないですか。
なぜ Isabelle は、Pure に書き換え規則を足して Dedukti のようにならなかったのですか。
専任講師：
その問いに、私は答えを持ち合わせていません。
調べましたが、Isabelle の開発陣が書き換え規則を足さなかった理由を、公開資料の中に見つけられませんでした。分かったのは、Isabelle の設計が別の系譜から来ている、という事実だけです。
Paulson が 1985 年に書いた論文の要旨には、Isabelle が Martin-Löf の
構成的型理論の定理を証明するために使われた、と記されています。
一方、Dedukti は Automath と Edinburgh LF の系譜から来ています。
つまり、出発点が違うんです。
タロウくん：
出発点が違うから、というだけですか？
専任講師：
それ以上のことは、私には分かりません。
推測はできます。
Isabelle が Pure に選んだのは高階論理で、推論を高階の単一化で進める作りです。Dedukti が選んだのは依存型のラムダ計算で、書き換え規則を型検査の中で走らせる作りです。
この 2 つは、そもそも噛み合わないのかもしれません。
しかし、これは私の推測です。裏づけを見つけていません。
答えられないことは、答えられないと申し上げます。
出典
- L. Paulson, "Formalising Mathematics In Simple Type Theory", arXiv:1804.07860. https://arxiv.org/abs/1804.07860
Dedukti 以外の Logical Framework
Logical Framework という考え方 は、Dedukti と Isabelle だけのものではありません。
ほかにどのような仕組みがあり、それぞれ何のために使われているのかを、コラムにまとめました。
📌 Dedukti 以外にも、λΠ計算 modulo rewriting と Logical Framework を組み込む翻訳の仕組みはあるか？
質問を 2 つに分けて答えます。
1つ目は「λΠ計算 modulo rewriting を使う仕組みは Dedukti 以外にあるか」です。
2つ目は「Logical Framework を使って証明を翻訳する仕組みは Dedukti 以外にあるか」です。
1 つ目 ── λΠ計算 modulo rewriting を使う仕組み
Lambdapi があります。
Dedukti と同じ λΠ計算 modulo rewriting の上に作られた、後発のプログラムです。Dedukti と .dk ファイルをやり取りできます。
筆者の環境でも、Lambdapi が書き出した .dk ファイルを Dedukti が型検査で受け入れることを確かめています。
λΠ計算 modulo rewriting を使う仕組みは、筆者が調べた公開資料の範囲では、Dedukti と Lambdapi の 2つ です。
書き換え規則を持つ点が、後述の Twelf や MMT との違いです。
2 つ目 ── Logical Framework を使って証明を翻訳する仕組み
こちらは複数あります。4 つ挙げます。
Twelf。
Edinburgh LF の言語を読み込むプログラムです。
Pfenning と Schürmann が 1999 年の国際会議 CADE で報告しています。
メタ言語は λΠ計算です。
書き換え規則はありません。このため、計算を型検査に組み込んでいる体系を記述すると、計算の等しさを証明項の中で明示する必要が出ます。
LFSC（Logical Framework with Side Conditions）。
Edinburgh LF に side condition ── 型検査の途中で走る、小さな計算の手続き ── を足したものです。Stump ほかが報告しています。
対象は SMT 充足可能性判定器の証明です。
cvc5 などの SMT 判定器が出力した証明を、LFSC の証明検査器が検査します。
Dedukti が定理証明支援系のメタ言語として働くのと同じ役割を、LFSC は SMT 判定器に対して 果たします。
MMT（Meta-Meta-Theory / Meta-Meta-Tool）。
Rabe と Kohlhase らが開発した枠組みです。
MMT は、関数型も命題も組み込んでいません。
Edinburgh LF そのものも、MMT の中の 1 つの理論として記述します 。
LATIN および LATIN2 という計画 で、多数の論理を Edinburgh LF の上に記述した「論理の地図」（Logic Atlas）を作っています。
EuroProofNet では、Dedukti と MMT を比較する研究も行われています。
Isabelle/Pure。
本記事の第 3 章で扱いました。
Isabelle は、Pure と呼ばれるメタ論理の上に、HOL や ZF といった対象論理を載せる作りになっています。
Logical Framework の考え方が、広く使われている定理証明支援系の中にすでに入っている例です。
Twelf、LFSC、MMT は、Dedukti と同じ用途で使われているのか
同じ用途とは、次のことです。
論理体系と型理論が異なる複数の定理証明支援系が検証した証明を、論理的な共通言語に翻訳し、元の定理証明支援系とは別のプログラムで再検証する。
3つの構成要件を、1つずつ見ていきます。
Twelf ── 用途が違います。
Twelf の主な用途は、論理体系そのもの を記述し、その論理体系について 成り立つ性質を証明することです。
たとえば「この型システムには型の安全性が成り立つ」という性質を、Twelf の上で証明します。
Lean 4 や Rocq が検証した証明を Twelf に翻訳し、Twelf で再検証するという使い方は、筆者が調べた公開資料の範囲では確認できませんでした。
Twelf のメタ言語には書き換え規則がありません。
Lean 4 や Rocq の定義的等価性（definitional equality）を記述するには、計算の等しさを証明項の中で明示する必要が出ます。
この点が、Dedukti が Edinburgh LF に書き換え規則を足した理由です。
LFSC ── 用途は同じですが、対象が違います。
LFSC は、証明を翻訳して別のプログラムで再検証するために使われています 。
この点は Dedukti と同じです。
違うのは、対象 です。
LFSC の対象は SMT 充足可能性判定器 です。
cvc5 などの SMT 判定器が出力した証明を、LFSC の証明検査器が検査します。
Dedukti の対象は定理証明支援系 です。Lean 4、Rocq、Agda、HOL Light などが出力した証明を扱います。
同じ考え方を、SMT 判定器に向けたものが LFSC、
定理証明支援系に向けたものが Dedukti、という関係です。
MMT ── 用途は重なりますが、重点が違います。
MMT は、複数の定理証明支援系のライブラリを 1 つの形式に翻訳しています。
OAF 計画（Open Archive of Formalization）で、Coq、HOL Light、IMPS、Isabelle、Mizar、PVS の 6 つのライブラリを OMDoc/MMT 形式に翻訳しました。
翻訳の対象が複数の定理証明支援系である点は、Dedukti と同じ です。
違うのは、翻訳したあとに何をするか です。
Dedukti の重点は、翻訳した証明を Dedukti の証明検査器にかけ、型検査を通すか拒否するかを判定することです。
MMT の重点は、翻訳した内容を検索し、ライブラリ間で同じ概念を対応づけ、依存関係を管理すること です。
MMT はこうした作業を 知識管理 と呼んでいます。
MMT でも型検査と証明検査は行えますが、Isabelle の輸出に関する報告では、独立した証明検査は応用の 1 つとして挙げられています。
EuroProofNet では、2025 年に Dedukti と MMT を比較する研究が行われています。両者の位置づけは、まだ整理の途中です。
3 つを比べると
Dedukti と同じ用途で使われているのは LFSC です。
ただし LFSC の対象は SMT 判定器であり、定理証明支援系ではありません。
MMT は対象が重なりますが、重点が知識管理にあります。
Twelf は用途が違います。
論理体系と型理論が異なる複数の定理証明支援系の証明を翻訳し、独立に再検証することを主目的に置いた仕組みは、筆者が調べた公開資料の範囲では Dedukti と Lambdapi です 。
Logical Framework を使わない翻訳の仕組みもあります
OpenTheory があります。
HOL Light、HOL4、ProofPower といった 高階論理の定理証明支援系のあいだで、証明を共有するための仕組み です。
対象を高階論理の一族に絞っているため、メタ言語を挟みません。
Keller と Werner による HOL Light から Coq への翻訳も、Logical Framework を使っていません。
この節のまとめ
Logical Framework という考え方 を使う仕組みは、Dedukti のほかに Twelf、LFSC、MMT、Isabelle/Pure があります。このうち、λΠ計算に書き換え規則を足した仕組みは Dedukti と Lambdapi です。書き換え規則があることが、Lean 4 や Rocq のように計算を型検査に組み込んだ体系を扱えることにつながります。
出典
- R. Harper, F. Honsell, G. Plotkin, "A framework for defining logics", Journal of the ACM 40(1), 1993, pp. 143-184. https://dl.acm.org/doi/10.1145/138027.138060
- F. Pfenning, C. Schürmann, "System description: Twelf — a meta-logical framework for deductive systems", CADE 1999. https://www.cs.cmu.edu/~fp/papers/cade99.pdf
- M. Wenzel, L. Paulson, T. Nipkow, "The Isabelle Framework", TPHOLs 2008.
- A. Stump et al., "SMT proof checking using a logical framework", Formal Methods in System Design, 2013.
- F. Rabe, "MMT: A Foundation-Independent Logical Framework", 2018. https://kwarc.info/people/frabe/
- M. Kohlhase, F. Rabe et al., "Experiences from Exporting Major Proof Assistant Libraries", Journal of Automated Reasoning, 2021. https://arxiv.org/abs/2005.03089
- M. Kohlhase et al., "Making Isabelle Content Accessible in Knowledge Representation Formats", TYPES 2019. https://arxiv.org/abs/2005.08884
- T. Felicissimo, "Adequate and computational encodings in the logical framework Dedukti", arXiv:2205.02883. https://arxiv.org/abs/2205.02883
- EuroProofNet WG1, "From Dedukti to MMT: A Comparative Study of Modular Frameworks for Logical Systems", 2025. https://europroofnet.github.io/wg1/
ここまでのまとめ
この記事は、次の 4 点を述べました。
1 点目。
de Bruijn は、証明を 小さな独立した プログラムで検査できる形にしておく べき だと考えました。この考え方を de Bruijn 基準 と呼びます。
2 点目。
定理証明支援系は、それぞれ違う論理の上に建っています。同じ定理が、定理証明支援系の数だけ別々に証明されています。
3 点目。
Logical Framework は、論理そのものを記述するための言語です。
1987年のEdinburgh LF に始まります。
論理の判断を型として表し、推論規則を識別子として宣言し、証明の検査を型検査に還元します。
Edinburgh LF の用途は、論理体系そのものを研究することでした。他の定理証明支援系の証明を受け取って再検証する用途ではありません。
4 点目。
Logical Framework の考え方は、Isabelle の中にもすでに入っています。Isabelle/Pure というメタ論理の上に、HOL や ZF が載っています。Edinburgh LF、Isabelle、Dedukti のいずれも、論理体系を記述する側を差し替えられ、検査する側は変わりません。Dedukti のほかに、Twelf、LFSC、MMT があります。
次回記事へ
次回の記事では、Dedukti の実績と限界 を扱います。
Dedukti の研究は 1998 年から続いています。
それにもかかわらず、産業界での配備実績を、筆者は公開資料の範囲では確認できませんでした。
年表、翻訳器の一覧、実際に翻訳された証明、利用者、GitHub の指標を並べ、何ができていて何ができていないのか を、そのままお伝えします。
📌 用語のミニ解説
📌 本文に登場した定理証明支援系・翻訳器・考え方の、初心者向けミニ解説
Logical Framework（ロジカル・フレームワーク）
論理そのものを記述するための言語です。ふつうの定理証明支援系は、1 つの論理を組み込んでいます。Logical Framework は、論理を定義の対象として扱います。1987 年の Edinburgh LF（Harper・Honsell・Plotkin）が源流で、本記事の Dedukti はこの系譜の現在形の 1 つです。
λProlog（ラムダ・プロローグ）
論理プログラミング言語 Prolog の拡張で、高階の項と束縛を扱えます（Miller・Nadathur）。論理を記述する用途にも使われるため、論理プログラミング型の Logical Framework と位置づけられます。Dedukti との違いは、計算機が何を実行するかです ── λProlog は導出の探索を実行し、Dedukti（dkcheck）は型検査だけをします。実装の 1 つ ELPI は、Rocq のタクティク開発にも使われています。
Matita（マティータ）
イタリアのボローニャ大学で開発された定理証明支援系です。Rocq と同じ CIC（帰納構成計算）の系統ですが、小さく作られており、証明項が取り出しやすい構造をしています。本記事に登場した「Dedukti 経由で複数の体系へ翻訳された算術ライブラリ」は、Matita で書かれたものです。
HOL Light（ホル・ライト）
高階論理（HOL）系の定理証明支援系です（John Harrison）。検査の核が数百行と極めて小さいことで知られます。実解析・複素解析のライブラリ Multivariate を持ち、ケプラー予想の形式証明（Flyspeck 計画）にも使われました。本記事の「2 万定理超を Rocq へ翻訳」の翻訳元です。
CoqInE（コック・イン・イー）
Rocq（旧 Coq）の証明を Dedukti へ翻訳する変換器です。Rocq のプラグインとして作られており、標準ライブラリの一部を翻訳した実績があります。
Zenon Modulo（ゼノン・モジュロ）
一階論理の自動証明器 Zenon の拡張です。deduction modulo を組み込み、見つけた証明を Dedukti 形式で出力できます。探索は自動証明器、検査は Dedukti、という分業の実例です。
BWare（ビーウェア）
フランスの研究プロジェクトです（2012〜2016 頃）。B メソッド ── 鉄道など安全性が問われる分野で使われてきた形式手法 ── の証明義務を、自動証明器で証明し、Dedukti で独立に検査する流れを研究しました。産業の題材に最も近づいた事例ですが、研究プロジェクトであって産業配備そのものではありません。
predicate subtyping と PVS（述語による部分型）
PVS は米国 SRI で開発された定理証明支援系で、航空宇宙分野の検証で広く使われてきました。その特徴が predicate subtyping ── 「0 でない実数」のように、述語で絞り込んだ部分型を作れる仕組みです。強力な半面、型検査が決定不能になります。この珍しい機能をどう符号化するかが、Dedukti 研究の題材になっています。
matching logic と K（マッチング論理）
K は、プログラミング言語の意味論を定義するための枠組みです。C・Java・イーサリアムの EVM などの意味論が K で定義されてきました。その論理的基盤が matching logic です。これも Dedukti への符号化の研究対象になっています。
de Bruijn 因子（de Bruijn factor）
序章の de Bruijn 基準（criterion）とは別の概念です。形式化した数学の長さを、元の非形式の文章の長さで割った比を指します。Wiedijk が名づけました。形式化すると文章が何倍に膨らむか、という量です。基準は「証明を独立に検査できるか」、因子は「どれだけ膨らむか」で、名前だけが同じです。出典：F. Wiedijk, "The De Bruijn Factor", 2000. https://www.cs.ru.nl/~freek/factor/
実機検証について
本記事で参照したコードは、すべて筆者の環境で実行しました。
検証できたことと、できなかったことを分けて記します。
検証環境
| 構成要素 | 版 | 入手経路 |
|---|---|---|
| OS | Ubuntu 24.04 | ─ |
| OCaml | 4.14.1 | apt |
| dune | 3.14.0 | apt |
| menhir | 20231231 | apt |
| Dedukti | v2.7（タグ） | GitHub Deducteam/Dedukti をソースビルド |
| Lambdapi | 2.5.1（タグ）＋改変 | GitHub Deducteam/lambdapi をソースビルド |
| bindlib | 6.0.0 | GitHub からソースビルド |
| pratter | 3.0.1 | GitHub からソースビルド |
| why3 | 1.6.0 | apt |
検証できたこと
- 連載 2 回目の「仕組み 1」で扱った Edinburgh LF 版のファイル（
lf.dk）は、筆者の環境の Dedukti v2.7 のdk checkで型検査を通った。
検証できなかったこと・注意
- Dedukti と Lambdapi の開発版（master）は dune 3.18 以上を要求し、Ubuntu 24.04 の dune 3.14 ではビルドできなかった。安定タグを使った。
- Dedukti の README は「opam の版は古いので、リポジトリを clone してインストールすることを推奨する」と述べている。筆者の経験と一致する。
- CoqInE、hol2dk、isabelle_dedukti などの翻訳器は、筆者の環境では実行していない。本記事に登場する翻訳器についての記述は、一次資料に基づく。
Lambdapi を用いた検査は、後の回に記します。
検証に使ったファイルの全文は、連載 2 回目の記事に掲載しました。
訂正一覧
公開後に訂正した箇所を、ここに追記していきます。現時点ではありません。
関連記事
本記事の接続先
- 論理はひとつではない ── 圏論論理学がつなぐ量子論理・トポス・圏論的量子力学 https://qiita.com/etale_cohomology/items/24858c3bd7c7d6833eaa
- if 文も SQL も、実は別々の「論理」だった ── 古典論理から量子論理まで、21 の論理体系を 5 人で議論【対話篇】 https://qiita.com/etale_cohomology/items/4fadbda1ebea7a63f68d
- 依存型を使わない Isabelle/HOL とは何か ── AWS のクラウド基盤を検証した定理証明系は、なぜ証明を自動で探せるのか
https://qiita.com/etale_cohomology/items/6987c76966a3513cd6e0
Isabelle/Pure という枠組みの上に HOL・ZF・FOL を載せる構造、sledgehammer による自動化、Isar 記法、seL4 と AWS Nitro Isolation Engine の検証を扱っています。本記事の第 3 章の背景です。
- トポスと論理の関係 ── ひとつのトポス（数学の宇宙）を選ぶと、なぜ古典論理か直観主義論理が決まるのか ── そして、トポス以外の「器」たち https://qiita.com/etale_cohomology/items/5206679c2fd02aea9512
- λProlog とは何か ── AI が数学を証明する時代、定理証明系 Rocq の内側で働く知られざる言語
https://qiita.com/etale_cohomology/items/98b416523f468dc64959
Prolog を高階論理と単純型付きラムダ計算で拡張した言語、その実装 ELPI、Rocq の拡張言語 Coq-Elpi、高階抽象構文（HOAS）を扱っています。本記事で挙げる論理プログラミング型の枠組みの詳細です。
数珠つなぎ連載（型理論から立方体型理論へ）
- 初回 https://qiita.com/etale_cohomology/items/365356fa41ed7b4d7829
- 2 本目 https://qiita.com/etale_cohomology/items/e3eae170f14f134c8f13
- 3 本目 https://qiita.com/etale_cohomology/items/f2aa70cdc826e15979a4
- 4 本目 https://qiita.com/etale_cohomology/items/75aa5395b5f8c03e1bf2
📚 Arend 連載（全 8 本）
- https://qiita.com/etale_cohomology/items/0abc51fe5e2a3eb02f08
- https://qiita.com/etale_cohomology/items/8126e8eae37eefdf86f6
- https://qiita.com/etale_cohomology/items/61193814df628ace0bf7
- https://qiita.com/etale_cohomology/items/679faed081b6cd8be97c
- https://qiita.com/etale_cohomology/items/865503fbcfc68b23d759
- https://qiita.com/etale_cohomology/items/e80c18c3c35460f316b7
- https://qiita.com/etale_cohomology/items/543ba6180aef46a21cbe
- https://qiita.com/etale_cohomology/items/3b332aa9c22ebe838c5c
出典一覧
- R. Harper, F. Honsell, G. Plotkin, "A Framework for Defining Logics", Journal of the ACM 40(1), 1993.
- D. Cousineau, G. Dowek, "Embedding Pure Type Systems in the lambda-Pi-calculus modulo", TLCA 2007. https://arxiv.org/abs/2310.12540
- A. Assaf, "Conservativity of Embeddings in the lambda Pi Calculus Modulo Rewriting", TLCA 2015. https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.31
- G. Dowek, "Models and Termination of Proof Reduction in the lambda Pi-Calculus Modulo Theory", ICALP 2017. https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2017.109
- T. Felicissimo, "Adequate and Computational Encodings in the Logical Framework Dedukti", FSCD 2022. https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.25
- G. Dowek, F. Thiré, "Logipedia: a multi-system encyclopedia of formal proofs", 2023. https://arxiv.org/abs/2305.00064
- Deducteam/Dedukti（GitHub）. https://github.com/Deducteam/Dedukti
- Deducteam/lambdapi（GitHub）. https://github.com/Deducteam/lambdapi
- Deducteam/isabelle_dedukti（GitHub）. https://github.com/Deducteam/isabelle_dedukti
- Deducteam/Agda2Dedukti（GitHub）. https://github.com/Deducteam/Agda2Dedukti
- Deducteam/Dedukti Issue #224. https://github.com/Deducteam/Dedukti/issues/224
- EuroProofNet（公式サイト）. https://europroofnet.github.io/
- EuroProofNet, Tools. https://europroofnet.github.io/tools/
- EuroProofNet, Deliverables 1 and 13. https://europroofnet.github.io/deliverable1/
- EuroProofNet, Deliverable 5. https://europroofnet.github.io/deliverable5/
- EuroProofNet, LFPSI 2025（国際スクール）. https://europroofnet.github.io/LFPSI25/
- J. Cockx, "How to write a translator to Dedukti: The case of Agda"（講演資料）, 2022. https://europroofnet.github.io/_pages/WG1/Jun2022/thiago_and_jesper.pdf
- A. Ranta, "Symbolic Informalization: Fluent, Productive, Multilingual", arXiv:2606.16893, 2026 年 6 月 15 日投稿. https://arxiv.org/abs/2606.16893
- 同論文の日本語版（alphaXiv による訳題「記号的非形式化：流暢、生産的、多言語」。要約は自動生成）. https://www.alphaxiv.org/ja/abs/2606.16893
- F. Wiedijk, "The De Bruijn Factor", 2000. https://www.cs.ru.nl/~freek/factor/
- G. Klein et al., "seL4: Formal Verification of an OS Kernel", SOSP 2009. https://dl.acm.org/doi/10.1145/1629575.1629596
- G. Gonthier et al., "A Machine-Checked Proof of the Odd Order Theorem", ITP 2013, LNCS 7998. https://link.springer.com/chapter/10.1007/978-3-642-39634-2_14
- T. Hales et al., "A formal proof of the Kepler conjecture", Forum of Mathematics Pi, arXiv:1501.02155. https://arxiv.org/abs/1501.02155
- T. Hales, "The Formal Proof of the Kepler Conjecture: a critical retrospective", arXiv:2402.08032. https://arxiv.org/abs/2402.08032
- Inria, Deducteam 2024 Activity Report. https://radar.inria.fr/rapportsactivite/RA2024/deducteam/DEDUCTEAM-RA-2024.pdf