Separation logic is a formalism designed to symbolically reason about computer programs that dynamically allocate data structures on memory. It allows to one mathematically _prove_ the correctness of such programs, for example showing the absence of memory leaks or violations. Using this proof system theoreticians could provide much cleaner and succinct proofs on the whiteboard, but their efforts to automate such reasoning process faced a number of limitations. Standard automated theorem proving techniques, based e.g. on resolution, did not seem to naturally apply to the new logic; thus researchers opted either to implement reasoning tools from scratch---missing the opportunity to exploit advances in modern theorem proving---or seek alternatives that avoid the perceived nuances of separation logic altogether---missing the conceptual advantages that separation logic _does_ provide. This research proposal seeks to demonstrate that modern theorem proving techniques are, in fact, compatible with separation logic reasoning. An approach that leads not only to much more efficient separation logic reasoners, but also broadens the scope of applications in which automated theorem proving can be practically applied.