CLEARSY / pptranspog

Encoding of proof obligations generated by Atelier B to typed first-order formats (SMT, TPTP) using the ppTrans approach
GNU General Public License v3.0
0 stars 2 forks source link

Axiomatization of exponentiation #10

Closed DavidDeharbe closed 11 months ago

DavidDeharbe commented 11 months ago

The B language reference manual defines the value of x^0 to be 1, when x is an INTEGER. The axiomatic definition of the translation of this operator does not give a value for 0^0. It should give the value 1.