Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Reasoning About Concurrency in High-Assurance, High-Performance Software Systems Read chapter Read first chapter

2017 | OriginalPaper | Chapter

On the Combination of the Bernays–Schönfinkel–Ramsey Fragment with Simple Linear Integer Arithmetic

Authors : Matthias Horbach, Marco Voigt, Christoph Weidenbach

Published in: Automated Deduction – CADE 26

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

In general, first-order predicate logic extended with linear integer arithmetic is undecidable. We show that the Bernays-Schönfinkel-Ramsey fragment (\(\exists ^* \forall ^*\)-sentences) extended with a restricted form of linear integer arithmetic is decidable via finite ground instantiation. The identified ground instances can be employed to restrict the search space of existing automated reasoning procedures considerably, e.g., when reasoning about quantified properties of array data structures formalized in Bradley, Manna, and Sipma’s array property fragment. Typically, decision procedures for the array property fragment are based on an exhaustive instantiation of universally quantified array indices with all the ground index terms that occur in the formula at hand. Our results reveal that one can get along with significantly fewer instances.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter Notions of Knowledge in Combinations of Theories Sharing Constructors
next chapter Satisfiability Modulo Transcendental Functions via Incremental Linearization
Footnotes
1
For any free-sort variable v that occurs in a clause \((\varLambda \,\Vert \, \varGamma \rightarrow \varDelta ) \in N\) exclusively in equations, we pretend that \(\varDelta \) contains an atom \(\text {False}_v(v)\), for a fresh predicate symbol \(\text {False}_v : \mathcal {S}\). This is merely a technical assumption. Without it, we would have to treat such variables v as a separate case in all definitions. The atom \(\text {False}_v(v)\) is not added “physically” to any clause.
 
Literature
1.
2.
Alagi, G., Weidenbach, C.: NRCL – A model building approach to the Bernays-Schönfinkel fragment. In: Lutz, C., Ranise, S. (eds.) FroCoS 2015. LNCS, vol. 9322, pp. 69–84. Springer, Cham (2015). doi:10.​1007/​978-3-319-24246-0_​5 CrossRef
3.
Althaus, E., Kruglov, E., Weidenbach, C.: Superposition modulo linear arithmetic SUP(LA). In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS (LNAI), vol. 5749, pp. 84–99. Springer, Heidelberg (2009). doi:10.​1007/​978-3-642-04222-5_​5 CrossRef
4.
Bachmair, L., Ganzinger, H., Waldmann, U.: Refutational theorem proving for hierarchic first-order theories. Appl. Algebra Eng. Commun. Comput. 5, 193–212 (1994)MathSciNetCrossRefMATH
5.
6.
Bradley, A.R.: Safety Analysis of Systems. PhD thesis (2007)
7.
Bradley, A.R., Manna, Z.: The Calculus of Computation – Decision Procedures with Applications to Verification. Springer, Heidelberg (2007)
8.
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 CrossRef
9.
Claessen, K., Lillieström, A., Smallbone, N.: Sort it out with monotonicity. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 207–221. Springer, Heidelberg (2011). doi:10.​1007/​978-3-642-22438-6_​17 CrossRef
10.
Downey, P.J.: Undecidability of Presburger Arithmetic with a Single Monadic Predicate Letter. Technical report, Center for Research in Computer Technology. Harvard University (1972)
11.
12.
Ge, Y., 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 CrossRef
13.
14.
Horbach, M., Voigt, M., Weidenbach, C.: On the combination of the Bernays-Schönfinkel-Ramsey fragment with simple linear integer arithmetic. ArXiv preprint, arXiv:​ 1705.​08792 [cs.LO] (2017)
15.
Korovin, K.: Inst–Gen – A modular approach to instantiation-based automated reasoning. In: Voronkov, A., Weidenbach, C. (eds.) Programming Logics. LNCS, vol. 7797, pp. 239–270. Springer, Heidelberg (2013). doi:10.​1007/​978-3-642-37651-1_​10 CrossRef
16.
17.
Kroening, D., Strichman, O.: Decision Procedures. Texts in Theoretical Computer Science. An EATCS Series, 2nd edn. Springer, Heidelberg (2016)
18.
Kruglov, E., Weidenbach, C.: Superposition decides the first-order logic fragment over ground theories. Math. Comput. Sci. 6(4), 427–456 (2012)MathSciNetCrossRefMATH
19.
20.
21.
Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM 53, 937–977 (2006)MathSciNetCrossRefMATH
22.
Piskac, R., de Moura, L.M., Bjørner, N.: Deciding effectively propositional logic using DPLL and substitution sets. J. Autom. Reasoning 44(4), 401–424 (2010)
23.
24.
Voigt, M., Weidenbach, C.: Bernays-Schönfinkel-Ramsey with simple bounds is NEXPTIME-complete. ArXiv preprint, arXiv:​1501.​07209 [cs.LO] (2015)
Metadata
Title
On the Combination of the Bernays–Schönfinkel–Ramsey Fragment with Simple Linear Integer Arithmetic
Authors
Matthias Horbach
Marco Voigt
Christoph Weidenbach
Copyright Year
2017
Book
Automated Deduction – CADE 26

Print ISBN: 978-3-319-63045-8

Electronic ISBN: 978-3-319-63046-5

Copyright Year: 2017

DOI
https://doi.org/10.1007/978-3-319-63046-5_6

Premium Partner

    Image Credits