On the implication problem for factorizations of discrete probability distributions

We address the problem of the existence of an algorithm that allows us to decide if a given set of full factorization constraints implies another full factorization constraint. In order to solve this problem, whose decidability is still under question, we present a time-exponential algorithm which enjoys the Church-Rosser property and whose output is a variable that can assume only two values: either success or failure. We prove that for a given instance of the implication problem, if the algorithm terminates with success, then the implication holds.