-
Notifications
You must be signed in to change notification settings - Fork 0
Source code for my PhD thesis "Towards justifying computer algebra algorithms in Isabelle/HOL"
License
Wenda302/thesis-code
Folders and files
Name | Name | Last commit message | Last commit date | |
---|---|---|---|---|
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 0
No packages published