Using a First Order Logic to Verify That Some Set of Reals Has No Lesbegue Measure

1. Cowles, J.: ACL2 book: Principle of dependent choices. Formal proof script available from author (2010)

   Google Scholar 

2. Davis, J.: Acl2-books repository. Presented at the ACL2 Workshop (2009)

   Google Scholar 

3. Gamboa, R., Cowles, J.: Theory extension in ACL2(r). Journal of Automated Reasoning (May 2007)

   Google Scholar 

4. Gamboa, R., Kaufmann, M.: Nonstandard analysis in ACL2. Journal of Automated Reasoning 27(4), 323–351 (2001)

   Article  MATH  MathSciNet  Google Scholar 

5. Goldblatt, R.: Lectures on the Hyperreals: An Introduction to Nonstandard Analysis, ch. 16. Springer, Heidelberg (1998)

   Google Scholar 

6. Jech, T.J.: The Axiom of Choice, vol. 75. North-Holland Publishing Company, Amsterdam (1973)

   MATH  Google Scholar 

7. Kaufmann, M., Moore, J.S.: Structured theory development for a mechanized logic. Journal of Automated Reasoning 26(2), 161–203 (2001)

   Article  MATH  MathSciNet  Google Scholar 

8. Nelson, E.: Internal set theory: A new approach to nonstandard analysis. Bulletin of the American Mathematical Society 83, 1165–1198 (1977)

   Article  MATH  MathSciNet  Google Scholar 

9. Royden, H.L.: Real Analysis, 2nd edn. Macmillan, Basingstoke (1968)

   Google Scholar 

10. Solovay, R.M.: A model of set theory in which every set of reals is Lebesgue measurable. Annals of Mathematics 92, 1–56 (1970)

    Article  MathSciNet  Google Scholar 

11. Vitali, G.: Sul problema della mesura dei gruppi di una retta (1905)

    Google Scholar 

Download references