E. Althaus, E. Kruglov, and C. Weidenbach, Superposition modulo linear arithmetic SUP(LA), FroCos, vol.5749, pp.84-99, 2009.

A. Armando, M. P. Bonacina, S. Ranise, and S. Schulz, New results on rewritebased satisfiability procedures, ACM Trans. Comput. Log, vol.10, issue.1, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00576862

L. Bachmair and H. Ganzinger, Rewrite-based equational theorem proving with selection and simplification, Journal of Logic and Computation, vol.4, issue.3, pp.217-247, 1994.

L. Bachmair and H. Ganzinger, Resolution Theorem Proving, Handbook of Automated Reasoning, 2001.

L. Bachmair, H. Ganzinger, and U. Waldmann, Refutational theorem proving for hierarchic first-order theories, Appl. Algebra Eng. Commun. Comput, vol.5, pp.193-212, 1994.

C. Barrett, C. L. Conway, M. Deters, L. Hadarean, D. Jovanovi? et al., Computer Aided Verification, vol.6806, pp.171-177, 2011.

P. Baumgartner, J. Bax, and U. Waldmann, Beagle -A Hierarchic Superposition Theorem Prover, 25th International Conference on Automated Deduction, vol.9195, pp.367-377, 2015.

P. Baumgartner, A. Fuchs, and C. Tinelli, ME(LIA) -Model Evolution With Linear Integer Arithmetic Constraints, 15th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR'08), vol.5330, pp.258-273, 2008.

P. Baumgartner and C. Tinelli, Model evolution with equality modulo built-in theories, CADE-23 -The 23nd International Conference on Automated Deduction, vol.6803, pp.85-100, 2011.

P. Baumgartner and U. Waldmann, Hierarchic superposition: Completeness without compactness, Fifth International Conference on Mathematical Aspects of Computer and Information Sciences, MACIS 2013, pp.8-12, 2013.
URL : https://hal.archives-ouvertes.fr/hal-01087872

P. Baumgartner and U. Waldmann, Hierarchic superposition with weak abstraction, 24th International Conference on Automated Deduction, vol.7898, pp.39-57, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00931919

P. Baumgartner and U. Waldmann, Hierarchic superposition revisited, 2019.
URL : https://hal.archives-ouvertes.fr/hal-02402941

M. P. Bonacina, C. Lynch, and L. M. De-moura, On deciding satisfiability by theorem proving with speculative inferences, J. Autom. Reasoning, vol.47, issue.2, pp.161-189, 2011.

L. M. De-moura and N. Bjørner, Engineering DPLL(T) + saturation, Automated Reasoning, 4th International Joint Conference, IJCAR, vol.5195, pp.475-490, 2008.

L. E. Dickson, Finiteness of the Odd Perfect and Primitive Abundant Numbers with n Distinct Prime Factors, Amer. J. Math, vol.35, issue.4, pp.413-422, 1913.

H. Ganzinger and K. Korovin, Theory instantiation, 13th Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'06), vol.4246, pp.497-511, 2006.

Y. Ge, C. Barrett, and C. Tinelli, Solving quantified verification conditions using satisfiability modulo theories, 21st International Conference on Automated Deduction, vol.4603, 2007.

Y. Ge and L. M. De-moura, Complete instantiation for quantified formulas in satisfiabiliby modulo theories, CAV, vol.5643, pp.306-320, 2009.

K. Korovin and A. Voronkov, Integrating linear arithmetic into superposition calculus, Computer Science Logic (CSL'07), vol.4646, pp.223-237, 2007.

L. Kovács and A. Voronkov, First-order theorem proving and Vampire, Computer Aided Verification -25th International Conference, CAV, vol.8044, pp.1-35

. Springer, , 2013.

E. Kruglov, Superposition Modulo Theory. Doctoral dissertation, 2013.

E. Kruglov and C. Weidenbach, Superposition decides the first-order logic fragment over ground theories, Mathematics in Computer Science, vol.6, pp.427-456, 2012.

R. Nieuwenhuis, First-order completion techniques, 1991.

R. Nieuwenhuis, A. Oliveras, and C. Tinelli, Solving SAT and SAT Modulo Theories: from an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T), Journal of the ACM, vol.53, issue.6, pp.937-977, 2006.

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

P. Rümmer, A constraint sequent calculus for first-order logic with linear integer arithmetic, 15th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR'08), vol.5330, pp.274-289, 2008.

G. Sutcliffe, The TPTP Problem Library and Associated Infrastructure. From CNF to TH0, Journal of Automated Reasoning, vol.59, issue.4, pp.483-502, 2017.

C. Walther, Many-sorted unification, Journal of the ACM, vol.35, issue.1, pp.1-17, 1988.

C. Weidenbach, D. Dimova, A. Fietzke, R. Kumar, M. Suda et al., SPASS version 3.5, 22nd International Conference on Automated Deduction, vol.5663, pp.140-145, 2009.