An Isabelle-Like Procedural Mode for HOL Light

Petros Papapanagiotou; Jacques Fleuriot

doi:10.1007/978-3-642-16242-8_40

An Isabelle-Like Procedural Mode for HOL Light

Petros Papapanagiotou, Jacques Fleuriot

School of Informatics

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

Abstract

HOL Light is a modern theorem proving system characterised by its powerful, low level interface that allows for flexibility and programmability. However, considerable effort is required to become accustomed to the system and to reach a point where one can comfortably achieve simple natural deduction proofs. Isabelle is another powerful and widely used theorem prover that provides useful features for natural deduction proofs, including its meta-logic and its four main natural deduction tactics. In this paper we describe our efforts to emulate some of these features of Isabelle in HOL Light. One of our aims is to decrease the learning curve of HOL Light and make it more accessible and usable by a range of users, while preserving its programmability.

Original language	English
Title of host publication	Logic for Programming, Artificial Intelligence, and Reasoning
Subtitle of host publication	17th International Conference, LPAR-17, Proceedings
Editors	Christian Fermüller, Andrei Voronkov
Publisher	Springer-Verlag GmbH
Pages	565-580
Number of pages	16
ISBN (Electronic)	978-3-642-16242-8
ISBN (Print)	978-3-642-16241-1
DOIs	https://doi.org/10.1007/978-3-642-16242-8_40
Publication status	Published - 1 Jan 2010
Event	17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2010 - Yogyakarta, Indonesia Duration: 10 Oct 2010 → 15 Oct 2010

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Berlin / Heidelberg
Volume	6397
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2010
Country	Indonesia
City	Yogyakarta
Period	10/10/10 → 15/10/10

Access to Document

10.1007/978-3-642-16242-8_40Licence: All Rights Reserved

http://www.springerlink.com/content/477k1l8m58146133/

Fingerprint Dive into the research topics of 'An Isabelle-Like Procedural Mode for HOL Light'. Together they form a unique fingerprint.

Cite this

Papapanagiotou, P., & Fleuriot, J. (2010). An Isabelle-Like Procedural Mode for HOL Light. In C. Fermüller, & A. Voronkov (Eds.), Logic for Programming, Artificial Intelligence, and Reasoning: 17th International Conference, LPAR-17, Proceedings (pp. 565-580). (Lecture Notes in Computer Science; Vol. 6397). Springer-Verlag GmbH. https://doi.org/10.1007/978-3-642-16242-8_40

@inproceedings{9da1ff79048f452392ad638b01fd5dea,

title = "An Isabelle-Like Procedural Mode for HOL Light",

abstract = "HOL Light is a modern theorem proving system characterised by its powerful, low level interface that allows for flexibility and programmability. However, considerable effort is required to become accustomed to the system and to reach a point where one can comfortably achieve simple natural deduction proofs. Isabelle is another powerful and widely used theorem prover that provides useful features for natural deduction proofs, including its meta-logic and its four main natural deduction tactics. In this paper we describe our efforts to emulate some of these features of Isabelle in HOL Light. One of our aims is to decrease the learning curve of HOL Light and make it more accessible and usable by a range of users, while preserving its programmability.",

author = "Petros Papapanagiotou and Jacques Fleuriot",

year = "2010",

month = jan,

day = "1",

doi = "10.1007/978-3-642-16242-8_40",

language = "English",

isbn = "978-3-642-16241-1",

series = "Lecture Notes in Computer Science",

publisher = "Springer-Verlag GmbH",

pages = "565--580",

editor = "Christian Ferm{\"u}ller and Andrei Voronkov",

booktitle = "Logic for Programming, Artificial Intelligence, and Reasoning",

note = "17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2010 ; Conference date: 10-10-2010 Through 15-10-2010",

}

Papapanagiotou, P & Fleuriot, J 2010, An Isabelle-Like Procedural Mode for HOL Light. in C Fermüller & A Voronkov (eds), Logic for Programming, Artificial Intelligence, and Reasoning: 17th International Conference, LPAR-17, Proceedings. Lecture Notes in Computer Science, vol. 6397, Springer-Verlag GmbH, pp. 565-580, 17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2010, Yogyakarta, Indonesia, 10/10/10. https://doi.org/10.1007/978-3-642-16242-8_40

An Isabelle-Like Procedural Mode for HOL Light. / Papapanagiotou, Petros ; Fleuriot, Jacques.

Logic for Programming, Artificial Intelligence, and Reasoning: 17th International Conference, LPAR-17, Proceedings. ed. / Christian Fermüller; Andrei Voronkov. Springer-Verlag GmbH, 2010. p. 565-580 (Lecture Notes in Computer Science; Vol. 6397).

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

TY - GEN

T1 - An Isabelle-Like Procedural Mode for HOL Light

AU - Papapanagiotou, Petros

AU - Fleuriot, Jacques

PY - 2010/1/1

Y1 - 2010/1/1

N2 - HOL Light is a modern theorem proving system characterised by its powerful, low level interface that allows for flexibility and programmability. However, considerable effort is required to become accustomed to the system and to reach a point where one can comfortably achieve simple natural deduction proofs. Isabelle is another powerful and widely used theorem prover that provides useful features for natural deduction proofs, including its meta-logic and its four main natural deduction tactics. In this paper we describe our efforts to emulate some of these features of Isabelle in HOL Light. One of our aims is to decrease the learning curve of HOL Light and make it more accessible and usable by a range of users, while preserving its programmability.

AB - HOL Light is a modern theorem proving system characterised by its powerful, low level interface that allows for flexibility and programmability. However, considerable effort is required to become accustomed to the system and to reach a point where one can comfortably achieve simple natural deduction proofs. Isabelle is another powerful and widely used theorem prover that provides useful features for natural deduction proofs, including its meta-logic and its four main natural deduction tactics. In this paper we describe our efforts to emulate some of these features of Isabelle in HOL Light. One of our aims is to decrease the learning curve of HOL Light and make it more accessible and usable by a range of users, while preserving its programmability.

U2 - 10.1007/978-3-642-16242-8_40

DO - 10.1007/978-3-642-16242-8_40

M3 - Conference contribution

SN - 978-3-642-16241-1

T3 - Lecture Notes in Computer Science

SP - 565

EP - 580

BT - Logic for Programming, Artificial Intelligence, and Reasoning

A2 - Fermüller, Christian

A2 - Voronkov, Andrei

PB - Springer-Verlag GmbH

T2 - 17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2010

Y2 - 10 October 2010 through 15 October 2010

ER -