이사벨 패럴렐 코퍼스

병렬 코퍼스는 한 언어의 텍스트와 다른 언어의 해당 텍스트를 짝지어 모아놓은 것입니다.

Isabelle Parallel Corpus(IPC)는 Isabelle 문서의 병렬 코퍼스를 만드는 커뮤니티 주도 이니셔티브입니다. IPC는 Isabelle의 공식 문서(정리, 보조정리, 정의 등)와 자연어 대응 문서를 연결합니다.

IPC 항목에는 여러 수준의 데이터 주석이 있습니다. 첫 번째 수준에서는 문서의 자연어 진술(예: 정리 진술)과 자연어 출처(예: 교과서)가 기록됩니다. 두 번째 수준의 주석은 자연어 증명의 문장과 해당 Isabelle 증명 스크립트의 진술을 쌍으로 묶습니다. 세 번째 수준의 주석을 통해 자연어의 단어를 이사벨 증명 스크립트의 토큰에 맞춰 정렬할 수 있습니다.