L. Bachmair, N. Dershowitz, and D. A. Plaisted, Completion without failure, Rewriting Techniques-Resolution of Equations in Algebraic Structures, vol.2, pp.1-30, 1989.

L. Bachmair and H. Ganzinger, Rewrite-based equational theorem proving with selection and simplification, J. Log. Comput, vol.4, issue.3, pp.217-247, 1994.

L. Bachmair and H. Ganzinger, Resolution theorem proving, Handbook of Automated Reasoning, vol.I, pp.19-99, 2001.

C. Ballarin, Locales: A module system for mathematical theories, J. Autom. Reason, vol.52, issue.2, pp.123-153, 2014.

J. Biendarra, J. C. Blanchette, A. Bouzy, M. Desharnais, M. Fleury et al., Foundational (co)datatypes and (co)recursion for higher-order logic, FroCoS 2017, vol.10483, pp.3-21, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01592196

J. C. Blanchette, M. Fleury, P. Lammich, and C. Weidenbach, A verified SAT solver framework with learn, forget, restart, and incrementality, Accepted in J. Autom. Reason
URL : https://hal.archives-ouvertes.fr/hal-01592164

J. C. Blanchette, M. Fleury, and D. Traytel, Nested multisets, hereditary multisets, and syntactic ordinals in Isabelle/HOL, FSCD 2017. LIPIcs, vol.84, pp.1-11, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01599176

J. C. Blanchette, C. Kaliszyk, L. C. Paulson, and J. Urban, Hammering towards QED, J. Formaliz. Reason, vol.9, issue.1, pp.101-148, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01386988

J. C. Blanchette, A. Popescu, and D. Traytel, Soundness and completeness proofs by coinductive methods, J. Autom. Reason, vol.58, issue.1, pp.149-179, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01643157

D. Brand, Proving theorems with the modifiction method, SIAM J. Comput, vol.4, issue.4, pp.412-430, 1975.

S. Cruanes, Logtk: A logic toolkit for automated reasoning and its implementation, EPiC Series in Computing, vol.31, pp.39-49, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01101057

M. Fleury, J. C. Blanchette, and P. Lammich, A verified SAT solver with watched literals using Imperative HOL, pp.158-171, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01904647

N. Hirokawa, A. Middeldorp, C. Sternagel, and S. Winkler, Infinite runs in abstract completion, 16. Schloss DagstuhlLeibniz-Zentrum für Informatik, vol.84, pp.1-19, 2017.

R. Nieuwenhuis and A. Rubio, Paramodulation-based theorem proving, Handbook of Automated Reasoning, vol.I, pp.371-443, 2001.

T. Nipkow, Teaching semantics with a proof assistant: No more LSD trip proofs, VMCAI 2012, vol.7148, pp.24-38, 2012.

T. Nipkow, L. C. Paulson, and M. Wenzel, Isabelle/HOL: A Proof Assistant for Higher-Order Logic, vol.2283, 2002.

N. Peltier, A variant of the superposition calculus, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01383903

H. Persson, Constructive completeness of intuitionistic predicate logic-a formalisation in type theory, 1996.

B. C. Pierce, Lambda, the ultimate TA: Using a proof assistant to teach programming language foundations, pp.121-122, 2009.

A. Schlichtkrull, Formalization of the resolution calculus for first-order logic, Accepted in J. Autom. Reason

A. Schlichtkrull, J. C. Blanchette, D. Traytel, and U. Waldmann, Formalizing Bachmair and Ganzinger's ordered resolution prover (technical report), 2018.

N. Shankar, Towards mechanical metamathematics, J. Autom. Reason, vol.1, issue.4, pp.407-434, 1985.

R. Thiemann and C. Sternagel, Certification of termination proofs using CeTA, TPHOLs 2009, vol.5674, pp.452-468, 2009.

A. Voronkov, AVATAR: The architecture for first-order theorem provers, CAV 2014, vol.8559, pp.696-710, 2014.

D. Wand, Polymorphic+typeclass superposition, EPiC Series in Computing, vol.31, pp.105-119, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01098078

C. Weidenbach, Combining superposition, sorts and splitting, Handbook of Automated Reasoning, vol.II, pp.1965-2013, 2001.

M. Wenzel, Isabelle/Isar-a generic framework for human-readable proof documents, Studies in Logic, Grammar, and Rhetoric, vol.10, issue.23, 2007.

M. Wenzel, J. Jeuring, J. A. Campbell, J. Carette, G. D. Reis et al., Isabelle/jEdit-a prover IDE within the PIDE framework, CICM 2012, vol.7362, pp.468-471, 2012.

H. Zhang and D. Kapur, First-order theorem proving using conditional rewrite rules, CADE-9, vol.310, pp.1-20, 1988.