NRCL -A model building approach to the Bernays-Schönfinkel fragment, Frontiers of Combining Systems -10th International Symposium, vol.9322, pp.69-84, 2015. ,
Lemma learning in the model evolution calculus, LPAR, vol.4246, pp.572-586, 2006. ,
LIA) -model evolution with linear integer arithmetic constraints, Logic for Programming, Artificial Intelligence, and Reasoning, 15th International Conference, vol.5330, pp.258-273, 2008. ,
Refutational theorem proving for hierarchic first-order theories, AAECC, vol.5, issue.3/4, pp.193-212, 1994. ,
Semantically-guided goal-sensitive reasoning: Model representation, Journal of Automated Reasoning, vol.56, issue.2, pp.113-141, 2016. ,
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
Description Logic, Theory Combination, and All That -Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday, Lecture Notes in Computer Science, vol.11560, pp.15-56, 2019. ,
Engineering DPLL(T) + saturation, Automated Reasoning, 4th International Joint Conference, vol.5195, pp.475-490, 2008. ,
Undecidability of presburger arithmetic with a single monadic predicate letter, 1972. ,
SCL clause learning from simple models, Automated Deduction -CADE 27 -27th International Conference on Automated Deduction, pp.233-249, 2019. ,
URL : https://hal.archives-ouvertes.fr/hal-02405550
Complete instantiation for quantified formulas in satisfiabiliby modulo theories, Computer Aided Verification, 21st International Conference, pp.306-320, 2009. ,
New directions in instatiation-based theorem proving, Samson Abramsky, editor, 18th Annual IEEE Symposium on Logic in Computer Science, LICS'03, LICS'03, pp.55-64, 2003. ,
The universal fragment of presburger arithmetic with unary uninterpreted predicates is undecidable, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01592177
Using CSP look-back techniques to solve real-world SAT instances, Proceedings of the Fourteenth National Conference on Artificial Intelligence and Ninth Innovative Applications of Artificial Intelligence Conference, AAAI 97, IAAI 97, pp.203-208, 1997. ,
Inst-gen -A modular approach to instantiation-based automated reasoning, Programming Logics -Essays in Memory of Harald Ganzinger, vol.7797, pp.239-270, 2013. ,
First-order theorem proving and vampire, Natasha Sharygina and Helmut Veith, editors, Computer Aided Verification -25th International Conference, CAV 2013, vol.8044, pp.1-35, 2013. ,
Superposition decides the first-order logic fragment over ground theories, Mathematics in Computer Science, vol.6, issue.4, pp.427-456, 2012. ,
Computation: Finite and Infinite Machines, 1967. ,
Solving SAT and SAT modulo theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T), Journal of the ACM, vol.53, pp.937-977, 2006. ,
Deciding effectively propositional logic using DPLL and substitution sets, Journal of Automated Reasoning, vol.44, issue.4, pp.401-424, 2010. ,
, ESCoR: FLoC'06 Workshop on Empirically Successful Computerized Reasoning, vol.192, pp.18-33, 2006.
Revisiting enumerative instantiation, Tools and Algorithms for the Construction and Analysis of Systems -24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, vol.10806, pp.112-131, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01744956
A constraint sequent calculus for first-order logic with linear integer arithmetic, LNCS, vol.5330, pp.274-289, 2008. ,
Between restarts and backjumps, Theory and Applications of Satisfiability Testing -SAT 2011 -14th International Conference, SAT 2011, vol.6695, pp.216-229, 2011. ,
Grasp -a new search algorithm for satisfiability, International Conference on Computer Aided Design, ICCAD, pp.220-227, 1996. ,
First-order logic theorem proving and model building via approximation and instantiation, Frontiers of Combining Systems, 10th International Symposium, vol.9322, pp.85-100, 2015. ,
The Bernays-Schönfinkel-Ramsey fragment with bounded difference constraints over the reals is decidable, Frontiers of Combining Systems -11th International Symposium, vol.10483, pp.244-261, 2017. ,
Automated reasoning building blocks, Correct System Design -Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday, vol.9360, pp.172-188, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01239428