Contribution: ExactRealArithmetic

Exact Real Arithmetic

Authors

• Jérôme Creci

Description

This contribution contains a proof of correctness of some exact real arithmetic algorithms from the PhD thesis of Valérie Ménissier-Morain

Keywords

correctness, real numbers, arithmetic

Available files

• ExactRealArithmetic.Lemmes_generaux.html
• ExactRealArithmetic.Rind_complements.html
• ExactRealArithmetic.Zarith_inegalites.html
• ExactRealArithmetic.Rabsolu_complements.html
• ExactRealArithmetic.Oppose.html
• ExactRealArithmetic.Zarith_operations.html
• ExactRealArithmetic.Racine.html
• ExactRealArithmetic.Inverse.html
• ExactRealArithmetic.Zsqrt_complements.html
• ExactRealArithmetic.Zpower_complements.html
• ExactRealArithmetic.Addition.html
• ExactRealArithmetic.sg.html
• ExactRealArithmetic.Lemmes.html
• ExactRealArithmetic.Zdiv2_complements.html
• ExactRealArithmetic.Rlog.html
• ExactRealArithmetic.Axiomes.html
• ExactRealArithmetic.Zind_complements.html
• ExactRealArithmetic.Multiplication.html
• ExactRealArithmetic.Absolue.html
• ExactRealArithmetic.powerRZ_complements.html
• ExactRealArithmetic.Zsgn_complemnts.html
• ExactRealArithmetic.Rbase_doubles_inegalites.html
• ExactRealArithmetic.Zdec_complements.html
• ExactRealArithmetic.Rbase_inegalites.html
• ExactRealArithmetic.Tactiques.html
• ExactRealArithmetic.Rbase_operations.html
• ExactRealArithmetic.definition.html
• ExactRealArithmetic.Zmax.html
• ExactRealArithmetic.Zabs_complements.html