<div class="csl-bib-body">
<div class="csl-entry">Wiesnet, F. (2025, May 16). <i>Program Extraction in Elementary Arithmetic: Fundamental Theorem of Arithmetic and Friends</i> [Conference Presentation]. Proof, Argumentation, Computation, Modalities and Negation (PACMAN 2025), Rom, Italy. http://hdl.handle.net/20.500.12708/223915</div>
</div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/223915
-
dc.description.abstract
We introduce the theory of formal program extraction from proofs, focusing on examples from elementary number theory.
In particular, we explore the computational content of Bézout’s Lemma, the Fundamental Theorem of Elementary Number Theory, and Fermat’s Factorization. The extraction process was carried out using the proof assistant Minlog, with the resulting programs translated into Haskell code, which we will present and discuss. We will also look at the challenges that arise during formalization in Minlog and explain how the way a proof is constructed impact the efficiency of the extracted programs.
en
dc.description.sponsorship
FWF - Österr. Wissenschaftsfonds
-
dc.language.iso
en
-
dc.subject
Numbertheory
en
dc.subject
Program extraction
en
dc.subject
Minlog
en
dc.subject
factorisation methods
en
dc.subject
Fundamental Rheorem of Arithmetic
en
dc.title
Program Extraction in Elementary Arithmetic: Fundamental Theorem of Arithmetic and Friends
en
dc.type
Presentation
en
dc.type
Vortrag
de
dc.relation.grantno
ESP 576-N
-
dc.type.category
Conference 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
Proof, Argumentation, Computation, Modalities and Negation (PACMAN 2025)
en
tuw.event.startdate
14-05-2025
-
tuw.event.enddate
16-05-2025
-
tuw.event.online
On Site
-
tuw.event.type
Event for scientific audience
-
tuw.event.place
Rom
-
tuw.event.country
IT
-
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 paper not in proceedings
-
item.openairecristype
http://purl.org/coar/resource_type/c_18cp
-
item.cerifentitytype
Publications
-
item.languageiso639-1
en
-
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
