On Superposition-Based Satisfiability Procedures and Their Combination

  • Hélène Kirchner
  • Silvio Ranise
  • Christophe Ringeissen
  • Duc Khanh Tran
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3722)


We study how to efficiently combine satisfiability procedures built by using a superposition calculus with satisfiability procedures for theories, for which the superposition calculus may not apply (e.g., for various decidable fragments of Arithmetic). Our starting point is the Nelson-Oppen combination method, where satisfiability procedures cooperate by exchanging entailed (disjunction of) equalities between variables. We show that the superposition calculus deduces sufficiently many such equalities for convex theories (e.g., the theory of equality and the theory of lists) and disjunction of equalities for non-convex theories (e.g., the theory of arrays) to guarantee the completeness of the combination method. Experimental results on proof obligations extracted from the certification of auto-generated aerospace software confirm the efficiency of the approach. Finally, we show how to make satisfiability procedures built by superposition both incremental and resettable by using a hierarchic variant of the Nelson-Oppen method.


Combination Method Elementary Equality Proof Obligation Unit Clause Empty Clause 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: On a rewriting approach to satisfiability procedures: extension, combination of theories and an experimental appraisal. In: Gramlich, B. (ed.) FroCos 2005. LNCS (LNAI), vol. 3717, pp. 65–80. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  2. 2.
    Armando, A., Ranise, S., Rusinowitch, M.: A Rewriting Approach to Satisfiability Procedures. Info. and Comp. 183(2), 140–164 (2003)zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    Déharbe, D., Ranise, S.: Light-Weight Theorem Proving for Debugging and Verifying Units of Code. In: Proc. of the Int. Conf. on Software Engineering and Formal Methods (SEFM 2003). IEEE Comp. Soc. Press, Los Alamitos (2003)Google Scholar
  4. 4.
    Denney, E., Fischer, B., Schumann, J.: Using automated theorem provers to certify auto-generated aerospace software. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol. 3097, pp. 198–212. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  5. 5.
    Dershowitz, N., Jouannaud, J.-P.: Handbook of Theoretical Computer Science, ch. 6. Rewrite Systems, vol. B, pp. 244–320. Elsevier Science Publishers B. V. North-Holland (1990)Google Scholar
  6. 6.
    Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: A Theorem Prover for Program Checking. Technical Report HPL-2003-148, HP Laboratories (2003)Google Scholar
  7. 7.
    Ganzinger, H., Hillenbrand, T., Waldmann, U.: Superposition modulo a Shostak theory. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 182–196. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  8. 8.
    Kapur, D., Nie, X.: Reasoning about Numbers in Tecton. In: Proc. 8th Inl. Symp. Methodologies for Intelligent Systems, pp. 57–70 (1994)Google Scholar
  9. 9.
    Kirchner, H., Ranise, S., Ringeissen, C., Tran, D.K.: On Superposition-Based Satisfiability Procedures and their Combination (Full Version), Available at
  10. 10.
    Nelson, G.: Techniques for program verification. Technical Report CS-81-10, Xerox Palo Research Center California USA (1981)Google Scholar
  11. 11.
    Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. on Programming Languages and Systems 1(2), 245–257 (1979)zbMATHCrossRefGoogle Scholar
  12. 12.
    Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson, A., Voronkov, A. (eds.) Hand. of Automated Reasoning (2001)Google Scholar
  13. 13.
    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, pp. 372–386. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  14. 14.
    Ranise, S., Ringeissen, C., Zarba, C.G.: Combining data structures with nonstably infinite theories using many-sorted logic. In: Gramlich, B. (ed.) FroCos 2005. LNCS (LNAI), vol. 3717, pp. 48–64. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  15. 15.
    Schulz, S.: E – A Brainiac Theorem Prover. Journal of AI Communications 15(2/3), 111–126 (2002)zbMATHGoogle Scholar
  16. 16.
    Shostak, R.E.: Deciding combinations of theories. J. of the ACM 31, 1–12 (1984)zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Hélène Kirchner
    • 1
  • Silvio Ranise
    • 1
  • Christophe Ringeissen
    • 1
  • Duc Khanh Tran
    • 1
  1. 1.LORIA & INRIA-Lorraine 

Personalised recommendations