An informal introduction to ACL2(r) and non-standard analysis

Matt Kaufmann
ACL2 Seminar (afternoon session)
February 3, 2015

Talk materials:

• Notes for the talk
• Auxiliary files mentioned in those notes:
  • File sqrt-short.lisp: an abbreviated proof sketch for showing existence of the square root
  • File no-sqrt-std.lisp: a slight modification of Ruben Gamboa's proof to show that the square root of 2 does not exist in ACL2