In abstract algebra, a partially ordered ring is a ring (A, +, ·), together with a compatible partial order, that is, a partial order on the underlying set A that is compatible with the ring operations in the sense that it satisfies: and for all .^{[1]} Various extensions of this definition exist that constrain the ring, the partial order, or both. For example, an Archimedean partially ordered ring is a partially ordered ring where 's partially ordered additive group is Archimedean.^{[2]}
An ordered ring, also called a totally ordered ring, is a partially ordered ring where is additionally a total order.^{[1]}^{[2]}
An lring, or latticeordered ring, is a partially ordered ring where is additionally a lattice order.
The additive group of a partially ordered ring is always a partially ordered group.
The set of nonnegative elements of a partially ordered ring (the set of elements for which also called the positive cone of the ring) is closed under addition and multiplication, that is, if is the set of nonnegative elements of a partially ordered ring, then and Furthermore,
The mapping of the compatible partial order on a ring to the set of its nonnegative elements is onetoone;^{[1]} that is, the compatible partial order uniquely determines the set of nonnegative elements, and a set of elements uniquely determines the compatible partial order if one exists.
If is a subset of a ring and:
then the relation where if and only if defines a compatible partial order on (that is, is a partially ordered ring).^{[2]}
In any lring, the absolute value of an element can be defined to be where denotes the maximal element. For any and holds.^{[3]}
An fring, or Pierce–Birkhoff ring, is a latticeordered ring in which ^{[4]} and imply that for all They were first introduced by Garrett Birkhoff and Richard S. Pierce in 1956, in a paper titled "Latticeordered rings", in an attempt to restrict the class of lrings so as to eliminate a number of pathological examples. For example, Birkhoff and Pierce demonstrated an lring with 1 in which 1 is not positive, even though it is a square.^{[2]} The additional hypothesis required of frings eliminates this possibility.
Let be a Hausdorff space, and be the space of all continuous, realvalued functions on is an Archimedean fring with 1 under the following pointwise operations: ^{[2]}
From an algebraic point of view the rings are fairly rigid. For example, localisations, residue rings or limits of rings of the form are not of this form in general. A much more flexible class of frings containing all rings of continuous functions and resembling many of the properties of these rings is the class of real closed rings.
IsarMathLib, a library for the Isabelle theorem prover, has formal verifications of a few fundamental results on commutative ordered rings. The results are proved in the ring1
context.^{[6]}
Suppose is a commutative ordered ring, and Then:
by  

The additive group of is an ordered group  OrdRing_ZF_1_L4

OrdRing_ZF_1_L7
 
and imply and 
OrdRing_ZF_1_L9

ordring_one_is_nonneg
 
OrdRing_ZF_2_L5
 
ord_ring_triangle_ineq
 
is either in the positive set, equal to 0 or in minus the positive set.  OrdRing_ZF_3_L2

The set of positive elements of is closed under multiplication if and only if has no zero divisors.  OrdRing_ZF_3_L3

If is nontrivial (), then it is infinite.  ord_ring_infinite
