Superposition modulo linear arithmetic SUP(LA), FroCos, vol.5749, pp.84-99, 2009. ,
New results on rewritebased satisfiability procedures, ACM Trans. Comput. Log, vol.10, issue.1, 2009. ,
URL : https://hal.archives-ouvertes.fr/inria-00576862
Rewrite-based equational theorem proving with selection and simplification, Journal of Logic and Computation, vol.4, issue.3, pp.217-247, 1994. ,
Resolution Theorem Proving, Handbook of Automated Reasoning, 2001. ,
Refutational theorem proving for hierarchic first-order theories, Appl. Algebra Eng. Commun. Comput, vol.5, pp.193-212, 1994. ,
, Computer Aided Verification, vol.6806, pp.171-177, 2011.
Beagle -A Hierarchic Superposition Theorem Prover, 25th International Conference on Automated Deduction, vol.9195, pp.367-377, 2015. ,
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. ,
Model evolution with equality modulo built-in theories, CADE-23 -The 23nd International Conference on Automated Deduction, vol.6803, pp.85-100, 2011. ,
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
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
Hierarchic superposition revisited, 2019. ,
URL : https://hal.archives-ouvertes.fr/hal-02402941
On deciding satisfiability by theorem proving with speculative inferences, J. Autom. Reasoning, vol.47, issue.2, pp.161-189, 2011. ,
Engineering DPLL(T) + saturation, Automated Reasoning, 4th International Joint Conference, IJCAR, vol.5195, pp.475-490, 2008. ,
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. ,
Theory instantiation, 13th Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'06), vol.4246, pp.497-511, 2006. ,
Solving quantified verification conditions using satisfiability modulo theories, 21st International Conference on Automated Deduction, vol.4603, 2007. ,
Complete instantiation for quantified formulas in satisfiabiliby modulo theories, CAV, vol.5643, pp.306-320, 2009. ,
Integrating linear arithmetic into superposition calculus, Computer Science Logic (CSL'07), vol.4646, pp.223-237, 2007. ,
First-order theorem proving and Vampire, Computer Aided Verification -25th International Conference, CAV, vol.8044, pp.1-35 ,
, , 2013.
Superposition Modulo Theory. Doctoral dissertation, 2013. ,
Superposition decides the first-order logic fragment over ground theories, Mathematics in Computer Science, vol.6, pp.427-456, 2012. ,
First-order completion techniques, 1991. ,
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. ,
Paramodulation-based theorem proving, Handbook of Automated Reasoning, pp.371-443, 2001. ,
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. ,
The TPTP Problem Library and Associated Infrastructure. From CNF to TH0, Journal of Automated Reasoning, vol.59, issue.4, pp.483-502, 2017. ,
Many-sorted unification, Journal of the ACM, vol.35, issue.1, pp.1-17, 1988. ,
SPASS version 3.5, 22nd International Conference on Automated Deduction, vol.5663, pp.140-145, 2009. ,