×

zbMATH — the first resource for mathematics

Harrison, John

Compute Distance To:
Author ID: harrison.john Recent zbMATH articles by "Harrison, John"
Published as: Harrison, J.; Harrison, John
Documents Indexed: 50 Publications since 1972, including 6 Books

Publications by Year

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.03001
Harrison, John
39
2009
Theorem proving with the real numbers. Zbl 0932.68099
Harrison, John
37
1998
HOL Light: an overview. Zbl 1252.68255
Harrison, John
35
2009
A HOL theory of Euclidean space. Zbl 1152.68520
Harrison, John
29
2005
The HOL Light theory of Euclidean space. Zbl 1260.68373
Harrison, John
27
2013
Towards self-verification of HOL Light. Zbl 1222.68364
Harrison, John
19
2006
A Skeptic’s approach to combining HOL and Maple. Zbl 0916.68142
Harrison, J.; Théry, L.
19
1998
Verifying nonlinear real formulas via sums of squares. Zbl 1144.68357
Harrison, John
18
2007
A revision of the proof of the Kepler conjecture. Zbl 1195.52004
Hales, Thomas C.; Harrison, John; McLaughlin, Sean; Nipkow, Tobias; Obua, Steven; Zumkeller, Roland
14
2010
A proof-producing decision procedure for real arithmetic. Zbl 1135.03329
McLaughlin, Sean; Harrison, John
12
2005
A formal proof of the Kepler conjecture. Zbl 1379.52018
Hales, 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.03303
Harrison, John
10
2008
Formalizing an analytic proof of the prime number theorem. Zbl 1185.68624
Harrison, John
9
2009
Some new results on decidability for elementary algebra and geometry. Zbl 1259.03020
Solovay, Robert M.; Arthan, R. D.; Harrison, John
8
2012
Without loss of generality. Zbl 1252.68254
Harrison, John
7
2009
Formalizing basic first order model theory. Zbl 0930.03010
Harrison, John
7
1998
Efficient and accurate computation of upper bounds of approximation errors. Zbl 1211.65025
Chevillard, S.; Harrison, J.; Joldeş, M.; Lauter, Ch.
6
2011
Dynamical properties of PWD0L systems. Zbl 0873.68117
Harrison, John
6
1995
Morphic congruences and D0L languages. Zbl 0938.68712
Harrison, John
6
1994
Constructing the real numbers in HOL. Zbl 0809.68102
Harrison, John
6
1994
Reasoning about the reals: The marriage of HOL and Maple. Zbl 0793.68084
Harrison, John; Théry, Laurent
5
1993
Formal verification of square root algorithms. Zbl 1021.68058
Harrison, John
4
2003
Formal verification of IA-64 division algorithms. Zbl 0974.68535
Harrison, John
3
2000
Zur Homotopietheorie von Abbildungen in homotopie-assoziative H-Räume. Zbl 0242.55013
Harrison, J.; Scheerer, H.
3
1972
A software implementation of the IEEE 754R decimal floating-point arithmetic using the binary encoding format. Zbl 1367.65212
Cornea, 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.03020
Harrison, John
2
2007
Floating-point verification using theorem proving. Zbl 1182.68120
Harrison, John
2
2006
Theorem proving in higher order logics. 13th international conference, TPHOLs 2000, Portland, OR, USA, August 14–18, 2000. Proceedings. Zbl 0944.00036
Aagaard, Mark (ed.); Harrison, John (ed.)
2
2000
Inductive definitions: automation and application. Zbl 1063.03501
Harrison, John
2
1995
Formal proofs of hypergeometric sums. Dedicated to the memory of Andrzej Trybulec. Zbl 1356.68190
Harrison, John
1
2015
A short survey of automated reasoning. Zbl 1162.68512
Harrison, John
1
2007
Optimizing proof search in model elimination. Zbl 1412.68231
Harrison, John
1
1996
Floating point verification in HOL. Zbl 1063.68652
Harrison, John
1
1995
A formal proof of the Kepler conjecture. Zbl 1379.52018
Hales, 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.68190
Harrison, John
1
2015
The HOL Light theory of Euclidean space. Zbl 1260.68373
Harrison, John
27
2013
Some new results on decidability for elementary algebra and geometry. Zbl 1259.03020
Solovay, Robert M.; Arthan, R. D.; Harrison, John
8
2012
Efficient and accurate computation of upper bounds of approximation errors. Zbl 1211.65025
Chevillard, S.; Harrison, J.; Joldeş, M.; Lauter, Ch.
6
2011
A revision of the proof of the Kepler conjecture. Zbl 1195.52004
Hales, Thomas C.; Harrison, John; McLaughlin, Sean; Nipkow, Tobias; Obua, Steven; Zumkeller, Roland
14
2010
Handbook of practical logic and automated reasoning. Zbl 1178.03001
Harrison, John
39
2009
HOL Light: an overview. Zbl 1252.68255
Harrison, John
35
2009
Formalizing an analytic proof of the prime number theorem. Zbl 1185.68624
Harrison, John
9
2009
Without loss of generality. Zbl 1252.68254
Harrison, John
7
2009
A software implementation of the IEEE 754R decimal floating-point arithmetic using the binary encoding format. Zbl 1367.65212
Cornea, Marius; Harrison, John; Anderson, Cristina; Tang, Ping Tak Peter; Schneider, Eric; Gvozdev, Evgeny
2
2009
Formal proof – theory and practice. Zbl 1154.03303
Harrison, John
10
2008
Verifying nonlinear real formulas via sums of squares. Zbl 1144.68357
Harrison, John
18
2007
Automating elementary number-theoretic proofs using Gröbner bases. Zbl 1213.03020
Harrison, John
2
2007
A short survey of automated reasoning. Zbl 1162.68512
Harrison, John
1
2007
Towards self-verification of HOL Light. Zbl 1222.68364
Harrison, John
19
2006
Floating-point verification using theorem proving. Zbl 1182.68120
Harrison, John
2
2006
A HOL theory of Euclidean space. Zbl 1152.68520
Harrison, John
29
2005
A proof-producing decision procedure for real arithmetic. Zbl 1135.03329
McLaughlin, Sean; Harrison, John
12
2005
Formal verification of square root algorithms. Zbl 1021.68058
Harrison, John
4
2003
Formal verification of IA-64 division algorithms. Zbl 0974.68535
Harrison, John
3
2000
Theorem proving in higher order logics. 13th international conference, TPHOLs 2000, Portland, OR, USA, August 14–18, 2000. Proceedings. Zbl 0944.00036
Aagaard, Mark (ed.); Harrison, John (ed.)
2
2000
Theorem proving with the real numbers. Zbl 0932.68099
Harrison, John
37
1998
A Skeptic’s approach to combining HOL and Maple. Zbl 0916.68142
Harrison, J.; Théry, L.
19
1998
Formalizing basic first order model theory. Zbl 0930.03010
Harrison, John
7
1998
Optimizing proof search in model elimination. Zbl 1412.68231
Harrison, John
1
1996
Dynamical properties of PWD0L systems. Zbl 0873.68117
Harrison, John
6
1995
Inductive definitions: automation and application. Zbl 1063.03501
Harrison, John
2
1995
Floating point verification in HOL. Zbl 1063.68652
Harrison, John
1
1995
Morphic congruences and D0L languages. Zbl 0938.68712
Harrison, John
6
1994
Constructing the real numbers in HOL. Zbl 0809.68102
Harrison, John
6
1994
Reasoning about the reals: The marriage of HOL and Maple. Zbl 0793.68084
Harrison, John; Théry, Laurent
5
1993
Zur Homotopietheorie von Abbildungen in homotopie-assoziative H-Räume. Zbl 0242.55013
Harrison, J.; Scheerer, H.
3
1972
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