Skip to content

Source code for my PhD thesis "Towards justifying computer algebra algorithms in Isabelle/HOL"

License

Notifications You must be signed in to change notification settings

Wenda302/thesis-code

Repository files navigation

The proofs should be compatible with Isabelle2017.

The relationship between the thesis and the sources is as follows:

Chapter 3 -> Sturm_Tarski
Chapter 4 -> Real_Algebraic_Number
Chapter 5 -> Univ_RCF
Chapter 6 -> Residue_Example (NOTE: proof sources for the theorems have already been incorporated in Analysis/Conformal_Mappings.thy in the Isabelle distribution. This folder only contains an example of applying Cauchy's residue theorem to evaluate improper integrals.)
Chapter 7 -> Winding_Number_Eval & Counting_Complex_Roots
Chapter 8 -> Multivariate_CAD

where Rank_Nullity_Theorem is a supporting library (by Jose Divasón and Jesús Aransay) from AFP.

About

Source code for my PhD thesis "Towards justifying computer algebra algorithms in Isabelle/HOL"

Resources

License

Stars

Watchers

Forks

Packages

No packages published