×

HOL

swMATH ID: 5492
Software Authors: Gordon, Michael J. C.
Description: Higher Order Logic (HOL) is a programming environment in which theorems can be proved and proof tools implemented. Built-in decision procedures and theorem provers can automatically establish many simple theorems. An Oracle mechanism gives access to external programs such as SAT and BDD engines. HOL 4 is particularly suitable as a platform for implementing combinations of deduction, execution, and property checking.
Homepage: http://hol.sourceforge.net/
Programming Languages: ML
Keywords: proof assistant; theorem prover
Related Software: Isabelle; Isabelle/HOL; ML; Coq; HOL Light; PVS; Nuprl; Archive Formal Proofs; ACL2; Mizar; TPTP; Isar; LCF; Sledgehammer; Flyspeck; z3; E Theorem Prover; VAMPIRE; NQTHM; Isabelle/Isar
Referenced in: 575 Publications

Standard Articles

1 Publication describing the Software, including 1 Publication in zbMATH Year
A brief overview of HOL4. Zbl 1165.68474
Slind, Konrad; Norrish, Michael
2008
all top 5

Referenced by 668 Authors

36 Tahar, Sofiène
28 Hasan, Osman
24 Paulson, Lawrence Charles
23 Myreen, Magnus O.
20 Blanchette, Jasmin Christian
20 Norrish, Michael
17 Nipkow, Tobias
16 Kaliszyk, Cezary
14 Urban, Josef
13 Kumar, Ramana
12 Benzmüller, Christoph Ewald
12 Popescu, Andrei
11 Owens, Scott
10 Guan, Yong
10 Lochbihler, Andreas
10 Traytel, Dmitry
9 Shi, Zhiping
9 Thiemann, René
8 Farmer, William M.
8 Slind, Konrad
8 Woodcock, James C. P.
7 Gauthier, Thibault
7 Hurd, Joe
7 Lammich, Peter
7 Sternagel, Christian
6 Arthan, Rob D.
6 Fox, Anthony C. J.
6 Gordon, Michael J. C.
6 Kunčar, Ondřej
6 Rabe, Florian
6 Weber, Tjark
5 Boulton, Richard J.
5 Divasón, Jose
5 Foster, Simon
5 Gordon, Mike J.
5 Guttmann, Walter
5 Haslbeck, Max W.
5 Klein, Gerwin
5 Li, Yongdong
5 Schneider, Klaus
5 Siddique, Umair
5 Sutcliffe, Geoff
5 Zhang, Jie
4 Abdulaziz, Mohammad
4 Ahmed, Waqar
4 Akbarpour, Behzad
4 Amjad, Hasan
4 Aravantinos, Vincent
4 Basin, David A.
4 Böhme, Sascha
4 Chan, Hing-Lun
4 Dill, David L.
4 Duan, Zhenhua
4 Eberl, Manuel
4 Höfner, Peter
4 Hölzl, Johannes
4 Kaufmann, Matt
4 Krauss, Alexander
4 Liu, Liya
4 Loewenstein, Paul N.
4 Moore, J Strother
4 Schlichtkrull, Anders
4 Shankar, Natarajan
4 Struth, Georg
4 Tan, Yong Kiam
4 Théry, Laurent
4 Tian, Cong
4 Wenzel, Makarius
4 Yamada, Akihisa
4 Zhang, Nan
3 Abrahamsson, Oskar
3 Aït Mohamed, Otmane
3 Andrews, Peter B.
3 Aransay, Jesús
3 Aspinall, David
3 Barthwal, Aditi
3 Bentkamp, Alexander
3 Bottesch, Ralph Christian
3 Brown, Chad Edward
3 Curzon, Paul
3 Dam, Mads
3 Davis, Jared
3 Felty, Amy P.
3 Fleuriot, Jacques D.
3 Fleury, Mathias
3 Geuvers, Jan Herman
3 Homeier, Peter V.
3 Howe, Douglas J.
3 Huffman, Brian
3 Hupel, Lars
3 Immler, Fabian
3 Jacobs, Bart
3 Joosten, Sebastiaan J. C.
3 Khan Afshar, Sanaz
3 Li, Liming
3 Li, Wenda
3 Marmsoler, Diego
3 Mhamdi, Tarek
3 Middeldorp, Aart
3 Nederpelt, Rob
...and 568 more Authors
all top 5

