L. M. De-moura and G. O. Passmore, The Strategy Challenge in SMT Solving, Automated Reasoning and Mathematics -Essays in Memory of William W. McCune, pp.15-44, 2013.
DOI : 10.1007/978-3-642-17511-4_27

M. Farooque, S. Graham-lengrand, and A. Mahboubi, A bisimulation between DPLL(T) and a proof-search strategy for the focused sequent calculus Work. on Logical Frameworks and Meta-Languages: Theory and Practice Psyche: a proof-search engine based on sequent calculus with an LCF-style architecture, Proc. of the 2013 Int GL13. S. Graham-Lengrand Proc. of the 22nd Int. Conf. on Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux'13), pp.149-156, 2013.

G. H. Ganzinger, H. Rueb, N. N. Shankar-sha05, and . Shankar, Modularity and refinement in inference systems Technical Report SRI-CSL-04-02, SRI Inference systems for logical algorithms, Proc. of the 25th Int. Conf. on Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'05), pp.60-78, 2004.