Abstract
The hierarchical superposition based theorem proving calculus of Bachmair, Ganzinger, and Waldmann enables the hierarchic combination of a theory with full first-order logic. If a clause set of the combination enjoys a sufficient completeness criterion, the calculus is even complete. We instantiate the calculus for the theory of linear arithmetic. In particular, we develop new effective versions for the standard superposition redundancy criteria taking the linear arithmetic theory into account. The resulting calculus is implemented in SPASS(LA) and extends the state of the art in proving properties of first-order formulas over linear arithmetic.
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
Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: New results on rewrite-based satisfiability procedures. ACM Trans. Comput. Log. 10(1), 129–179 (2009)
Althaus, E., Dumitriu, D.: Fast and accurate bounds on linear programs. In: Vahrenhold, J. (ed.) SEA 2009. LNCS, vol. 5526, pp. 40–50. Springer, Heidelberg (2009)
Bachmair, L., Ganzinger, H., Waldmann, U.: Refutational theorem proving for hierarchic first-order theories. Applicable Algebra in Engineering, Communication and Computing, AAECC 5(3/4), 193–212 (1994)
Dimova, D.: On the translation of timed automata into first-order logic. In: Fietzke, A., Weidenbach, C. (supervisors) (2009)
de Moura, L.M., Bjørner, N.: Engineering dpll(t) + saturation. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 475–490. Springer, Heidelberg (2008)
Faure, G., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E.: Sat modulo the theory of linear arithmetic: Exact, inexact and commercial solvers. In: Kleine Büning, H., Zhao, X. (eds.) SAT 2008. LNCS, vol. 4996, pp. 77–90. Springer, Heidelberg (2008)
Hustadt, U., Schmidt, R.A., Georgieva, L.: A survey of decidable first-order fragments and description logics. Journal of Relational Methods in Computer Science 1, 251–276 (2004)
Korovin, K., Voronkov, A.: Integrating linear arithmetic into superposition calculus. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol. 4646, pp. 223–237. Springer, Heidelberg (2007)
Nonnengart, A.: Hybrid systems verification by location elimination. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 352–365. Springer, Heidelberg (2000)
Schrijver, A.: Theory of linear and integer programming. John Wiley & Sons, Inc., Chichester (1989)
Waldmann, U.: Superposition and chaining for totally ordered divisible abelian groups. In: Goré, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol. 2083, pp. 226–241. Springer, Heidelberg (2001)
Weidenbach, C.: Combining superposition, sorts and splitting. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 27, vol. 2, pp. 1965–2012. Elsevier, Amsterdam (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Althaus, E., Kruglov, E., Weidenbach, C. (2009). Superposition Modulo Linear Arithmetic SUP(LA). In: Ghilardi, S., Sebastiani, R. (eds) Frontiers of Combining Systems. FroCoS 2009. Lecture Notes in Computer Science(), vol 5749. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04222-5_5
Download citation
DOI: https://doi.org/10.1007/978-3-642-04222-5_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-04221-8
Online ISBN: 978-3-642-04222-5
eBook Packages: Computer ScienceComputer Science (R0)