Charoula Poullaidou Undergraduate Dissertation 2016/17

Implementing Tarski's High School Algebra and Tarski's Geometry in Isabelle/HOL

Supervised by G.Struth

Abstract

This project aims to study Tarski's work in two specific areas and implement Tarski's Axioms in Isabelle, an interactive theorem prover. More specifically, Tarski's contribution in Algebra which included Tarski's High School Axioms will be researched and implemented in Isabelle/HOL. Wilkie's counterexample on Tarski's Identities problem will be examined in the same environment. Finally, the project continues on to Tarski's Geometry Axioms work, while showing the axioms' independency and proving how they took their latest form.