New results on rewritebased satisfiability procedures, ACM Trans. Comput. Log, vol.10, issue.1, 2009. ,
URL : https://hal.archives-ouvertes.fr/inria-00576862
A rewriting approach to satisfiability procedures, Inf. Comput, vol.183, issue.2, pp.140-164, 2003. ,
Connecting many-sorted theories, J. Symb. Log, vol.72, issue.2, pp.535-583, 2007. ,
Term rewriting and all that, 1998. ,
Rewrite-based equational theorem proving with selection and simplification, J. Log. Comput, vol.4, issue.3, pp.217-247, 1994. ,
An abstract decision procedure for a theory of inductive data types, JSAT, vol.3, issue.1-2, pp.21-46, 2007. ,
Hierarchic superposition with weak abstraction, Automated Deduction -CADE-24 -24th International Conference on Automated Deduction, vol.7898, pp.39-57, 2013. ,
URL : https://hal.archives-ouvertes.fr/hal-00931919
A Gentle Non-Disjoint Combination of Satisfiability Procedures, Proc. of the 7th International Joint Conference on Automated Reasoning, IJCAR, vol.8562, pp.122-136, 2014. ,
URL : https://hal.archives-ouvertes.fr/hal-01087162
A Polite Non-Disjoint Combination Method: Theories with Bridging Functions Revisited, Automated Deduction -CADE-25 -25th International Conference on Automated Deduction, vol.9195, pp.419-433, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01157898
A rewriting approach to the combination of data structures with bridging theories, Frontiers of Combining Systems (FroCoS), vol.9322, pp.275-290, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01206187
Combining lists with non-stably infinite theories, Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'04), vol.3452, pp.51-66, 2005. ,
URL : https://hal.archives-ouvertes.fr/inria-00000481
Model-theoretic methods in combined constraint satisfiability, Journal of Automated Reasoning, vol.33, issue.3-4, pp.221-249, 2004. ,
Polite theories revisited, Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'10), vol.6397, pp.402-416 ,
, , 2010.
Superposition decides the first-order logic fragment over ground theories, Mathematics in Computer Science, vol.6, issue.4, pp.427-456, 2012. ,
Simplification by cooperating decision procedures, ACM Trans. on Programming Languages and Systems, vol.1, issue.2, pp.245-257, 1979. ,
Combinable extensions of Abelian groups, 22nd International Conference on Automated Deduction, vol.5663, pp.51-66, 2009. ,
URL : https://hal.archives-ouvertes.fr/inria-00383041
Combining satisfiability procedures for unions of theories with a shared counting operator, Fundam. Inform, vol.105, issue.1-2, pp.163-187, 2010. ,
URL : https://hal.archives-ouvertes.fr/inria-00526683
Reasoning about recursively defined data structures, J. ACM, vol.27, issue.3, pp.403-411, 1980. ,
Reasoning about algebraic data types with abstractions, J. Autom. Reasoning, vol.57, issue.4, pp.281-318, 2016. ,
Combining data structures with nonstably infinite theories using many-sorted logic, Frontiers of Combining Systems (FroCoS), vol.3717, pp.48-64, 2005. ,
URL : https://hal.archives-ouvertes.fr/inria-00070335
A practical decision procedure for arithmetic with function symbols, J. ACM, vol.26, issue.2, pp.351-360, 1979. ,
Locality results for certain extensions of theories with bridging functions, 22nd International Conference on Automated Deduction, vol.5663, pp.67-83, 2009. ,
Automated reasoning in extensions of theories of constructors with recursively defined functions and homomorphisms, Interaction versus Automation: The two Faces of Deduction, number 09411 in Dagstuhl Seminar Proceedings. Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, 2010. ,
Decision procedures for algebraic data types with abstractions, Principles of Programming Languages (POPL), pp.199-210, 2010. ,
Satisfiability modulo recursive programs, Static Analysis -18th International Symposium, vol.6887, pp.298-315, 2011. ,
Cooperation of background reasoners in theory reasoning by residue sharing, J. Autom. Reasoning, vol.30, issue.1, pp.1-31, 2003. ,
A new correctness proof of the Nelson-Oppen combination procedure, Frontiers of Combining Systems (FroCoS), Applied Logic, pp.103-120, 1996. ,
Unions of non-disjoint theories and combinations of satisfiability procedures, Theoretical Comput. Sci, vol.290, issue.1, pp.291-353, 2003. ,
URL : https://hal.archives-ouvertes.fr/inria-00099668
Combination of convex theories: Modularity, deduction completeness, and explanation, J. Symb. Comput, vol.45, issue.2, pp.261-286, 2010. ,
URL : https://hal.archives-ouvertes.fr/inria-00331479
Combining theories with shared set operations, Frontiers of Combining Systems, vol.5749, pp.366-382, 2009. ,
Combining lists with integers, International Joint Conference on Automated Reasoning (Short Papers), pp.170-179, 2001. ,
Combining multisets with integers, 18th International Conference on Automated Deduction, vol.2392, pp.363-376, 2002. ,
Combining sets with cardinals, J. Autom. Reasoning, vol.34, issue.1, pp.1-29, 2005. ,
Decision procedures for term algebras with integer constraints, Inf. Comput, vol.204, issue.10, pp.1526-1574, 2006. ,