Abstract
First-order linear real arithmetic enriched with uninterpreted predicate symbols yields an interesting modeling language. However, satisfiability of such formulas is undecidable, even if we restrict the uninterpreted predicate symbols to arity one. In order to find decidable fragments of this language, it is necessary to restrict the expressiveness of the arithmetic part. One possible path is to confine arithmetic expressions to difference constraints of the form \(x - y \mathrel {\triangleleft }c\), where \(\mathrel {\triangleleft }\) ranges over the standard relations \(<, \le , =, \ne , \ge ,>\) and x, y are universally quantified. However, it is known that combining difference constraints with uninterpreted predicate symbols yields an undecidable satisfiability problem again. In this paper, it is shown that satisfiability becomes decidable if we in addition bound the ranges of universally quantified variables. As bounded intervals over the reals still comprise infinitely many values, a trivial instantiation procedure is not sufficient to solve the problem.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Alur, R., Dill, D.L.: A theory of timed automata. Theoret. Comput. Sci. 126(2), 183–235 (1994)
Bachmair, L., Ganzinger, H., Waldmann, U.: Refutational theorem proving for hierarchic first-order theories. Appl. Algebra Eng. Commun. Comput. 5, 193–212 (1994)
Baumgartner, P., Waldmann, U.: Hierarchic superposition with weak abstraction. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 39–57. Springer, Heidelberg (2013). doi:10.1007/978-3-642-38574-2_3
Bradley, A.R., Manna, Z., Sipma, H.B.: What’s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 427–442. Springer, Heidelberg (2005). doi:10.1007/11609773_28
Downey, P.J.: Undecidability of Presburger arithmetic with a single monadic predicate letter. Technical report, Center for Research in Computer Technology, Harvard University (1972)
Fietzke, A., Weidenbach, C.: Superposition as a decision procedure for timed automata. Math. Comput. Sci. 6(4), 409–425 (2012)
Ge, Y., de Moura, L.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 306–320. Springer, Heidelberg (2009). doi:10.1007/978-3-642-02658-4_25
Graham, R.L., Rothschild, B.L., Spencer, J.H.: Ramsey Theory, 2nd edn. A Wiley-Interscience publication, New York (1990)
Horbach, M., Voigt, M., Weidenbach, C.: On the combination of the Bernays-Schönfinkel-Ramsey fragment with simple linear integer arithmetic. In: Automated Deduction (CADE-26) (to appear)
Horbach, M., Voigt, M., Weidenbach, C.: The universal fragment of Presburger arithmetic with unary uninterpreted predicates is undecidable. ArXiv preprint, arXiv:1703.01212 [cs.LO] (2017)
Kroening, D., Strichman, O.: Decision Procedures. Texts in Theoretical Computer Science. An EATCS Series, 2nd edn. Springer, Heidelberg (2016). doi:10.1007/978-3-662-50497-0
Kruglov, E., Weidenbach, C.: Superposition decides the first-order logic fragment over ground theories. Math. Comput. Sci. 6(4), 427–456 (2012)
Niebert, P., Mahfoudh, M., Asarin, E., Bozga, M., Maler, O., Jain, N.: Verification of timed automata via satisfiability checking. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol. 2469, pp. 225–243. Springer, Heidelberg (2002). doi:10.1007/3-540-45739-9_15
Pratt, V.R.: Two Easy Theories Whose Combination is Hard. Technical report, Massachusetts Institute of Technology (1977)
Putnam, H.: Decidability and essential undecidability. J. Symbolic Logic 22(1), 39–54 (1957)
Voigt, M.: The Bernays-Schönfinkel-Ramsey Fragment with Bounded Difference Constraints over the Reals is Decidable. ArXiv preprint, arXiv:1706.08504 [cs.LO] (2017)
Voigt, M., Weidenbach, C.: Bernays-Schönfinkel-Ramsey with Simple Bounds is NEXPTIME-complete. ArXiv preprint, arXiv:1501.07209 [cs.LO] (2015)
Acknowledgement
The present author is indebted to the anonymous reviewers for their constructive criticism and valuable suggestions.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Voigt, M. (2017). The Bernays–Schönfinkel–Ramsey Fragment with Bounded Difference Constraints over the Reals Is Decidable. In: Dixon, C., Finger, M. (eds) Frontiers of Combining Systems. FroCoS 2017. Lecture Notes in Computer Science(), vol 10483. Springer, Cham. https://doi.org/10.1007/978-3-319-66167-4_14
Download citation
DOI: https://doi.org/10.1007/978-3-319-66167-4_14
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-66166-7
Online ISBN: 978-3-319-66167-4
eBook Packages: Computer ScienceComputer Science (R0)