John R. Cowles, Ruben Gamboa. Using a First Order Logic to Verify That Some Set of Reals Has No Lesbegue Measure. In Matt Kaufmann, Lawrence C. Paulson, editors, Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings. Volume 6172 of Lecture Notes in Computer Science, pages 25-34, Springer, 2010. [doi]
Abstract is missing.