A rewriting approach to satisfiability procedures, Information and Computation, vol.183, issue.2, pp.140-164, 2003. ,
DOI : 10.1016/S0890-5401(03)00020-8
New results on rewrite-based satisfiability procedures, ACM Transactions on Computational Logic, vol.10, issue.1, 2008. ,
DOI : 10.1145/1459010.1459014
URL : https://hal.archives-ouvertes.fr/inria-00576862
Abstract Congruence Closure, Journal of Automated Reasoning, vol.31, issue.2, pp.129-168, 2003. ,
DOI : 10.1023/B:JARS.0000009518.26415.49
URL : https://hal.archives-ouvertes.fr/inria-00099511
A generalization of Shostak's method for combining decision procedures, Proc. of the 4th International Workshop on Frontiers of Combining Systems, FroCoS'02, pp.132-147, 2002. ,
Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures, Proc. of the 3rd Int. Conference on Automated Reasoning (IJCAR'06), pp.513-527, 2006. ,
DOI : 10.1007/11814771_42
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.109.2926
Combining Unification Algorithms, Journal of Symbolic Computation, vol.16, issue.6, pp.597-626, 1993. ,
DOI : 10.1006/jsco.1993.1066
URL : http://doi.org/10.1006/jsco.1993.1066
Efficient theory combination via boolean search, Information and Computation, vol.204, issue.10, pp.1493-1525, 2006. ,
DOI : 10.1016/j.ic.2005.05.011
URL : http://doi.org/10.1016/j.ic.2005.05.011
What???s Decidable About Arrays?, Proc. of the 7th Int. Conf. on Verification, Model Checking, and Abstract Interpretation (VMCAI'06), pp.427-442, 2006. ,
DOI : 10.1007/11609773_28
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.119.4969
Strategies for combining decision procedures Conference on Tools and Algorithms for the Construction and Analysis of Systems, Proc. of the 9th Int, pp.537-553, 2003. ,
Canonization for disjoint unions of theories, Proc. of the 19th International Conference on Automated Deduction (CADE'03), pp.197-211, 2003. ,
On Shostak's decision procedure for combinations of theories, Proc. of the 13th International Conference on Automated Deduction, pp.463-477, 1996. ,
DOI : 10.1007/3-540-61511-3_107
Justifying Equality, Selected Papers from the Workshops on Disproving and the Second International Workshop on Pragmatics of Decision Procedures Issue 3 of Electronic Notes in Theoretical Computer Science (ENTCS), pp.69-85, 2004. ,
DOI : 10.1016/j.entcs.2004.06.068
Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, chapter 6: Rewrite Systems, pp.244-320, 1990. ,
Simplify: a theorem prover for program checking, Journal of the ACM, vol.52, issue.3, pp.365-473, 2005. ,
DOI : 10.1145/1066100.1066102
Variations on the Common Subexpression Problem, Journal of the ACM, vol.27, issue.4, pp.758-771, 1980. ,
DOI : 10.1145/322217.322228
A Mathematical Introduction to Logic, 1972. ,
Techniques for Verification of Concurrent Systems with Invariants, 2004. ,
Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants, 12th Intl ,
DOI : 10.1007/3-540-45620-1_26
URL : https://hal.archives-ouvertes.fr/inria-00001088
Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol.3920, pp.167-181, 2006. ,
Shostak Light, Proc. of the 18th International Conference on Automated Deduction, pp.332-346, 2002. ,
DOI : 10.1007/3-540-45620-1_28
Decision procedures for extensions of the theory of arrays, Annals of Mathematics and Artificial Intelligence, vol.27, issue.1, pp.3-4231, 2007. ,
DOI : 10.1007/s10472-007-9078-x
URL : https://hal.archives-ouvertes.fr/inria-00576588
Shostak's congruence closure as completion, Proc. of Rewriting Techniques and Applications, 8th International ConferenceRTA'97), pp.23-37, 1997. ,
DOI : 10.1007/3-540-62950-5_59
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.47.2178
A Rewrite Rule Based Framework for Combining Decision Procedures *, Proc. of the 4th Int. Workshop on Frontiers of Combining Systems, pp.87-102, 2002. ,
DOI : 10.1007/3-540-45988-X_8
On superpositionbased satisfiability procedures and their combination, Proc. of Second International Colloquium on Theoretical Aspects of Computing, pp.594-608, 2005. ,
URL : https://hal.archives-ouvertes.fr/inria-00000586
Automatic Combinability of Rewriting-Based Satisfiability Procedures, Proc. of the 13th Int. Conference on Logic for Programming, pp.542-556, 2006. ,
DOI : 10.1007/11916277_37
URL : https://hal.archives-ouvertes.fr/inria-00117261
Combining decision procedures In Formal Methods at the Cross Roads: From Panacea to Foundational Support, LNCS, vol.2757, pp.381-422, 2003. ,
Normalized Rewriting: an Alternative to Rewriting modulo a Set of Equations, Journal of Symbolic Computation, vol.21, issue.3, pp.253-288, 1996. ,
DOI : 10.1006/jsco.1996.0011
Simplification by Cooperating Decision Procedures, ACM Transactions on Programming Languages and Systems, vol.1, issue.2, pp.245-257, 1979. ,
DOI : 10.1145/357073.357079
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.104.2828
Proof-Producing Congruence Closure, Proc. of the 16th International Conference on Rewriting Techniques and ApplicationsRTA'05), pp.453-468, 2005. ,
DOI : 10.1007/978-3-540-32033-3_33
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.76.1716
Paramodulation-Based Theorem Proving, Hand. of Automated Reasoning, pp.371-443, 2001. ,
DOI : 10.1016/B978-044450813-3/50009-6
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.22.6344
Combining matching algorithms: The regular case, Journal of Symbolic Computation, vol.12, issue.6, pp.633-653, 1991. ,
DOI : 10.1016/S0747-7171(08)80145-9
Nelson-Oppen, Shostak and the Extended Canonizer: A Family Picture with a Newborn, Proc. of First International Colloquium on Theoretical Aspects of Computing, pp.372-386, 2004. ,
DOI : 10.1007/978-3-540-31862-0_27
URL : https://hal.archives-ouvertes.fr/inria-00099985
Combining Proof-Producing Decision Procedures, Proc. of the 6th Int. Symposium on Frontiers of Combining Systems, pp.237-251, 2007. ,
DOI : 10.1007/978-3-540-74621-8_16
URL : https://hal.archives-ouvertes.fr/inria-00187425
Deconstructing Shostak, Proceedings 16th Annual IEEE Symposium on Logic in Computer Science, pp.19-28, 2001. ,
DOI : 10.1109/LICS.2001.932479
Combining shostak theories, Proc. of the 13th International Conference on Rewriting Techniques and Applications, pp.1-18, 2002. ,
Lazy Satisfiability Modulo Theories, Journal on Satisfiability , Boolean Modeling and Computation (JSAT), vol.3, pp.141-224, 2007. ,
Deciding Combinations of Theories, Journal of the ACM, vol.31, issue.1, pp.1-12, 1984. ,
DOI : 10.1145/2422.322411
The Algebra of Equality Proofs, Proc. of the 16th International Conference on Rewriting Techniques and Applications (RTA), pp.469-483, 2005. ,
DOI : 10.1007/978-3-540-32033-3_34
Efficiency of a Good But Not Linear Set Union Algorithm, Journal of the ACM, vol.22, issue.2, pp.215-225, 1975. ,
DOI : 10.1145/321879.321884
Unions of non-disjoint theories and combinations of satisfiability procedures, Theoretical Computer Science, vol.290, issue.1, pp.291-353, 2003. ,
DOI : 10.1016/S0304-3975(01)00332-2
URL : https://hal.archives-ouvertes.fr/inria-00099668
Technopôle de Nancy-Brabois -Campus scientifique 615, rue du Jardin Botanique -BP 101 -54602 Villers-lès ,