Separation logic provided a breakthrough in reasoning about the heap in many
cases, making specs and proofs tractable and close to the programmer's
intuition. Its "frame rule" enables local reasoning by answering the frame
problem: describing what does not change when updating parts of the heap.
However, for algorithms exhibiting intrinsic sharing, neither separation logic
nor any other formalism has achieved simple proofs. We propose that most
programs manipulating graphs, DAGs, or overlaid data structures require an
answer to a different problem, the ramification problem (like the frame
problem, another classic AI problem): describing how global structures change
because of a local update. This work presents a solution in the form of a new
inference rule: the ramification rule, mixing separation logic and relevant
logic, and valid in any separation logic. We show how it allows sound and local
reasoning about effects on data structures with sharing.