Computing minimal axiomatisations in Gödel propositional logic

We solve the minimization problem for finitely axiomatizable theories in Gödel infinite-valued propositional logic. That is, we obtain an algorithm that when input a formula α(X1,..,Xn) outputs a formula β(X1,..,Xm) such that (i) the theories singly axiomatized by α and β have isomorphic algebraic semantics, and (ii) if β'(X1,..,Xm') is any formula satisfying (i), then m'≥m.