対訳コーパスは、ある言語のテキストと別の言語の対応するテキストを組み合わせたコレクションです。

Isabelle Parallel Corpus (IPC) は、Isabelle 文書の並列コーパスを作成するためのコミュニティ主導の取り組みです。 IPC は、Isabelle の形式的な文書 (定理、補題、定義など) を自然言語に対応するテキストと組み合わせます。

IPC のエントリには複数レベルのデータ注釈があります。第 1 レベルでは、文書の自然言語ステートメント (定理ステートメントなど) と自然言語ソース (教科書など) が記録されます。注釈の第 2 レベルは、自然言語証明の文と、イザベル証明スクリプトの対応するステートメントを組み合わせます。注釈の 3 番目のレベルでは、自然言語の単語と Isabelle の証明スクリプト内のトークンの位置合わせが可能になります。