A new proof of Euclid's algorithm
Logic in Computer Science
2023-11-06 v1 Data Structures and Algorithms
Logic
Abstract
Our main result is a new proof of correctness of Euclid's algorithm. The proof is conducted in algorithmic theory of natural numbers Th3. A formula H is constructed that expresses the halting property of the algorithm. Next, the proof of H is is presented. In the proof we make use of inference rules of calculus of programs. The only formulas accepted without the proof are axioms of program calculus or axioms of the theory Th3. We complete our result by showing that the theorem on correctness of Euclid's algorithm can not be proved in any elementary theory of natural numbers.
Cite
@article{arxiv.2311.01474,
title = {A new proof of Euclid's algorithm},
author = {Andrzej Salwicki},
journal= {arXiv preprint arXiv:2311.01474},
year = {2023}
}