<div class="csl-bib-body">
<div class="csl-entry">Wiesnet, F. (2025, April 23). <i>Program Extraction in Number Theory: The Fundamental Theorem of Arithmetic and Friends</i> [Presentation]. Oberseminar Mathematische Logik 2025, Ludwig-Maximilians Universität München, Germany. http://hdl.handle.net/20.500.12708/223916</div>
</div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/223916
-
dc.description.abstract
We present a constructive treatment of central theorems from elementary number theory within the interactive proof system Minlog. Formalization in Minlog not only guarantees the correctness of the proofs but also enables the extraction of executable programs, with a particular focus on their computational content. For this purpose, we make use of Minlog’s built-in program extraction mechanism. To achieve efficient implementations, algorithmic aspects are already taken into account during the proof construction. For instance, the proofs explicitly use the binary representation of natural numbers, as it is significantly more efficient in computation than the traditional successor-based representation. The underlying Minlog implementation includes formalizations of theorems such as Bézout’s identity, the fundamental theorem of arithmetic, and Fermat’s factorization method. Using selected examples, we illustrate how this constructive and algorithmically oriented approach influences the structure of the proofs and how it differs from classical standard proofs. We also demonstrate the extracted programs in Haskell. While prior knowledge of Minlog or the underlying logical theory is helpful, the talk is designed to be accessible without it. Only a basic understanding of elementary number theory will be necessary.
en
dc.description.sponsorship
FWF - Österr. Wissenschaftsfonds
-
dc.language.iso
de
-
dc.subject
Minlog
de
dc.subject
Zahlentheorie
de
dc.subject
konstruktive Mathematik
de
dc.subject
Programextraktion
de
dc.subject
Faktorisierungsverfahren
de
dc.subject
Fundamentalsatz der Zahlentheorie
de
dc.title
Program Extraction in Number Theory: The Fundamental Theorem of Arithmetic and Friends
en
dc.type
Presentation
en
dc.type
Vortrag
de
dc.relation.grantno
ESP 576-N
-
dc.type.category
Presentation
-
tuw.publication.invited
invited
-
tuw.project.title
Materielle Interpretation
-
tuw.researchTopic.id
I1
-
tuw.researchTopic.name
Logic and Computation
-
tuw.researchTopic.value
100
-
tuw.publication.orgunit
E104-02 - Forschungsbereich Computational Logic
-
tuw.event.name
Oberseminar Mathematische Logik 2025
de
tuw.event.startdate
23-04-2025
-
tuw.event.enddate
23-04-2025
-
tuw.event.online
On Site
-
tuw.event.type
Event for scientific audience
-
tuw.event.place
Ludwig-Maximilians Universität München
-
tuw.event.country
DE
-
tuw.event.presenter
Wiesnet, Franziskus
-
wb.sciencebranch
Informatik
-
wb.sciencebranch
Mathematik
-
wb.sciencebranch.oefos
1020
-
wb.sciencebranch.oefos
1010
-
wb.sciencebranch.value
5
-
wb.sciencebranch.value
95
-
item.openairetype
conference presentation
-
item.openairecristype
http://purl.org/coar/resource_type/R60J-J5BD
-
item.cerifentitytype
Publications
-
item.languageiso639-1
de
-
item.grantfulltext
none
-
item.fulltext
no Fulltext
-
crisitem.author.dept
E104-02 - Forschungsbereich Computational Logic
-
crisitem.author.parentorg
E104 - Institut für Diskrete Mathematik und Geometrie
