Importing HOL into Isabelle/HOL

被引：0

作者：

Obua, Steven ^{[1
]}

Skalberg, Sebastian ^{[1
]}

机构：

[1] Tech Univ Munich, D-85748 Garching, Germany

来源：

AUTOMATED REASONING, PROCEEDINGS | 2006年 / 4130卷

关键词：

D O I：

暂无

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

We developed an importer from both HOL 4 and HOL-light into Isabelle/HOL. The importer works by replaying proofs within Isabelle/HOL that have been recorded in HOL 4 or HOL-light and is therefore completely safe. Concepts in the source HOL system, that is types and constants, can be mapped to concepts in Isabelle/HOL; this facilitates a true integration of imported theorems and theorems that are already available in Isabelle/HOL. The importer is part of the standard Isabelle distribution.

引用

页码：298 / 302

页数：5