haku: @instructor Janhunen, Tomi / yhteensä: 12
viite: 2 / 12
| Tekijä: | Peltola, Veli |
| Työn nimi: | Interactively explorable formal proofs for textbooks of mathematics |
| Formaalien todistusten interaktiivinen tarkastelu matematiikan oppikirjoissa | |
| Julkaisutyyppi: | Diplomityö |
| Julkaisuvuosi: | 2015 |
| Sivut: | vi + 73 Kieli: eng |
| Koulu/Laitos/Osasto: | Perustieteiden korkeakoulu |
| Oppiaine: | Matematiikka (F3006) |
| Valvoja: | Hollanti, Camilla |
| Ohjaaja: | Janhunen, Tomi |
| Elektroninen julkaisu: | http://urn.fi/URN:NBN:fi:aalto-201510164760 |
| Sijainti: | P1 Ark Aalto 3143 | Arkisto |
| Avainsanat: | formal languages formal proofs mathematics education first-order logic second-order arithmetic continuum hypothesis formaalit todistukset formaalit kielet matematiikan opetus ensimmäisen kertaluvun logiikka toisen kertaluvun aritmetiikka Bertrandin postulaatti kontinuumihypoteesi |
| Tiivistelmä (fin): | 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. |
| Tiivistelmä (eng): | 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. |
| ED: | 2015-11-08 |
INSSI tietueen numero: 52367
+ lisää koriin
INSSI