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 -