Proving in the Isabelle Proof Assistant that the Set of Real Numbers is not Countable

Research output: Contribution to conferencePaperResearchpeer-review

218 Downloads (Pure)

Abstract

We present a new succinct proof of the uncountability of the real numbers – optimized
for clarity – based on the proof by Benjamin Porter in the Isabelle Analysis theory.
Original languageEnglish
Publication date2018
Number of pages6
Publication statusPublished - 2018
EventInternational Workshop on Theorem proving components for Educational software - Oxford , United Kingdom
Duration: 18 Jul 201818 Jul 2018
http://www.uc.pt/en/congressos/thedu/thedu18/programme

Conference

ConferenceInternational Workshop on Theorem proving components for Educational software
Country/TerritoryUnited Kingdom
CityOxford
Period18/07/201818/07/2018
Internet address

Fingerprint

Dive into the research topics of 'Proving in the Isabelle Proof Assistant that the Set of Real Numbers is not Countable'. Together they form a unique fingerprint.

Cite this