Edit Profile Harrison, John Compute Distance To: Compute Author ID: harrison.john Published as: Harrison, J.; Harrison, John Documents Indexed: 50 Publications since 1972, including 6 Books Co-Authors 0 single-authored 1 Chevillard, Sylvain 1 Grundy, Jim 1 Joldeş, Mioara 1 Lauter, Christoph Quirin 1 von Wright, Joakim Serials 1 Theoretical Computer Science 1 Lecture Notes in Computer Science all top 5 Fields 1 General and overarching topics; collections (00-XX) 1 Mathematical logic and foundations (03-XX) 1 Real functions (26-XX) 1 Special functions (33-XX) 1 Numerical analysis (65-XX) 1 Computer science (68-XX) Publications by Year all cited Publications top 5 cited Publications Citations contained in zbMATH 33 Publications have been cited 354 times in 252 Documents Cited by ▼ Year ▼ Handbook of practical logic and automated reasoning. Zbl 1178.03001Harrison, John 39 2009 Theorem proving with the real numbers. Zbl 0932.68099Harrison, John 37 1998 HOL Light: an overview. Zbl 1252.68255Harrison, John 35 2009 A HOL theory of Euclidean space. Zbl 1152.68520Harrison, John 29 2005 The HOL Light theory of Euclidean space. Zbl 1260.68373Harrison, John 27 2013 Towards self-verification of HOL Light. Zbl 1222.68364Harrison, John 19 2006 A Skeptic’s approach to combining HOL and Maple. Zbl 0916.68142Harrison, J.; Théry, L. 19 1998 Verifying nonlinear real formulas via sums of squares. Zbl 1144.68357Harrison, John 18 2007 A revision of the proof of the Kepler conjecture. Zbl 1195.52004Hales, Thomas C.; Harrison, John; McLaughlin, Sean; Nipkow, Tobias; Obua, Steven; Zumkeller, Roland 14 2010 A proof-producing decision procedure for real arithmetic. Zbl 1135.03329McLaughlin, Sean; Harrison, John 12 2005 A formal proof of the Kepler conjecture. Zbl 1379.52018Hales, Thomas; Adams, Mark; Bauer, Gertrud; Dang, Tat Dat; Harrison, John; Hoang, Le Truong; Kaliszyk, Cezary; Magron, Victor; McLaughlin, Sean; Nguyen, Tat Thang; Nguyen, Quang Truong; Nipkow, Tobias; Obua, Steven; Pleso, Joseph; Rute, Jason; Solovyev, Alexey; Ta, Thi Hoai An; Tran, Nam Trung; Trieu, Thi Diep; Urban, Josef; Vu, Ky; Zumkeller, Roland 11 2017 Formal proof – theory and practice. Zbl 1154.03303Harrison, John 10 2008 Formalizing an analytic proof of the prime number theorem. Zbl 1185.68624Harrison, John 9 2009 Some new results on decidability for elementary algebra and geometry. Zbl 1259.03020Solovay, Robert M.; Arthan, R. D.; Harrison, John 8 2012 Without loss of generality. Zbl 1252.68254Harrison, John 7 2009 Formalizing basic first order model theory. Zbl 0930.03010Harrison, John 7 1998 Efficient and accurate computation of upper bounds of approximation errors. Zbl 1211.65025Chevillard, S.; Harrison, J.; Joldeş, M.; Lauter, Ch. 6 2011 Dynamical properties of PWD0L systems. Zbl 0873.68117Harrison, John 6 1995 Morphic congruences and D0L languages. Zbl 0938.68712Harrison, John 6 1994 Constructing the real numbers in HOL. Zbl 0809.68102Harrison, John 6 1994 Reasoning about the reals: The marriage of HOL and Maple. Zbl 0793.68084Harrison, John; Théry, Laurent 5 1993 Formal verification of square root algorithms. Zbl 1021.68058Harrison, John 4 2003 Formal verification of IA-64 division algorithms. Zbl 0974.68535Harrison, John 3 2000 Zur Homotopietheorie von Abbildungen in homotopie-assoziative H-Räume. Zbl 0242.55013Harrison, J.; Scheerer, H. 3 1972 A software implementation of the IEEE 754R decimal floating-point arithmetic using the binary encoding format. Zbl 1367.65212Cornea, Marius; Harrison, John; Anderson, Cristina; Tang, Ping Tak Peter; Schneider, Eric; Gvozdev, Evgeny 2 2009 Automating elementary number-theoretic proofs using Gröbner bases. Zbl 1213.03020Harrison, John 2 2007 Floating-point verification using theorem proving. Zbl 1182.68120Harrison, John 2 2006 Theorem proving in higher order logics. 13th international conference, TPHOLs 2000, Portland, OR, USA, August 14–18, 2000. Proceedings. Zbl 0944.00036Aagaard, Mark (ed.); Harrison, John (ed.) 2 2000 Inductive definitions: automation and application. Zbl 1063.03501Harrison, John 2 1995 Formal proofs of hypergeometric sums. Dedicated to the memory of Andrzej Trybulec. Zbl 1356.68190Harrison, John 1 2015 A short survey of automated reasoning. Zbl 1162.68512Harrison, John 1 2007 Optimizing proof search in model elimination. Zbl 1412.68231Harrison, John 1 1996 Floating point verification in HOL. Zbl 1063.68652Harrison, John 1 1995 A formal proof of the Kepler conjecture. Zbl 1379.52018Hales, Thomas; Adams, Mark; Bauer, Gertrud; Dang, Tat Dat; Harrison, John; Hoang, Le Truong; Kaliszyk, Cezary; Magron, Victor; McLaughlin, Sean; Nguyen, Tat Thang; Nguyen, Quang Truong; Nipkow, Tobias; Obua, Steven; Pleso, Joseph; Rute, Jason; Solovyev, Alexey; Ta, Thi Hoai An; Tran, Nam Trung; Trieu, Thi Diep; Urban, Josef; Vu, Ky; Zumkeller, Roland 11 2017 Formal proofs of hypergeometric sums. Dedicated to the memory of Andrzej Trybulec. Zbl 1356.68190Harrison, John 1 2015 The HOL Light theory of Euclidean space. Zbl 1260.68373Harrison, John 27 2013 Some new results on decidability for elementary algebra and geometry. Zbl 1259.03020Solovay, Robert M.; Arthan, R. D.; Harrison, John 8 2012 Efficient and accurate computation of upper bounds of approximation errors. Zbl 1211.65025Chevillard, S.; Harrison, J.; Joldeş, M.; Lauter, Ch. 6 2011 A revision of the proof of the Kepler conjecture. Zbl 1195.52004Hales, Thomas C.; Harrison, John; McLaughlin, Sean; Nipkow, Tobias; Obua, Steven; Zumkeller, Roland 14 2010 Handbook of practical logic and automated reasoning. Zbl 1178.03001Harrison, John 39 2009 HOL Light: an overview. Zbl 1252.68255Harrison, John 35 2009 Formalizing an analytic proof of the prime number theorem. Zbl 1185.68624Harrison, John 9 2009 Without loss of generality. Zbl 1252.68254Harrison, John 7 2009 A software implementation of the IEEE 754R decimal floating-point arithmetic using the binary encoding format. Zbl 1367.65212Cornea, Marius; Harrison, John; Anderson, Cristina; Tang, Ping Tak Peter; Schneider, Eric; Gvozdev, Evgeny 2 2009 Formal proof – theory and practice. Zbl 1154.03303Harrison, John 10 2008 Verifying nonlinear real formulas via sums of squares. Zbl 1144.68357Harrison, John 18 2007 Automating elementary number-theoretic proofs using Gröbner bases. Zbl 1213.03020Harrison, John 2 2007 A short survey of automated reasoning. Zbl 1162.68512Harrison, John 1 2007 Towards self-verification of HOL Light. Zbl 1222.68364Harrison, John 19 2006 Floating-point verification using theorem proving. Zbl 1182.68120Harrison, John 2 2006 A HOL theory of Euclidean space. Zbl 1152.68520Harrison, John 29 2005 A proof-producing decision procedure for real arithmetic. Zbl 1135.03329McLaughlin, Sean; Harrison, John 12 2005 Formal verification of square root algorithms. Zbl 1021.68058Harrison, John 4 2003 Formal verification of IA-64 division algorithms. Zbl 0974.68535Harrison, John 3 2000 Theorem proving in higher order logics. 13th international conference, TPHOLs 2000, Portland, OR, USA, August 14–18, 2000. Proceedings. Zbl 0944.00036Aagaard, Mark (ed.); Harrison, John (ed.) 2 2000 Theorem proving with the real numbers. Zbl 0932.68099Harrison, John 37 1998 A Skeptic’s approach to combining HOL and Maple. Zbl 0916.68142Harrison, J.; Théry, L. 19 1998 Formalizing basic first order model theory. Zbl 0930.03010Harrison, John 7 1998 Optimizing proof search in model elimination. Zbl 1412.68231Harrison, John 1 1996 Dynamical properties of PWD0L systems. Zbl 0873.68117Harrison, John 6 1995 Inductive definitions: automation and application. Zbl 1063.03501Harrison, John 2 1995 Floating point verification in HOL. Zbl 1063.68652Harrison, John 1 1995 Morphic congruences and D0L languages. Zbl 0938.68712Harrison, John 6 1994 Constructing the real numbers in HOL. Zbl 0809.68102Harrison, John 6 1994 Reasoning about the reals: The marriage of HOL and Maple. Zbl 0793.68084Harrison, John; Théry, Laurent 5 1993 Zur Homotopietheorie von Abbildungen in homotopie-assoziative H-Räume. Zbl 0242.55013Harrison, J.; Scheerer, H. 3 1972 all cited Publications top 5 cited Publications all top 5 Cited by 413 Authors 20 Tahar, Sofiène 17 Hasan, Osman 11 Harrison, John R. 10 Guan, Yong 10 Paulson, Lawrence Charles 9 Shi, Zhiping 8 Nipkow, Tobias 7 Kaliszyk, Cezary 6 Divasón, Jose 6 Popescu, Andrei 5 Blanchette, Jasmin Christian 5 Li, Yongdong 5 Melquiond, Guillaume 5 Rümmer, Philipp 4 Aransay, Jesús 4 Arthan, Rob D. 4 Khan Afshar, Sanaz 4 Kunčar, Ondřej 4 Myreen, Magnus O. 4 Siddique, Umair 3 Akbarpour, Behzad 3 Armando, Alessandro 3 Bertot, Yves 3 Boldo, Sylvie 3 Farmer, William M. 3 Kleine Büning, Hans 3 Kröning, Daniel 3 Li, Liming 3 Li, Wenda 3 Obua, Steven 3 Paşca, Ioana 3 Salomaa, Arto Kustaa 3 Subramani, Krishnan 3 Urban, Josef 3 Wei, Hongxing 3 Wiedijk, Freek 3 Wojciechowski, Piotr J. 2 Abbasi, Naeem 2 Adams, Mark 2 Aravantinos, Vincent 2 Avigad, Jeremy 2 Benzmüller, Christoph Ewald 2 Bergstra, Jan A. 2 Calude, Cristian S. 2 Caprotti, Olga 2 Chaieb, Amine 2 Chandy, Kanianthra Mani 2 Coglio, Alessandro 2 Davis, Jared 2 de Moura, Leonardo 2 Dunets, Andriy 2 Fleury, Mathias 2 Fox, Anthony C. J. 2 Gauthier, Thibault 2 Geuvers, Jan Herman 2 Giunchiglia, Fausto 2 Gonthier, Georges 2 Gopalakrishnan, Ganesh Lalitha 2 Gottliebsen, Hanne 2 Hales, Thomas Callister 2 Harrison, John 2 Honkala, Juha 2 Immler, Fabian 2 Joldeş, Mioara 2 Jonáš, Martin 2 Joosten, Sebastiaan J. C. 2 Kohlhase, Michael 2 Lelay, Catherine 2 Maggesi, Marco 2 Magron, Victor 2 Mahmoud, Mohamed Yousri 2 Makowsky, Johann-Andreas 2 Martin-Dorel, Érik 2 Martín-Mateos, Francisco-Jesús 2 Martin, Ursula 2 Mayero, Micaela 2 McLaughlin, Sean 2 Mitra, Sayan 2 Muñoz, César A. 2 Narkawicz, Anthony Joseph 2 Norrish, Michael 2 Pąk, Karol 2 Passmore, Grant Olney 2 Rashid, Adnan 2 Reif, Wolfgang 2 Scheerer, Hans 2 Schellhorn, Gerhard 2 Schlichtkrull, Anders 2 Seddiki, Ons 2 Solovyev, Alexey 2 Strejček, Jan 2 Théry, Laurent 2 Thiemann, René 2 Traytel, Dmitry 2 Wang, Guohui 2 Weidenbach, Christoph 2 Wintersteiger, Christoph M. 2 Wu, Aixuan 2 Yamada, Akihisa 2 Ye, Shiwei ...and 313 more Authors all top 5 Cited in 57 Serials 56 Journal of Automated Reasoning 14 Theoretical Computer Science 12 Formal Aspects of Computing 11 Journal of Symbolic Computation 10 Formal Methods in System Design 7 Mathematics in Computer Science 5 MSCS. Mathematical Structures in Computer Science 4 Artificial Intelligence 4 Journal of Applied Logic 3 Information Processing Letters 3 Annals of Mathematics and Artificial Intelligence 3 Mathematical Problems in Engineering 3 Journal of Applied Mathematics 3 Journal of Formalized Reasoning 2 Acta Informatica 2 Journal of Computer and System Sciences 2 Discrete & Computational Geometry 2 Information and Computation 2 Numerical Algorithms 2 The Bulletin of Symbolic Logic 2 Sādhanā 1 Communications in Mathematical Physics 1 Jahresbericht der Deutschen Mathematiker-Vereinigung (DMV) 1 Mathematical Methods in the Applied Sciences 1 Rocky Mountain Journal of Mathematics 1 Mathematics of Computation 1 Applied Mathematics and Optimization 1 Archiv der Mathematik 1 BIT 1 Fuzzy Sets and Systems 1 Information Sciences 1 Journal of Mathematical Economics 1 Mathematische Annalen 1 Mathematische Zeitschrift 1 Synthese 1 Science of Computer Programming 1 Mathematical Social Sciences 1 Annals of Pure and Applied Logic 1 Journal of Computer Science and Technology 1 International Journal of Computer Mathematics 1 Bulletin of the American Mathematical Society. New Series 1 Indagationes Mathematicae. New Series 1 Applicable Algebra in Engineering, Communication and Computing 1 Journal of Logic, Language and Information 1 Advances in Applied Clifford Algebras 1 Journal of Functional Programming 1 Higher-Order and Symbolic Computation 1 LMS Journal of Computation and Mathematics 1 Journal of Systems Science and Complexity 1 JP Journal of Algebra, Number Theory and Applications 1 Sibirskie Èlektronnye Matematicheskie Izvestiya 1 Logical Methods in Computer Science 1 Forum of Mathematics, Pi 1 Journal of Logical and Algebraic Methods in Programming 1 European Journal of Mathematics 1 Proceedings of the Royal Society of London. A. Mathematical, Physical and Engineering Sciences 1 SIAM Journal on Applied Algebra and Geometry all top 5 Cited in 39 Fields 220 Computer science (68-XX) 66 Mathematical logic and foundations (03-XX) 23 Numerical analysis (65-XX) 9 Real functions (26-XX) 7 Number theory (11-XX) 6 General and overarching topics; collections (00-XX) 5 History and biography (01-XX) 5 Linear and multilinear algebra; matrix theory (15-XX) 5 Convex and discrete geometry (52-XX) 5 Operations research, mathematical programming (90-XX) 5 Information and communication theory, circuits (94-XX) 4 Special functions (33-XX) 4 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 3 Combinatorics (05-XX) 3 Ordinary differential equations (34-XX) 3 Geometry (51-XX) 3 Algebraic topology (55-XX) 3 Probability theory and stochastic processes (60-XX) 3 Mechanics of particles and systems (70-XX) 3 Optics, electromagnetic theory (78-XX) 3 Systems theory; control (93-XX) 3 Mathematics education (97-XX) 2 Field theory and polynomials (12-XX) 2 Commutative algebra (13-XX) 2 Algebraic geometry (14-XX) 2 Several complex variables and analytic spaces (32-XX) 2 Calculus of variations and optimal control; optimization (49-XX) 2 Quantum theory (81-XX) 1 Nonassociative rings and algebras (17-XX) 1 Topological groups, Lie groups (22-XX) 1 Measure and integration (28-XX) 1 Functions of a complex variable (30-XX) 1 Partial differential equations (35-XX) 1 Dynamical systems and ergodic theory (37-XX) 1 Approximations and expansions (41-XX) 1 Harmonic analysis on Euclidean spaces (42-XX) 1 General topology (54-XX) 1 Statistics (62-XX) 1 Statistical mechanics, structure of matter (82-XX) Citations by Year