G. Alagi and C. Weidenbach, NRCL -A model building approach to the bernaysschönfinkel fragment, Frontiers of Combining Systems -10th International Symposium, vol.9322, pp.69-84, 2015.

L. Bachmair and H. Ganzinger, Rewrite-based equational theorem proving with selection and simplification, Revised version of Max-Planck-Institut für Informatik technical report, vol.4, pp.217-247, 1991.

P. Bernays and M. Schönfinkel, Zum entscheidungsproblem der mathematischen logik, Mathematische Annalen, vol.99, pp.342-372, 1928.

A. Biere, M. Heule, T. Hans-van-maaren, and . Walsh, Handbook of Satisfiability, vol.185, 2009.

. Jasmin-christian, M. Blanchette, C. Fleury, and . Weidenbach, A verified SAT solver framework with learn, forget, restart, and incrementality, Automated Reasoning -8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, vol.9706, pp.25-44, 2016.

A. R. Bradley and Z. Manna, The Calculus of Computation -Decision Procedures with Applications to Verification, 2007.

M. Bromberger, A reduction from unbounded linear mixed arithmetic problems into bounded problems, Automated Reasoning -9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC, vol.10900, pp.329-345, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01942228

M. Bromberger, T. Sturm, and C. Weidenbach, Linear integer arithmetic revisited, Automated Deduction -CADE-25 -25th International Conference on Automated Deduction, vol.9195, pp.623-637, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01239394

M. Bromberger and C. Weidenbach, New techniques for linear arithmetic: cubes and equalities, Formal Methods in System Design, vol.51, issue.3, pp.433-461, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01656397

A. Fiori and C. Weidenbach, Scl -clause learning from simple models, Automated Deduction -CADE-27, 27th International Conference on Automated Deduction, 2019.
URL : https://hal.archives-ouvertes.fr/hal-02405550

R. M. Karp, Reducibility among combinatorial problems, Proceedings of a symposium on the Complexity of Computer Computations, pp.85-103, 1972.

D. Kroening and O. Strichman, Decision Procedures An Algorithmic Point of View. Texts in Theoretical Computer Science, 2008.

M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik, Chaff: Engineering an efficient sat solver, Design Automation Conference, pp.530-535, 2001.

C. H. Papadimitriou, On the complexity of integer programming, Journal of the ACM, vol.28, issue.4, pp.765-768, 1981.

J. A. , N. Pérez, and A. Voronkov, Proof systems for effectively propositional logic, Automated Reasoning, 4th International Joint Conference, vol.5195, pp.426-440, 2008.

K. Pipatsrisawat and A. Darwiche, On the power of clause-learning sat solvers with restarts, CP, vol.5732, pp.654-668, 2009.

D. A. Plaisted, Complete problems in the first-order predicate calculus, Journal of Computer and System Sciences, vol.29, pp.8-35, 1984.

P. M. João, K. A. Silva, and . Sakallah, Grasp -a new search algorithm for satisfiability, International Conference on Computer Aided Design, ICCAD, pp.220-227, 1996.

F. M. Suchanek, G. Kasneci, and G. Weikum, Yago: a core of semantic knowledge, Proceedings of the 16th International Conference on World Wide Web, pp.697-706, 2007.
URL : https://hal.archives-ouvertes.fr/hal-01472497

M. Suda, C. Weidenbach, and P. Wischnewski, On the saturation of yago, Automated Reasoning, 5th International Joint Conference, IJCAR 2010, vol.6173, pp.441-456, 2010.

C. Weidenbach, Do portfolio solvers harm, 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements, vol.51, pp.76-81, 2017.