We give an elementary theory of Henselian local rings and construct the Henselisation of a local ring. All our theorems have an algorithmic content.

This article is a logical continuation of the Henri Lombardi and Franz-Viktor Kuhlmann article [9]. We address some classical points of the theory of valued fields with an elementary and constructive point of view. We deal with Krull valuations, and not simply discrete valuations. First of all, we show how to construct the Henselization of a valued field; we restrict to fields in which one has at one's disposal algorithmic tools to test the nullity or the valuation ring membership. It (...) is therefore a work that differs as much in spirit as in field of application from that of Mines, Richman and Bridges , who address the framework of Heyting fields and discrete valuation. We show then in a constructive way a batch of classical results in Henselian fields, notably factorization criteria and Krasner's Lemma. We conclude by a construction of the inertia field of a valued field. (shrink)

We give a constructive treatment of the theory of Noetherian rings. We avoid the usual restriction to coherent rings; we can even deal with non-discrete rings. We introduce the concept of rings with certifiable equality which covers discrete rings and much more. A ring R with certifiable equality can be fitted with a partial ideal membership test for ideals of R. Lazy bases of ideals of R [X ] are introduced in order to derive a partial ideal membership test for (...) ideals of R [X ]. It is then proved that if R is Noetherian, then so is R [X ]. (shrink)