3 papers
math.LO2009
Some new results on decidability for elementary algebra and geometry
Robert M. Solovay, R. D. Arthan, John Harrison
We carry out a systematic study of decidability for theories of (a) real vector spaces, inner product spaces, and Hilbert spaces and (b) normed spaces, Banach spaces and metric spa…
math.MG2009
A revision of the proof of the Kepler conjecture
Thomas C. Hales, John Harrison, Sean McLaughlin +3
The Kepler conjecture asserts that no packing of congruent balls in three-dimensional Euclidean space has density greater than that of the face-centered cubic packing. The original…
cs.AI2006
LPAR-05 Workshop: Empirically Successfull Automated Reasoning in Higher-Order Logic (ESHOL)
Christoph Benzmueller, John Harrison, Carsten Schuermann
This workshop brings together practioners and researchers who are involved in the everyday aspects of logical systems based on higher-order logic. We hope to create a friendly and…