  In this paper we show that reversible analysis of logic languages by abstract
interpretation can be performed without loss of precision by systematically
refining abstract domains. The idea is to include semantic structures into
abstract domains in such a way that the refined abstract domain becomes rich
enough to allow approximate bottom-up and top-down semantics to agree. These
domains are known as condensing abstract domains. Substantially, an abstract
domain is condensing if goal-driven and goal-independent analyses agree, namely
no loss of precision is introduced by approximating queries in a
goal-independent analysis. We prove that condensation is an abstract domain
property and that the problem of making an abstract domain condensing boils
down to the problem of making the domain complete with respect to unification.
In a general abstract interpretation setting we show that when concrete domains
and operations give rise to quantales, i.e. models of propositional linear
logic, objects in a complete refined abstract domain can be explicitly
characterized by linear logic-based formulations. This is the case for abstract
domains for logic program analysis approximating computed answer substitutions
where unification plays the role of multiplicative conjunction in a quantale of
idempotent substitutions. Condensing abstract domains can therefore be
systematically derived by minimally extending any, generally non-condensing
domain, by a simple domain refinement operator.
