  By exploiting the algebraic and order theoretic mechanisms behind Sahlqvist
correspondence, the theory of unified correspondence provides powerful tools
for correspondence and canonicity across different semantics and signatures,
covering all the logics whose algebraic semantics are given by normal
(distributive) lattice expansions (referred to as (D)LEs). In particular, the
algorithm ALBA, parametric in each (D)LE, effectively computes the first order
correspondents of (D)LE-inductive formulas. We present an algorithm that makes
use of ALBA's rules and algebraic language to invert its steps in the DLE
setting; therefore effectively computing an inductive formula starting from its
first order correspondent.
