Abstract
Constraint solvers are key modules in many systems with reasoning capabilities (e.g., automated theorem provers). To incorporate constraint solvers in such systems, the capability of producing conflict sets or explanations of their results is crucial. For expressiveness, constraints are usually built out in unions of theories and constraint solvers in such unions are obtained by modularly combining solvers for the component theories. In this paper, we consider the problem of modularly constructing conflict sets for a combined theory by re-using available proof-producing procedures for the component theories. The key idea of our solution to this problem is the concept of explanation graph, which is a labelled, acyclic and undirected graph capable of recording the entailment of some equalities. Explanation graphs allow us to record explanations computed by a proof-producing procedure and to refine the Nelson-Oppen combination method to modularly build conflict sets for disjoint unions of theories. We also study how the computed conflict sets relate to an appropriate notion of minimality.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Boudet, A.: Combining unification algorithms. Journal of Symbolic Computation 16(6), 597–626 (1993)
Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., van Rossum, P., Ranise, S., Sebastiani, R.: Efficient Theory Combination via Boolean Search. J. of Information and Computation 10(204), 1411–1596 (2006)
Burg, J., Lang, S.-D., Hughes, C.E.: Intelligent Backtracking in CLP(R). Ann. Math. Artif. Intell. 17(3-4), 189–211 (1996)
de Moura, L., Rueß, H., Shankar, N.: Justifying Equality. In: Proc. of the Workshop on Pragmatics of Decision Procedures for Automated Reasoning (PDPAR 2004), Also in ENTCS, vol. 125(3) (2004)
Downey, P.J., Sethi, R., Tarjan, R.E.: Variations on the common subexpression problem. J. ACM 27(4), 758–771 (1980)
Enderton, H.B.: A Mathematical Introduction to Logic. Academic Press, San Diego (1972)
Fontaine, P.: Techniques for Verification of Concurrent Systems with Invariants. PhD thesis, Université de Liège (2004)
Fontaine, P., Marion, J.-Y., Merz, S., Prensa Nieto, L., Tiu, A.F.: Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol. 3920, pp. 167–181. Springer, Heidelberg (2006)
Kirchner, H., Ranise, S., Ringeissen, C., Tran, D.-K.: Automatic Combinability of Rewriting-Based Satisfiability Procedures. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 542–556. Springer, Heidelberg (2006)
Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. on Programming Languages and Systems 1(2), 245–257 (1979)
Nieuwenhuis, R., Oliveras, A.: Proof-Producing Congruence Closure. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 453–468. Springer, Heidelberg (2005)
Nipkow, T.: Combining matching algorithms: The regular case. Journal of Symbolic Computation 12, 633–653 (1991)
Ranise, S., Ringeissen, C., Tran, D.-K.: Nelson-Oppen, Shostak and the Extended Canonizer: A Family Picture with a Newborn. In: Liu, Z., Araki, K. (eds.) ICTAC 2004. LNCS, vol. 3407, Springer, Heidelberg (2005)
Ranise, S., Tinelli, C.: Satisfiability Modulo Theories. IEEE Magazine on Intelligent Systems 21(6), 71–81 (2006)
Schrijver, A.: Theory of linear and integer programming. John Wiley & Sons, Chichester (1986)
Schulz, S.: E – a brainiac theorem prover. AI Communications (2002)
Stump, A., Tang, L.-Y.: The Algebra of Equality Proofs. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 469–483. Springer, Heidelberg (2005)
Tarjan, R.E.: Efficiency of a good but not linear set union algorithm. J. of the ACM 22(2), 215–225 (1975)
Tran, D.-K.: Conception de Procédures de Décision par Combinaison et Saturation. PhD thesis, Université Henri Poincaré, Nancy, France, Ch. 8 (in english) (2007)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ranise, S., Ringeissen, C., Tran, DK. (2007). Combining Proof-Producing Decision Procedures. In: Konev, B., Wolter, F. (eds) Frontiers of Combining Systems. FroCoS 2007. Lecture Notes in Computer Science(), vol 4720. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74621-8_16
Download citation
DOI: https://doi.org/10.1007/978-3-540-74621-8_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-74620-1
Online ISBN: 978-3-540-74621-8
eBook Packages: Computer ScienceComputer Science (R0)