Abstract
The rewriting approach to \(\mathcal{T}\)-satisfiability is based on establishing termination of a rewrite-based inference system for first-order logic on the \(\mathcal{T}\)-satisfiability problem. Extending previous such results, including the quantifier-free theory of equality and the theory of arrays with or without extensionality, we prove termination for the theories of records with or without extensionality, integer offsets and integer offsets modulo. A general theorem for termination on combinations of theories, that covers any combination of the theories above, is given next. For empirical evaluation, the rewrite-based theorem prover E is compared with the validity checkers CVC and CVC Lite, on both synthetic and real-world benchmarks, including both valid and invalid instances. Parametric synthetic benchmarks test scalability, while real-world benchmarks test ability to handle huge sets of literals. Contrary to the folklore that a general-purpose prover cannot compete with specialized reasoners, the experiments are overall favorable to the theorem prover, showing that the rewriting approach is both elegant and practical.
Research supported in part by MIUR grant no. 2003-097383.
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
Arkoudas, K., Zee, K., Kuncak, V., Rinard, M.: Verifying a File System Implementation. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004, vol. 3308, pp. 373–390. Springer, Heidelberg (2004)
Armando, A., Bonacina, M.P., Ranise, S., Rusinowitch, M., Sehgal, A.K.: High-Performance Deduction for Verification: a Case Study in the Theory of Arrays. In: Notes of the 2nd VERIFY Workshop, 3rd FLoC, number 07/2002 in Technical Reports, pp. 103–112. DIKU, U. Copenhagen (2002)
Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: Big Proof Engines as Little Proof Engines: New Results on Rewrite-Based Satisfiability Procedures. In: Notes of the 3rd PDPAR Workshop, CAV-17, Technical Reports. U. Edinburgh (2005)
Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: On a Rewriting Approach to Satisfiability Procedures: Theories of Data Structures, Combination Framework and Experimental Appraisal. Technical Report 36/2005, Dip. di Informatica, U. Verona (May 2005), http://www.sci.univr.it/~bonacina/verify.html
Armando, A., Ranise, S., Rusinowitch, M.: A Rewriting Approach to Satisfiability Procedures. Information and Computation 183(2), 140–164 (2003)
Barrett, C.W., Berezin, S.: CVC Lite: A New Implementation of the Cooperating Validity Checker. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 515–518. Springer, Heidelberg (2004)
Barrett, C.W., Dill, D.L., Stump, A.: A Generalization of Shostak’s Method for Combining Decision Procedures. In: Armando, A. (ed.) FroCos 2002. LNCS, vol. 2309, p. 132. Springer, Heidelberg (2002)
Bryant, R.E., Lahiri, S.K., Seshia, S.A.: Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002, vol. 2404, p. 78. Springer, Heidelberg (2002)
de Moura, L., Owre, S., Rueß, H., Rushby, J., Shankar, N.: The ICS Decision Procedures for Embedded Deduction. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS, vol. 3097, pp. 218–222. Springer, Heidelberg (2004)
Déharbe, D., Ranise, S.: Light-Weight Theorem Proving for Debugging and Verifying Units of Code. In: Proc. SEFM 2003. IEEE, Los Alamitos (2003)
Detlefs, D.L., Nelson, G., Saxe, J.B.: Simplify: a Theorem Prover for Program Checking. Technical Report 148, HP Labs (2003)
Ganzinger, H.: Shostak Light. In: Voronkov, A. (ed.) CADE 2002. LNCS, vol. 2392, pp. 332–347. Springer, Heidelberg (2002)
Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): Fast Decision Procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 175–188. Springer, Heidelberg (2004)
Nelson, G., Oppen, D.C.: Simplification by Cooperating Decision Procedures. ACM TOPLAS 1(2), 245–257 (1979)
Nieuwenhuis, R., Rubio, A.: Paramodulation-Based Theorem Proving. In: Handbook of Automated Reasoning, vol. 1. Elsevier Science, Amsterdam (2001)
Rueß, H., Shankar, N.: Deconstructing Shostak. In: Proc. LICS-16. IEEE, Los Alamitos (2001)
Schulz, S.: E – A Brainiac Theorem Prover. J. of AI Comm. 15(2–3), 111–126 (2002)
Schulz, S., Bonacina, M.P.: On Handling Distinct Objects in the Superposition Calculus. In: Notes of the 5th Int. Workshop on Implementation of Logics, LPAR-11, March 2005, pp. 66–77 (2005)
Shankar, N.: Little Engines of Proof, Invited talk, 3rd FLoC, Copenhagen (2002), http://www.csl.sri.com/users/shankar/LEP.html
Shostak, R.E.: Deciding Combinations of Theories. J. ACM 31(1), 1–12 (1984)
Stump, A., Barrett, C.W., Dill, D.L.: CVC: A cooperating validity checker. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 500. Springer, Heidelberg (2002)
Stump, A., Barrett, C.W., Dill, D.L., Levitt, J.: A Decision Procedure for an Extensional Theory of Arrays. In: Proc. LICS-16. IEEE, Los Alamitos (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Armando, A., Bonacina, M.P., Ranise, S., Schulz, S. (2005). On a Rewriting Approach to Satisfiability Procedures: Extension, Combination of Theories and an Experimental Appraisal. In: Gramlich, B. (eds) Frontiers of Combining Systems. FroCoS 2005. Lecture Notes in Computer Science(), vol 3717. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11559306_4
Download citation
DOI: https://doi.org/10.1007/11559306_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-29051-3
Online ISBN: 978-3-540-31730-2
eBook Packages: Computer ScienceComputer Science (R0)