Importing HOL into Isabelle/HOL

Steven Obua; Sebastian Skalberg

doi:10.1007/11814771_27

Importing HOL into Isabelle/HOL

Steven Obua, Sebastian Skalberg

School of Informatics

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

We developed an importer from both HOL 4 and HOL-light into Isabelle/HOL. The importer works by replaying proofs within Is- abelle/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.

Original language	English
Title of host publication	Automated Reasoning
Subtitle of host publication	Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006. Proceedings
Editors	Ulrich Furbach, Natarajan Shankar
Publisher	Springer Berlin Heidelberg
Pages	298-302
Number of pages	5
ISBN (Electronic)	978-3-540-37188-5
ISBN (Print)	978-3-540-37187-8
DOIs	https://doi.org/10.1007/11814771_27
Publication status	Published - 2006

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Berlin Heidelberg
Volume	4130
ISSN (Print)	0302-9743

Access to Document

10.1007/11814771_27

http://dx.doi.org/10.1007/11814771_27

Cite this

@inproceedings{d240f69fdb604916bdf6966f4c566edd,

title = "Importing HOL into Isabelle/HOL",

abstract = "We developed an importer from both HOL 4 and HOL-light into Isabelle/HOL. The importer works by replaying proofs within Is- abelle/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. ",

author = "Steven Obua and Sebastian Skalberg",

year = "2006",

doi = "10.1007/11814771_27",

language = "English",

isbn = "978-3-540-37187-8",

series = "Lecture Notes in Computer Science",

publisher = "Springer Berlin Heidelberg",

pages = "298--302",

editor = "Ulrich Furbach and Natarajan Shankar",

booktitle = "Automated Reasoning",

}

Importing HOL into Isabelle/HOL. / Obua, Steven; Skalberg, Sebastian.

Automated Reasoning: Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006. Proceedings. ed. / Ulrich Furbach; Natarajan Shankar. Springer Berlin Heidelberg, 2006. p. 298-302 (Lecture Notes in Computer Science; Vol. 4130).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Importing HOL into Isabelle/HOL

AU - Obua, Steven

AU - Skalberg, Sebastian

PY - 2006

Y1 - 2006

N2 - We developed an importer from both HOL 4 and HOL-light into Isabelle/HOL. The importer works by replaying proofs within Is- abelle/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.

AB - We developed an importer from both HOL 4 and HOL-light into Isabelle/HOL. The importer works by replaying proofs within Is- abelle/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.

U2 - 10.1007/11814771_27

DO - 10.1007/11814771_27

M3 - Conference contribution

SN - 978-3-540-37187-8

T3 - Lecture Notes in Computer Science

SP - 298

EP - 302

BT - Automated Reasoning

A2 - Furbach, Ulrich

A2 - Shankar, Natarajan

PB - Springer Berlin Heidelberg

ER -