An Isabelle-Like Procedural Mode for HOL Light

Research output: Chapter in Book/Report/Conference proceedingConference 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 languageEnglish
Title of host publicationLogic for Programming, Artificial Intelligence, and Reasoning
Subtitle of host publication 17th International Conference, LPAR-17, Proceedings
EditorsChristian Fermüller, Andrei Voronkov
PublisherSpringer-Verlag GmbH
Pages565-580
Number of pages16
ISBN (Electronic)978-3-642-16242-8
ISBN (Print)978-3-642-16241-1
DOIs
Publication statusPublished - 1 Jan 2010
Event17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2010 - Yogyakarta, Indonesia
Duration: 10 Oct 201015 Oct 2010

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin / Heidelberg
Volume6397
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2010
CountryIndonesia
CityYogyakarta
Period10/10/1015/10/10

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

Cite this