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
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. ,
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. ,