Referenced in 57 Serials

83 Journal of Automated Reasoning
22 Formal Aspects of Computing
18 Formal Methods in System Design
15 Theoretical Computer Science
10 Journal of Applied Logic
9 Information and Computation
6 Journal of Formalized Reasoning
6 Journal of Logical and Algebraic Methods in Programming
5 Journal of Symbolic Computation
4 Journal of Functional Programming
4 Journal of Applied Mathematics
4 Mathematics in Computer Science
3 Science of Computer Programming
3 AI Communications
3 MSCS. Mathematical Structures in Computer Science
3 Annals of Mathematics and Artificial Intelligence
3 The Journal of Logic and Algebraic Programming
3 Lecture Notes in Computer Science
3 Logical Methods in Computer Science
2 Acta Informatica
2 Artificial Intelligence
2 Information Processing Letters
2 Journal of Computer and System Sciences
2 Distributed Computing
2 Nordic Journal of Computing
2 Mathematical Problems in Engineering
2 Journal of Combinatorial Optimization
2 Journal of the ACM
2 Sādhanā
2 Logica Universalis
1 Jahresbericht der Deutschen Mathematiker-Vereinigung (DMV)
1 The Mathematical Intelligencer
1 IEEE Transactions on Computers
1 Journal of Philosophical Logic
1 The Journal of Symbolic Logic
1 Annales Societatis Mathematicae Polonae. Series IV
1 Annals of Pure and Applied Logic
1 Journal of Computer Science and Technology
1 Journal of Cryptology
1 Bulletin of the European Association for Theoretical Computer Science (EATCS)
1 International Journal of Computer Mathematics
1 Indagationes Mathematicae. New Series
1 Bulletin of the Belgian Mathematical Society - Simon Stevin
1 Advances in Applied Clifford Algebras
1
1 Higher-Order and Symbolic Computation
1 Fundamenta Informaticae
1
1 ACM Transactions on Computational Logic
1 International Journal of Parallel, Emergent and Distributed Systems
1 Cambridge Tracts in Theoretical Computer Science
1 The Kluwer International Series in Engineering and Computer Science
1 AMAST Series in Computing
1 Forum of Mathematics, Pi
1 Nonlinear Analysis. Theory, Methods & Applications
1 Proceedings of the Royal Society of London. A. Mathematical, Physical and Engineering Sciences
1 Texts in Theoretical Computer Science. An EATCS Series
all top 5

Referenced in 35 Fields

549 Computer science (68-XX)
156 Mathematical logic and foundations (03-XX)
19 Information and communication theory, circuits (94-XX)
12 Combinatorics (05-XX)
11 Number theory (11-XX)
10 Numerical analysis (65-XX)
7 Real functions (26-XX)
6 Linear and multilinear algebra; matrix theory (15-XX)
6 Probability theory and stochastic processes (60-XX)
6 Operations research, mathematical programming (90-XX)
5 History and biography (01-XX)
5 Category theory; homological algebra (18-XX)
4 General and overarching topics; collections (00-XX)
4 Commutative algebra (13-XX)
4 Game theory, economics, finance, and other social and behavioral sciences (91-XX)
4 Systems theory; control (93-XX)
3 Field theory and polynomials (12-XX)
3 Functions of a complex variable (30-XX)
3 Ordinary differential equations (34-XX)
3 Optics, electromagnetic theory (78-XX)
2 Order, lattices, ordered algebraic structures (06-XX)
2 Group theory and generalizations (20-XX)
2 Measure and integration (28-XX)
2 Dynamical systems and ergodic theory (37-XX)
2 Convex and discrete geometry (52-XX)
2 Mechanics of particles and systems (70-XX)
1 Algebraic geometry (14-XX)
1 Several complex variables and analytic spaces (32-XX)
1 Special functions (33-XX)
1 Calculus of variations and optimal control; optimization (49-XX)
1 Geometry (51-XX)
1 Manifolds and cell complexes (57-XX)
1 Quantum theory (81-XX)
1 Biology and other natural sciences (92-XX)
1 Mathematics education (97-XX)

Referencing Publications by Year