Interactively explorable formal proofs for textbooks of mathematics

 |  Login

Show simple item record

dc.contributor Aalto-yliopisto fi
dc.contributor Aalto University en
dc.contributor.advisor Janhunen, Tomi
dc.contributor.author Peltola, Veli
dc.date.accessioned 2015-10-16T08:51:55Z
dc.date.available 2015-10-16T08:51:55Z
dc.date.issued 2015-09-29
dc.identifier.uri https://aaltodoc.aalto.fi/handle/123456789/18170
dc.description.abstract Electronic textbooks of mathematics would benefit from interactively explorable proofs, where the reader can request a more detailed explanation for any part of the proof he or she does not understand. This requires that definitions, theorem statements, and proofs are written in some formal language. In this thesis we investigate the theoretical and practical challenges of producing such textbooks. Any particular choice of language cannot be adequate for all textbooks, so we construct a theoretical framework for discussing extensible languages. Under this framework we define three languages for expressing definitions and theorem statements. The first two correspond to the standard languages of propositional and first-order logics. The third language is expressive enough for most definitions and theorem statements in discrete mathematics, but conceptually less problematic than the languages of set theory and higher-order logic, because it cannot express unrestricted quantification over sets that are larger than the set of real numbers. In addition, an implementation of an interactive proof explorer is presented. Its capabilities are demonstrated with an explorable proof of Bertrand’s postulate. The focus of this thesis is on the experience of the reader, and the results seem promising in that regard. With further work on making the authoring tools more efficient to use, it should be feasible to formalize an entire textbook. en
dc.description.abstract Sähköisissä matematiikan oppikirjoissa olisi hyötyä interaktiivisista todistuksista, joiden avulla lukija voisi pyytää tarkentavaa selitystä mihin tahansa kohtaan, jota hän ei ymmärrä. Tällaisen kirjan kirjoittaminen vaatii, että määritelmät, lauseet ja todistukset on kirjoitettu jollain formaalilla kielellä. Tässä diplomityössä tutkitaan sekä käytännön että teorian tasolla interaktiivisia todistuksia sisältävien oppikirjojen kirjoittamiseen liittyviä haasteita. Koska mikään yksittäinen kieli ei voi olla riittävä kaikkien oppikirjojen tarpeisiin, työssä määritellään kielen laajentamisen käsite. Tämän viitekehyksen sisällä kehitetään määritelmille ja lauseille kolme kieltä, joista kaksi ensimmäistä vastaavat lauselogiikkaa ja ensimmäisen kertaluvun predikaattilogiikkaa. Kolmas kieli, joka on näiden laajennus, on ilmaisuvoimaltaan riittävä monien diskreettiin matematiikkaan keskittyvien oppikirjojen formalisoimiseen. Tämä kieli on käsitteellisesti yksinkertaisempi kuin joukko-opin tai korkeamman kertaluvun predikaattilogiikan kielet, koska siinä ei pysty rajoittamattomasti kvantifioimaan sellaisten joukkojen yli, jotka ovat suurempia kuin reaalilukujen joukko. Lisäksi työssä esitellään tietokoneohjelma, jonka avulla interaktiivisesti tarkasteltavia formaaleja todistuksia voi lukea, sekä tämän ohjelman avulla kirjoitettu Bertrandin postulaatin todistus. Tässä työssä keskitytään todistuksiin lukijan näkökulmasta, ja tulokset ovat siltä osin lupaavia. Kokonaisen oppikirjan formalisoimiseksi vaaditaan vielä lisätyötä oppikirjan kirjoittajan työn helpottamiseksi. fi
dc.format.extent 73 + 6
dc.format.mimetype application/pdf en
dc.language.iso en en
dc.title Interactively explorable formal proofs for textbooks of mathematics en
dc.title Formaalien todistusten interaktiivinen tarkastelu matematiikan oppikirjoissa fi
dc.type G2 Pro gradu, diplomityö en
dc.contributor.school Perustieteiden korkeakoulu fi
dc.subject.keyword formal languages en
dc.subject.keyword formal proofs en
dc.subject.keyword mathematics education en
dc.subject.keyword first-order logic en
dc.subject.keyword second-order arithmetic en
dc.subject.keyword continuum hypothesis en
dc.identifier.urn URN:NBN:fi:aalto-201510164760
dc.programme.major Matematiikka fi
dc.programme.mcode F3006 fi
dc.type.ontasot Master's thesis en
dc.type.ontasot Diplomityö fi
dc.contributor.supervisor Hollanti, Camilla
dc.programme Teknillisen fysiikan ja matematiikan koulutusohjelma fi


Files in this item

This item appears in the following Collection(s)

Show simple item record

Search archive


Advanced Search

article-iconSubmit a publication

Browse

My Account