Derivative algebra (abstract algebra)

In abstract algebra, a derivative algebra is an algebraic structure of the signature

where
is a Boolean algebra and ^D is a unary operator, the derivative operator, satisfying the identities:

0^D = 0
x^DD ≤ x + x^D
^D = x^D + y^D.

x^D is called the derivative of x. Derivative algebras provide an algebraic abstraction of the derived set operator in topology. They also play the same role for the modal logic wK4 = K + that Boolean algebras play for ordinary propositional logic.