  In this work we propose a multi-valued extension of logic programs under the
stable models semantics where each true atom in a model is associated with a
set of justifications, in a similar spirit than a set of proof trees. The main
contribution of this paper is that we capture justifications into an algebra of
truth values with three internal operations: an addition '+' representing
alternative justifications for a formula, a commutative product '*'
representing joint interaction of causes and a non-commutative product '.'
acting as a concatenation or proof constructor. Using this multi-valued
semantics, we obtain a one-to-one correspondence between the syntactic proof
tree of a standard (non-causal) logic program and the interpretation of each
true atom in a model. Furthermore, thanks to this algebraic characterization we
can detect semantic properties like redundancy and relevance of the obtained
justifications. We also identify a lattice-based characterization of this
algebra, defining a direct consequences operator, proving its continuity and
that its least fix point can be computed after a finite number of iterations.
Finally, we define the concept of causal stable model by introducing an
analogous transformation to Gelfond and Lifschitz's program reduct.
