Unit:
Department of Informatics and TelecommunicationsΠληροφορική
Author:
PANAGIOTOPOULOS GEORGIOS
Supervisors info:
Ροντογιάννης Παναγιώτης, Καθηγητής, Τμήμα Πληροφορικής και Τηλεπικοινωνιών, Εθνικό και Καποδιστριακό Πανεπιστήμιο Αθηνών
Άγγελος Χαραλαμπίδης, Επίκουρος Καθηγητής, Τμήμα Πληροφορικής και Τηλεματικής, Χαροκόπειο Πανεπιστήμιο
Original Title:
Formalized Proofs of the Extension of Consistent Approximation Fixpoint Theory
Translated title:
Formalized Proofs of the Extension of Consistent Approximation Fixpoint Theory
Summary:
The purpose of this thesis is to formalize key proofs within the framework of consistent approximation fixpoint theory using the Lean 4 theorem prover, with the aim to refine the proofs themselves as well as verify their results. This is accomplished by constraining the formalization process to already verified tools, specifically the Lean base library and Mathlib.
Main subject category:
Technology - Computer science
Keywords:
lattice, fixpoint, logic, proof, lean
