Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates. (English) Zbl 1543.03046
Summary: First-order linear rational arithmetic enriched with uninterpreted predicates yields an interesting and very expressive modeling language. However, already the presence of a single uninterpreted predicate symbol of arity one or greater renders the associated satisfiability problem undecidable. We identify two decidable fragments, both based on the Bernays-Schönfinkel-Ramsey prefix class. Due to the inherent infiniteness of the underlying domain, a finite model property in the usual sense cannot be established. Nevertheless, we show that satisfiable sentences always have a model that can be described by finite means. To this end, we restrict the syntax of arithmetic atoms. In the first fragment that is presented, arithmetic operations are only allowed over terms without universally quantified variables. In the second fragment, arithmetic atoms are essentially confined to difference constraints over universally quantified variables with bounded range. We will call such atoms bounded difference constraints. As bounded intervals over the rationals still comprise infinitely many values, a trivial instantiation procedure is not sufficient to solve the satisfiability problem. After a slight shift of perspective, the positive decidability result for the first fragment can be restated in the framework of combinations of theories over non-disjoint vocabularies. More precisely, we combine first-order theories that share a dense total order without endpoints.
MSC:
| 03B25 | Decidability of theories and sets of sentences |
| 03B62 | Combined logics |
| 03F30 | First-order arithmetic and fragments |
Keywords:
Bernays-Schönfinkel-Ramsey fragment; first-order arithmetic; linear rational arithmetic; difference constraints; combinations of theoriesReferences:
| [1] | Abadi, A.; Rabinovich, A.; Sagiv, M., Decidable fragments of many-sorted logic, J. Symb. Comput., 45, 2, 153-172 (2010) · Zbl 1183.03007 |
| [2] | Abadi, A., Rabinovich, A.M., Sagiv, M.: Decidable fragments of many-sorted logic. In: Logic for Programming, Artificial Intelligence, and Reasoning (LPAR’07), pp. 17-31 (2007) · Zbl 1137.03302 |
| [3] | Alagi, G., Weidenbach, C.: NRCL—a model building approach to the Bernays-Schönfinkel fragment. In: Frontiers of Combining Systems (FroCoS’15), LNCS 9322, pp. 69-84. Springer (2015) · Zbl 1471.03013 |
| [4] | Althaus, E., Kruglov, E., Weidenbach, C.: Superposition modulo linear arithmetic SUP(LA). In: Frontiers of Combining Systems (FroCoS’09), pp. 84-99 (2009) · Zbl 1193.03024 |
| [5] | Alur, R., Dill, D.L.: Automata for modeling real-time systems. In: Automata, Languages and Programming (ICALP’90), pp. 322-335 (1990) · Zbl 0765.68150 |
| [6] | Alur, R.; Dill, DL, A theory of timed automata, Theor. Comput. Sci., 126, 2, 183-235 (1994) · Zbl 0803.68071 |
| [7] | Areces, C., Fontaine, P.: Combining theories: the Ackerman and guarded fragments. In: Frontiers of Combining Systems (FroCoS’11), pp. 40-54 (2011) · Zbl 1348.03027 |
| [8] | Armando, A.; Bonacina, MP; Ranise, S.; Schulz, S., New results on rewrite-based satisfiability procedures, ACM Trans. Comput. Log., 10, 1, 129-179 (2009) · Zbl 1367.68243 |
| [9] | Armando, A., Castellini, C., Giunchiglia, E., Maratea, M.: A SAT-based decision procedure for the Boolean combination of difference constraints. In: Theory and Applications of Satisfiability Testing (SAT’04), Revised Selected Papers (2004) · Zbl 1122.68583 |
| [10] | Bachmair, L., Ganzinger, H., Waldmann, U.: Theorem proving for hierarchic first-order theories. In: Algebraic and Logic Programming (ALP’92), pp. 420-434 (1992) · Zbl 0925.03074 |
| [11] | Bachmair, L.; Ganzinger, H.; Waldmann, U., Refutational theorem proving for hierarchic first-order theories, Appl. Algebra Eng. Commun. Comput., 5, 193-212 (1994) · Zbl 0797.03008 |
| [12] | Baier, C.; Katoen, JP, Principles of Model Checking (2008), Cambridge: MIT Press, Cambridge · Zbl 1179.68076 |
| [13] | Barbosa, H.: New techniques for instantiation and proof production in SMT solving (nouvelles techniques pour l’instanciation et la production des preuves dans SMT). Ph.D. thesis, University of Lorraine, Nancy, France (2017) |
| [14] | Barrett, C.; Tinelli, C.; Clarke, EM; Henzinger, TA; Veith, H.; Bloem, R., Satisfiability modulo theories, Handbook of Model Checking, 305-343 (2018), Berlin: Springer, Berlin · Zbl 1392.68379 |
| [15] | Baumgartner, P.; Fuchs, A.; de Nivelle, H.; Tinelli, C., Computing finite models by reduction to function-free clause logic, J. Appl. Log., 7, 1, 58-74 (2009) · Zbl 1171.68040 |
| [16] | Baumgartner, P., Waldmann, U.: Hierarchic superposition: completeness without compactness. In: Košta, M., Sturm, T. (eds.) Fifth International Conference on Mathematical Aspects of Computer and Information Sciences (MACIS’13), pp. 8-12 (2013) |
| [17] | Baumgartner, P., Waldmann, U.: Hierarchic superposition with weak abstraction. In: Automated Deduction (CADE-24), LNCS 7898, pp. 39-57. Springer (2013) · Zbl 1381.03017 |
| [18] | Blumensath, A., Grädel, E.: Automatic structures. In: Logic in Computer Science (LICS 2000), pp. 51-62 (2000) |
| [19] | Blumensath, A.; Grädel, E., Finite presentations of infinite structures: automata and interpretations, Theory Comput. Syst., 37, 6, 641-674 (2004) · Zbl 1061.03038 |
| [20] | Bonacina, M.P., Fontaine, P., Ringeissen, C., Tinelli, C.: Theory combination: beyond equality sharing. In: Description Logic, Theory Combination, and All That—Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday, pp. 57-89 (2019) · Zbl 1443.68116 |
| [21] | Börger, E.; Grädel, E.; Gurevich, Y., The Classical Decision Problem. Perspectives in Mathematical Logic (1997), Berlin: Springer, Berlin · Zbl 0865.03004 |
| [22] | Bouyer, P.; Fahrenberg, U.; Larsen, KG; Markey, N.; Ouaknine, J.; Worrell, J.; Clarke, EM; Henzinger, TA; Veith, H.; Bloem, R., Model checking real-time systems, Handbook of Model Checking, 1001-1046 (2018), Berlin: Springer, Berlin · Zbl 1392.68235 |
| [23] | Bradley, A.R.: Safety analysis of systems. Ph.D. thesis, Department of Computer Science of Stanford University (2007) |
| [24] | Bradley, AR; Manna, Z., The Calculus of Computation—Decision Procedures with Applications to Verification (2007), Berlin: Springer, Berlin · Zbl 1126.03001 |
| [25] | Bradley, A.R., Manna, Z., Sipma, H.B.: What’s decidable about arrays? In: Verification, Model Checking, and Abstract Interpretation (VMCAI’06), pp. 427-442 (2006) · Zbl 1176.68116 |
| [26] | Bresolin, D.; Della Monica, D.; Montanari, A.; Sciavicco, G., The light side of interval temporal logic: the Bernays-Schönfinkel fragment of CDT, Ann. Math. Artif. Intell., 71, 1-3, 11-39 (2014) · Zbl 1325.03015 |
| [27] | 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: Computer Aided Verification (CAV’02), pp. 78-92 (2002) · Zbl 1010.68522 |
| [28] | Büchi, JR, Weak second-order arithmetic and finite automata, Zeitschrift für mathematische Logik und Grundlagen der Mathematik, 6, 66-92 (1960) · Zbl 0103.24705 |
| [29] | Büchi, J.R.: On a decision method in restricted second order arithmetic. In: Nagel, E., Suppes, P., Tarski, A. (eds.) Proceedings of the 1960 International Congress on Logic, Methodology and Philosophy of Science, pp. 1-11. Stanford University Press (1962) · Zbl 0147.25103 |
| [30] | Charatonik, W., Witkowski, P.: On the complexity of the Bernays-Schönfinkel class with datalog. In: Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-17), LNCS 6397, pp. 187-201. Springer (2010) · Zbl 1307.03019 |
| [31] | Chocron, P., Fontaine, P., Ringeissen, C.: A gentle non-disjoint combination of satisfiability procedures. In: Automated Reasoning (IJCAR’14), pp. 122-136 (2014) · Zbl 1423.68441 |
| [32] | Chocron, P., Fontaine, P., Ringeissen, C.: A polite non-disjoint combination method: theories with bridging functions revisited. In: Automated Deduction (CADE-25), pp. 419-433 (2015) · Zbl 1465.68303 |
| [33] | Comon, H., Jurski, Y.: Multiple counters automata, safety analysis and Presburger arithmetic. In: Computer Aided Verification (CAV’98), pp. 268-279 (1998) |
| [34] | Comon, H., Jurski, Y.: Timed automata and the theory of real numbers. In: Concurrency Theory (CONCUR’99), pp. 242-257 (1999) · Zbl 0940.68092 |
| [35] | Conchon, S.; Krstic, S., Strategies for combining decision procedures, Theor. Comput. Sci., 354, 2, 187-210 (2006) · Zbl 1088.68161 |
| [36] | Cotton, S., Asarin, E., Maler, O., Niebert, P.: Some progress in satisfiability checking for difference logic. In: Formal Modelling and Analysis of Timed Systems and Formal Techniques in Real-Time and Fault-Tolerant Systems (FORMATS/FTRTFT’04), pp. 263-276 (2004) · Zbl 1109.68513 |
| [37] | Cotton, S., Maler, O.: Fast and flexible difference constraint propagation for DPLL(T). In: Theory and Applications of Satisfiability Testing (SAT’06), pp. 170-183 (2006) · Zbl 1187.68537 |
| [38] | Cox, J.; McAloon, K.; Benhamou, F.; Colmerauer, A., Decision procedures for constraint-based extensions of Datalog, Constraint Logic Programming, Selected Research, 17-32 (1993), Cambridge: The MIT Press, Cambridge |
| [39] | Cox, J.; McAloon, K.; Tretkoff, C., Computational complexity and constraint logic programming languages, Ann. Math. Artif. Intell., 5, 2-4, 163-189 (1992) · Zbl 0866.68013 |
| [40] | Downey, P.J.: Undecidability of Presburger arithmetic with a single monadic predicate letter. Center for Research in Computer Technology, Harvard University, Technical report (1972) |
| [41] | Doyen, L.; Frehse, G.; Pappas, GJ; Platzer, A.; Clarke, EM; Henzinger, TA; Veith, H.; Bloem, R., Verification of hybrid systems, Handbook of Model Checking, 1047-1110 (2018), Berlin: Springer, Berlin · Zbl 1392.68246 |
| [42] | Ebbinghaus, H.; Flum, J.; Thomas, W., Mathematical Logic (1994), Berlin: Springer, Berlin · Zbl 0795.03001 |
| [43] | Eggers, A., Kruglov, E., Kupferschmid, S., Scheibler, K., Teige, T., Weidenbach, C.: Superposition modulo non-linear arithmetic. In: Frontiers of Combining Systems (FroCoS’11), pp. 119-134 (2011) · Zbl 1348.68218 |
| [44] | Emmer, M., Khasidashvili, Z., Korovin, K., Sticksel, C., Voronkov, A.: EPR-based bounded model checking at word level. In: Automated Reasoning (IJCAR’12), pp. 210-224 (2012) · Zbl 1358.68190 |
| [45] | Emmer, M., Khasidashvili, Z., Korovin, K., Voronkov, A.: Encoding industrial hardware verification problems into effectively propositional logic. In: Formal Methods in Computer-Aided Design (FMCAD’10), pp. 137-144 (2010) |
| [46] | Enderton, HB, A Mathematical Introduction to Logic (1972), London: Academic Press, London · Zbl 0298.02002 |
| [47] | Fermüller, CG; Leitsch, A.; Hustadt, U.; Tammet, T.; Robinson, A.; Voronkov, A., Resolution decision procedures, Handbook of Automated Reasoning, 1791-1849 (2001), Amsterdam: Elsevier, Amsterdam · Zbl 0993.68119 |
| [48] | Ferrante, J.; Rackoff, CW, The Computational Complexity of Logical Theories (1979), Berlin: Springer, Berlin · Zbl 0404.03028 |
| [49] | Fietzke, A.: Labelled superposition. Ph.D. thesis, Department of Computer Science, Saarland University (2013) |
| [50] | Fietzke, A.; Weidenbach, C., Superposition as a decision procedure for timed automata, Math. Comput. Sci., 6, 4, 409-425 (2012) · Zbl 1262.68159 |
| [51] | Finkbeiner, B., Müller, C., Seidl, H., Zalinescu, E.: Verifying security policies in multi-agent workflows with loops. In: Computer and Communications Security (CCS’17), pp. 633-645 (2017) |
| [52] | Fontaine, P.: Combinations of theories and the Bernays-Schönfinkel-Ramsey class. In: Verification Workshop in connection with CADE-21 (VERIFY’07) (2007) |
| [53] | Fontaine, P.: Combinations of theories for decidable fragments of first-order logic. In: Frontiers of Combining Systems (FroCoS’09), LNCS 5749, pp. 263-278. Springer (2009) · Zbl 1193.03020 |
| [54] | Frühwirth, T.; Abdennadher, S., Essentials of Constraint Programming (2003), Berlin: Springer, Berlin · Zbl 1064.68026 |
| [55] | Gács, P.; Lovász, L., Khachiyan’s algorithm for linear programming, Math. Program. Study, 14, 61-68 (1981) · Zbl 0463.90066 |
| [56] | Ganzinger, H.: Shostak light. In: Automated Deduction (CADE-18), pp. 332-346 (2002) · Zbl 1072.68572 |
| [57] | Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): fast decision procedures. In: Computer Aided Verification (CAV’04), pp. 175-188 (2004) · Zbl 1103.68616 |
| [58] | Ganzinger, H., Hillenbrand, T., Waldmann, U.: Superposition modulo a shostak theory. In: Automated Deduction (CADE-19), pp. 182-196 (2003) · Zbl 1278.68260 |
| [59] | Ge, Y., de Moura, L.M.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Computer Aided Verification (CAV’09), LNCS 5643, pp. 306-320. Springer (2009) · Zbl 1242.68280 |
| [60] | Ghilardi, S.; Gianola, A., Modularity results for interpolation, amalgamation and superamalgamation, Ann. Pure Appl. Log., 169, 8, 731-754 (2018) · Zbl 1469.03092 |
| [61] | Ghilardi, S.; Nicolini, E.; Zucchelli, D., A comprehensive combination framework, ACM Trans. Comput. Log., 9, 2, 8:1-8:54 (2008) · Zbl 1407.03011 |
| [62] | Graham, R.; Rothschild, B.; Spencer, J., Ramsey Theory. A Wiley-Interscience Publication (1990), Hoboken: Wiley, Hoboken · Zbl 0705.05061 |
| [63] | Habermehl, P., Iosif, R., Vojnar, T.: What else is decidable about integer arrays? In: Foundations of Software Science and Computational Structures (FOSSACS’08), pp. 474-489 (2008) · Zbl 1139.03007 |
| [64] | Halpern, JY, Presburger arithmetic with unary predicates is \(\Pi^1_1\) complete, J. Symb. Log., 56, 2, 637-642 (1991) · Zbl 0738.03017 |
| [65] | Henzinger, TA; Nicollin, X.; Sifakis, J.; Yovine, S., Symbolic model checking for real-time systems, Inf. Comput., 111, 2, 193-244 (1994) · Zbl 0806.68080 |
| [66] | Hillenbrand, T.: Superposition and decision procedures back and forth. Ph.D. thesis, Department of Computer Science, Saarland University (2008) |
| [67] | Hillenbrand, T., Weidenbach, C.: Superposition for bounded domains. In: Automated Reasoning and Mathematics—Essays in Memory of William W. McCune, LNCS 7788, pp. 68-100. Springer (2013) · Zbl 1383.03018 |
| [68] | Hoffart, J.; Suchanek, FM; Berberich, K.; Weikum, G., YAGO2: a spatially and temporally enhanced knowledge base from Wikipedia, Artif. Intell., 194, 28-61 (2013) · Zbl 1270.68303 |
| [69] | 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’17), LNCS 10395, pp. 77-94 (2017). An extended version is available at the arXiv preprint server under the signature arXiv:1705.08792 [cs.LO] · Zbl 1496.03046 |
| [70] | 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) |
| [71] | Ihlemann, C.: Reasoning in combinations of theories. Ph.D. thesis, Department of Computer Science, Saarland University (2010) · Zbl 1291.03018 |
| [72] | Ihlemann, C., Sofronie-Stokkermans, V.: On hierarchical reasoning in combinations of theories. In: Automated Reasoning (IJCAR’10), pp. 30-45 (2010) · Zbl 1291.03018 |
| [73] | Itzhaky, S., Banerjee, A., Immerman, N., Lahav, O., Nanevski, A., Sagiv, M.: Modular reasoning about heap paths via effectively propositional formulas. In: Principles of Programming Languages (POPL’14), pp. 385-396 (2014) · Zbl 1284.68403 |
| [74] | Itzhaky, S., Banerjee, A., Immerman, N., Nanevski, A., Sagiv, M.: Effectively-propositional reasoning about reachability in linked data structures. In: Computer Aided Verification (CAV’13), pp. 756-772 (2013) |
| [75] | Itzhaky, S., Bjørner, N., Reps, T.W., Sagiv, M., Thakur, A.V.: Property-directed shape analysis. In: Computer Aided Verification (CAV’14), pp. 35-51 (2014) |
| [76] | Jacobs, S.: Hierarchic decision procedures for verification. Ph.D. thesis, Department of Computer Science, Saarland University (2009) |
| [77] | Karbyshev, A., Bjørner, N., Itzhaky, S., Rinetzky, N., Shoham, S.: Property-directed inference of universal invariants or proving their absence. In: Computer Aided Verification (CAV’15), pp. 583-602 (2015) · Zbl 1381.68169 |
| [78] | Karmarkar, N., A new polynomial-time algorithm for linear programming, Combinatorica, 4, 4, 373-395 (1984) · Zbl 0557.90065 |
| [79] | Khachiyan, LG, Polynomial algorithms in linear programming, USSR Comput. Math. Math. Phys., 20, 1, 53-72 (1980) · Zbl 0459.90047 |
| [80] | Kieroński, E.; Pratt-Hartmann, I.; Tendera, L., Two-variable logics with counting and semantic constraints, SIGLOG News, 5, 3, 22-43 (2018) |
| [81] | Korovin, K.: Non-cyclic sorts for first-order satisfiability. In: Frontiers of Combining Systems (FroCoS’13), LNCS 8152, pp. 214-228. Springer (2013) · Zbl 1398.68484 |
| [82] | Kroening, D.; Strichman, O., Decision Procedures (2016), Berlin: Springer, Berlin · Zbl 1358.68002 |
| [83] | Kruglov, E.: Superposition modulo theory. Ph.D. thesis, Department of Computer Science, Saarland University (2013) |
| [84] | Kruglov, E.; Weidenbach, C., Superposition decides the first-order logic fragment over ground theories, Math. Comput. Sci., 6, 4, 427-456 (2012) · Zbl 1262.68160 |
| [85] | Kuncak, V., Piskac, R., Suter, P., Wies, T.: Building a calculus of data structures. In: Verification, Model Checking, and Abstract Interpretation (VMCAI’10), pp. 26-44 (2010) · Zbl 1273.68100 |
| [86] | Lamotte-Schubert, M.: Automatic authorization analysis. Ph.D. thesis, Department of Computer Science, Saarland University (2015) |
| [87] | Lamotte-Schubert, M.; Weidenbach, C., BDI: a new decidable clause class, J. Log. Comput., 27, 2, 441-468 (2017) · Zbl 1444.03015 |
| [88] | Lewis, HR, Complexity results for classes of quantificational formulas, J. Comput. Syst. Sci., 21, 3, 317-353 (1980) · Zbl 0471.03034 |
| [89] | Lewis, H.R.: A logic of concrete time intervals (extended abstract). In: Logic in Computer Science (LICS’90), pp. 380-389 (1990) |
| [90] | Loos, R.; Weispfenning, V., Applying linear quantifier elimination, Comput. J., 36, 5, 450-462 (1993) · Zbl 0787.03021 |
| [91] | Mahfoudh, M.: Sur la Vérification de la Satisfaction pour la Logique des Différences. Ph.D. thesis, Université Joseph Fourier - Grenoble 1 (2003) |
| [92] | Mahfoudh, M., Niebert, P., Asarin, E., Maler, O.: A satisfiability checker for difference logic. In: Theory and Applications of Satisfiability Testing (SAT’02), pp. 222-230 (2002) · Zbl 1278.68187 |
| [93] | Manna, Z., Zarba, C.G.: Combining decision procedures. In: Formal Methods at the Crossroads. From Panacea to Foundational Support, 10th Anniversary Colloquium of UNU/IIST, the International Institute for Software Technology of The United Nations University, Lisbon, Portugal, Revised Papers, pp. 381-422 (2002) · Zbl 1274.68078 |
| [94] | Mortimer, M., On languages with two variables, Math. Log. Q., 21, 1, 135-140 (1975) · Zbl 0343.02009 |
| [95] | de Moura, LM; Bjørner, N., Satisfiability modulo theories: introduction and applications, Commun. ACM, 54, 9, 69-77 (2011) |
| [96] | Nelson, G., Combining satisfiability procedures by equality-sharing, Contemp. Math., 29, 201-211 (1984) · Zbl 0564.03011 |
| [97] | Nelson, G.; Oppen, DC, Simplification by cooperating decision procedures, ACM Trans. Program. Lang. Syst., 1, 2, 245-257 (1979) · Zbl 0452.68013 |
| [98] | Niebert, P., Mahfoudh, M., Asarin, E., Bozga, M., Maler, O., Jain, N.: Verification of timed automata via satisfiability checking. In: Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT’02), pp. 225-244 (2002) · Zbl 1278.68187 |
| [99] | Nieuwenhuis, R., Oliveras, A.: DPLL(T) with exhaustive theory propagation and its application to difference logic. In: Computer Aided Verification (CAV’05), pp. 321-334 (2005) · Zbl 1081.68629 |
| [100] | Oppen, DC, Complexity, convexity and combinations of theories, Theor. Comput. Sci., 12, 291-302 (1980) · Zbl 0437.03007 |
| [101] | Otto, M., Two variable first-order logic over ordered domains, J. Symb. Log., 66, 2, 685-702 (2001) · Zbl 0990.03005 |
| [102] | Padon, O., McMillan, K.L., Panda, A., Sagiv, M., Shoham, S.: Ivy: safety verification by interactive generalization. In: Programming Language Design and Implementation (PLDI’16), pp. 614-630 (2016) |
| [103] | Pérez, J.A.N., Voronkov, A.: Encodings of bounded LTL model checking in effectively propositional logic. In: Automated Deduction (CADE-21), pp. 346-361 (2007) · Zbl 1213.68386 |
| [104] | Pérez, J.A.N., Voronkov, A.: Encodings of problems in effectively propositional logic. In: Theory and Applications of Satisfiability Testing (SAT’07), p. 3 (2007) · Zbl 1213.68386 |
| [105] | Pérez, J.A.N., Voronkov, A.: Proof systems for effectively propositional logic. In: Automated Reasoning (IJCAR’08), pp. 426-440 (2008) · Zbl 1165.03318 |
| [106] | Pérez, J.A.N., Voronkov, A.: Planning with effectively propositional logic. In: Programming Logics—Essays in Memory of Harald Ganzinger, LNCS 7797, pp. 302-316 (2013) · Zbl 1383.68086 |
| [107] | Piskac, R.; de Moura, LM; Bjørner, N., Deciding effectively propositional logic using DPLL and substitution sets, J. Autom. Reason., 44, 4, 401-424 (2010) · Zbl 1197.03011 |
| [108] | Policriti, A.; Omodeo, E., The Bernays-Schönfinkel-Ramsey class for set theory: decidability, J. Symb Log., 77, 896-918 (2012) · Zbl 1251.03025 |
| [109] | Pratt, V.R.: Two easy theories whose combination is hard. Technical report, Massachusetts Institute of Technology (1977) |
| [110] | Putnam, H., Decidability and essential undecidability, J. Symb. Log., 22, 1, 39-54 (1957) · Zbl 0078.24501 |
| [111] | Quaas, K., Shirmohammadi, M., Worrell, J.: Revisiting reachability in timed automata. In: Logic in Computer Science (LICS’17), pp. 1-12 (2017) · Zbl 1457.68147 |
| [112] | Rabin, MO, Decidability of second-order theories and automata on infinite trees, Trans. Am. Math. Soc., 141, 1-35 (1969) · Zbl 0221.02031 |
| [113] | Ranise, S., Ringeissen, C., Tran, D.: Nelson-Oppen, Shostak and the extended canonizer: a family picture with a newborn. In: Theoretical Aspects of Computing (ICTAC’04), Revised Selected Papers, pp. 372-386 (2004) · Zbl 1108.68574 |
| [114] | Ranise, S., Ringeissen, C., Zarba, C.G.: Combining data structures with nonstably infinite theories using many-sorted logic. In: Frontiers of Combining Systems (FroCoS’05), pp. 48-64 (2005) · Zbl 1171.68439 |
| [115] | Rebele, T., Suchanek, F.M., Hoffart, J., Biega, J., Kuzey, E., Weikum, G.: YAGO: A multilingual knowledge base from Wikipedia, Wordnet, and Geonames. In: The Semantic Web (ISWC’16), pp. 177-185 (2016) |
| [116] | Reynolds, A., Barbosa, H., Fontaine, P.: Revisiting Enumerative Instantiation. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS’18), pp. 112-131 (2018) · Zbl 1423.68468 |
| [117] | Reynolds, A., Iosif, R., Serban, C.: Reasoning in the Bernays-Schönfinkel-Ramsey fragment of separation logic. In: Verification, Model Checking, and Abstract Interpretation (VMCAI’17), pp. 462-482 (2017) · Zbl 1484.68104 |
| [118] | Reynolds, A.; King, T.; Kuncak, V., Solving quantified linear arithmetic by counterexample-guided instantiation, Form. Methods Syst. Des., 51, 3, 500-532 (2017) · Zbl 1377.68138 |
| [119] | Robinson, J., Definability and decision problems in arithmetic, J. Symb. Log., 14, 2, 98-114 (1949) · Zbl 0034.00801 |
| [120] | Rueß, H., Shankar, N.: Deconstructing Shostak. In: Logic in Computer Science (LICS’01), pp. 19-28 (2001) |
| [121] | Ruggieri, S.; Eirinakis, P.; Subramani, K.; Wojciechowski, PJ, On the complexity of quantified linear systems, Theor. Comput. Sci., 518, 128-134 (2014) · Zbl 1358.03051 |
| [122] | Schrijver, A., Theory of Linear and Integer Programming (1999), Hoboken: Wiley, Hoboken · Zbl 0665.90063 |
| [123] | Scott, D., A decision method for validity of sentences in two variables, J. Symb. Log., 27, 477 (1962) |
| [124] | Shankar, N., Rueß, H.: Combining Shostak theories. In: Rewriting Techniques and Applications (RTA’02), pp. 1-18 (2002) · Zbl 1045.03015 |
| [125] | Shelah, S., The monadic theory of order, Ann. Math., 102, 3, 379-419 (1975) · Zbl 0345.02034 |
| [126] | Shostak, RE, Deciding combinations of theories, J. ACM, 31, 1, 1-12 (1984) · Zbl 0629.68089 |
| [127] | Sofronie-Stokkermans, V.: Hierarchic reasoning in local theory extensions. In: Automated Deduction (CADE-20), pp. 219-234 (2005) · Zbl 1135.03330 |
| [128] | Sofronie-Stokkermans, V.: On combinations of local theory extensions. In: Programming Logics—Essays in Memory of Harald Ganzinger, LNCS 7797 pp. 392-413 (2013) · Zbl 1383.03020 |
| [129] | Sofronie-Stokkermans, V.: Hierarchical reasoning in local theory extensions and applications. In: Symbolic and Numeric Algorithms for Scientific Computing (SYNASC’14), pp. 34-41 (2014) · Zbl 1476.03043 |
| [130] | Strichman, O., Seshia, S.A., Bryant, R.E.: Deciding separation formulas with SAT. In: Computer Aided Verification (CAV’02), pp. 209-222 (2002) · Zbl 1010.68168 |
| [131] | Sturm, T., A survey of some methods for real quantifier elimination, decision, and satisfiability and their applications, Math. Comput. Sci., 11, 3-4, 483-502 (2017) · Zbl 1425.68380 |
| [132] | Sturm, T., Voigt, M., Weidenbach, C.: Deciding first-order satisfiability when universal and existential variables are separated. In: Logic in Computer Science (LICS’16), pp. 86-95. IEEE/ACM (2016). An extended version is available at the arXiv preprint server under the signature arXiv:1511.08999 [cs.LO] · Zbl 1394.03013 |
| [133] | Suchanek, FM; Kasneci, G.; Weikum, G., YAGO: a large ontology from Wikipedia and WordNet, J. Web Semant., 6, 3, 203-217 (2008) |
| [134] | Suda, M., Weidenbach, C., Wischnewski, P.: On the saturation of YAGO. In: Automated Reasoning (IJCAR’10), pp. 441-456 (2010) · Zbl 1291.68372 |
| [135] | Talupur, M., Sinha, N., Strichman, O., Pnueli, A.: Range allocation for separation logic. In: Computer Aided Verification (CAV’04), pp. 148-161 (2004) · Zbl 1103.68079 |
| [136] | Tinelli, C., Harandi, M.T.: A new correctness proof of the Nelson-Oppen combination procedure. In: Frontiers of Combining Systems (FroCoS’96), pp. 103-119 (1996) · Zbl 0893.03001 |
| [137] | Tinelli, C.; Ringeissen, C., Unions of non-disjoint theories and combinations of satisfiability procedures, Theor. Comput. Sci., 290, 1, 291-353 (2003) · Zbl 1018.68033 |
| [138] | Tinelli, C.; Zarba, CG, Combining nonstably infinite theories, J. Autom. Reason., 34, 3, 209-238 (2005) · Zbl 1108.03014 |
| [139] | Tran, D.; Ringeissen, C.; Ranise, S.; Kirchner, H., Combination of convex theories: modularity, deduction completeness, and explanation, J. Symb. Comput., 45, 2, 261-286 (2010) · Zbl 1192.68190 |
| [140] | Voigt, M.: The Bernays-Schönfinkel-Ramsey fragment with bounded difference constraints over the reals is decidable. In: Frontiers of Combining Systems (FroCoS’17), LNCS 10483, pp. 244-261 (2017). An extended version is available at the arXiv preprint server under the signature arXiv:1706.08504 [cs.LO] · Zbl 1496.03032 |
| [141] | Voigt, M.: A fine-grained hierarchy of hard problems in the separated fragment. In: Logic in Computer Science (LICS’17), pp. 1-12. IEEE/ACM (2017). An extended version is available at the arXiv preprint server under the signature arXiv:1704.02145 [cs.LO] · Zbl 1457.68118 |
| [142] | Voigt, M.: Decidable fragments of first-order logic and of first-order linear arithmetic with uninterpreted predicates. Ph.D. thesis, Department of Computer Science, Saarland University (2019). doi:10.22028/D291-28428 |
| [143] | Voigt, M.: Separateness of variables—a novel perspective on decidable first-order fragments (2019). Submitted. A preprint version is available at the arXiv preprint server under the signature arXiv:1911.11500 [cs.LO] |
| [144] | Voigt, M., Weidenbach, C.: Bernays-Schönfinkel-Ramsey with simple bounds is NEXPTIME-complete. ArXiv preprint arXiv:1501.07209 [cs.LO] (2015). http://arxiv.org/abs/1501.07209 |
| [145] | Wang, C., Gupta, A., Ganai, M.K.: Predicate learning and selective theory deduction for a difference logic solver. In: Design Automation Conference (DAC’06), pp. 235-240 (2006) |
| [146] | Weispfenning, V., The complexity of linear problems in fields, J. Symb. Comput., 5, 1-2, 3-27 (1988) · Zbl 0646.03005 |
| [147] | Wies, T., Piskac, R., Kuncak, V.: Combining theories with shared set operations. In: Frontiers of Combining Systems (FroCoS’09), LNCS 5749, pp. 366-382. Springer (2009) · Zbl 1193.03030 |
| [148] | Wischnewski, P.: Efficient reasoning procedures for complex first-order theories. Ph.D. thesis, Department of Computer Science, Saarland University (2012) |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
