Symbolic model construction for saturated constrained Horn clauses. (English) Zbl 1540.03020
Sattler, Uli (ed.) et al., Frontiers of combining systems. 14th international symposium, Frocos 2023, Prague, Czech Republic, September 20–22, 2023. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 14279, 137-155 (2023).
Summary: Clause sets saturated by hierarchic ordered resolution do not offer a model representation that can be effectively queried, in general. They only offer the guarantee of the existence of a model. We present an effective symbolic model construction for saturated constrained Horn clauses. Constraints are in linear arithmetic, the first-order part is restricted to a function-free language. The model is constructed in finite time, and non-ground clauses can be effectively evaluated with respect to the model. Furthermore, we prove that our model construction produces the least model.
For the entire collection see [Zbl 1535.68013].
For the entire collection see [Zbl 1535.68013].
MSC:
| 03B35 | Mechanization of proofs and logical operations |
Keywords:
Bernays-Schönfinkel fragment; linear arithmetic; Horn clauses; superposition; model constructionSoftware:
SpacerReferences:
| [1] | Althaus, E.; Kruglov, E.; Weidenbach, C.; Ghilardi, S.; Sebastiani, R., Superposition modulo linear arithmetic SUP(LA), Frontiers of Combining Systems, 84-99 (2009), Heidelberg: Springer, Heidelberg · Zbl 1193.03024 · doi:10.1007/978-3-642-04222-5_5 |
| [2] | Bachmair, L.; Ganzinger, H.; Waldmann, U.; Gottlob, G.; Leitsch, A.; Mundici, D., Superposition with simplification as a decision procedure for the monadic class with equality, Computational Logic and Proof Theory, 83-96 (1993), Heidelberg: Springer, Heidelberg · Zbl 0793.68127 · doi:10.1007/BFb0022557 |
| [3] | Bachmair, L.; Ganzinger, H.; Waldmann, U., Refutational theorem proving for hierarchic first-order theories, AAECC, 5, 193-212 (1994) · Zbl 0797.03008 · doi:10.1007/BF01190829 |
| [4] | Basin, DA; Ganzinger, H., Automated complexity analysis based on ordered resolution, JACM, 48, 1, 70-109 (2001) · Zbl 1320.68163 · doi:10.1145/363647.363681 |
| [5] | Baumgartner, P.; Fuchs, A.; Tinelli, C.; Cervesato, I.; Veith, H.; Voronkov, A., (LIA) - model evolution with linear integer arithmetic constraints, Logic for Programming, Artificial Intelligence, and Reasoning, 258-273 (2008), Heidelberg: Springer, Heidelberg · Zbl 1182.03033 · doi:10.1007/978-3-540-89439-1_19 |
| [6] | Baumgartner, P.; Waldmann, U.; Lutz, C.; Sattler, U.; Tinelli, C.; Turhan, A-Y; Wolter, F., Hierarchic superposition revisited, Description Logic, Theory Combination, and All That, 15-56 (2019), Cham: Springer, Cham · Zbl 1443.68212 · doi:10.1007/978-3-030-22102-7_2 |
| [7] | Bjørner, N.; Gurfinkel, A.; McMillan, K.; Rybalchenko, A.; Beklemishev, LD; Blass, A.; Dershowitz, N.; Finkbeiner, B.; Schulte, W., Horn clause solvers for program verification, Fields of Logic and Computation II, 24-51 (2015), Cham: Springer, Cham · Zbl 1465.68044 · doi:10.1007/978-3-319-23534-9_2 |
| [8] | Bromberger, M., A sorted datalog hammer for supervisor verification conditions modulo simple linear arithmetic, Tools and Algorithms for the Construction and Analysis of Systems, 480-501 (2022), Cham: Springer, Cham · doi:10.1007/978-3-030-99524-9_27 |
| [9] | Bromberger, M.; Dragoste, I.; Faqeh, R.; Fetzer, C.; Krötzsch, M.; Weidenbach, C.; Konev, B.; Reger, G., A datalog hammer for supervisor verification conditions modulo simple linear arithmetic, Frontiers of Combining Systems, 3-24 (2021), Cham: Springer, Cham · Zbl 07497913 · doi:10.1007/978-3-030-86205-3_1 |
| [10] | Bromberger, M.; Fiori, A.; Weidenbach, C.; Henglein, F.; Shoham, S.; Vizel, Y., Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories, Verification, Model Checking, and Abstract Interpretation, 511-533 (2021), Cham: Springer, Cham · Zbl 1472.03024 · doi:10.1007/978-3-030-67067-2_23 |
| [11] | Bromberger, M., Leutgeb, L., Weidenbach, C.: An efficient subsumption test pipeline for BS(LRA) clauses. In: Blanchette, J., Kovács, L., Pattinson, D. (eds.) IJCAR 2022. LNCS, vol. 13385, pp. 147-168. Springer, Cham (2022). doi:10.1007/978-3-031-10769-6_10 · Zbl 07628186 |
| [12] | Bromberger, M., Leutgeb, L., Weidenbach, C.: Symbolic model construction for saturated constrained horn clauses. arXiv (2023). doi:10.48550/arXiv.2305.05064 · Zbl 07628186 |
| [13] | Caferra, R.; Leitsch, A.; Peltier, N., Automated Model Building, APLS (2004), Dordrecht: Springer, Dordrecht · Zbl 1085.03009 · doi:10.1007/978-1-4020-2653-9 |
| [14] | Cooper, DC, Theorem proving in arithmetic without multiplication, Mach. Intell., 7, 91-99 (1972) · Zbl 0258.68046 |
| [15] | De Angelis, E.; Fioravanti, F.; Gallagher, JP; Hermenegildo, MV; Pettorossi, A.; Proietti, M., Analysis and transformation of constrained horn clauses for program verification, TPLP, 22, 6, 974-1042 (2022) · Zbl 1541.68215 · doi:10.1017/S1471068421000211 |
| [16] | Downey, P.J.: Undecidability of presburger arithmetic with a single monadic predicate letter. Center for Research in Computer Technology, Harvard University, Technical report (1972) |
| [17] | Fedyukovich, G.; Zhang, Y.; Gupta, A.; Chockler, H.; Weissenbacher, G., Syntax-guided termination analysis, Computer Aided Verification, 124-143 (2018), Cham: Springer, Cham · Zbl 1511.68076 · doi:10.1007/978-3-319-96145-3_7 |
| [18] | Feferman, S.: Some applications of the notions of forcing and generic sets. Fundamenta Mathematicae. 56(3), 325-345 (1964). http://eudml.org/doc/213821 · Zbl 0129.26401 |
| [19] | Fermüller, CG; Leitsch, A., Hyperresolution and automated model building, LOGCOM, 6, 2, 173-203 (1996) · Zbl 0861.68086 · doi:10.1093/logcom/6.2.173 |
| [20] | Fermüller, CG; Leitsch, A., Decision procedures and model building in equational clause logic, IGPL, 6, 1, 17-41 (1998) · Zbl 0903.03010 · doi:10.1093/jigpal/6.1.17 |
| [21] | Fiori, A., Weidenbach, C.: SCL with theory constraints. arXiv (2020). http://arxiv.org/abs/2003.04627 |
| [22] | Gange, G.; Navas, JA; Schachte, P.; Søndergaard, H.; Stuckey, PJ, Horn clauses as an intermediate representation for program analysis and transformation, TPLP, 15, 4-5, 526-542 (2015) · Zbl 1379.68089 · doi:10.1017/S1471068415000204 |
| [23] | Ganzinger, H., de Nivelle, H.: A superposition decision procedure for the guarded fragment with equality. In: 14th LICS, 1999, pp. 295-303. IEEE Computer Society (1999). doi:10.1109/LICS.1999.782624 |
| [24] | Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: PLDI, pp. 405-416. ACM (2012). doi:10.1145/2254064.2254112 |
| [25] | Hoder, K.; Bjørner, N.; Cimatti, A.; Sebastiani, R., Generalized property directed reachability, Theory and Applications of Satisfiability Testing - SAT 2012, 157-171 (2012), Heidelberg: Springer, Heidelberg · Zbl 1273.68229 · doi:10.1007/978-3-642-31612-8_13 |
| [26] | Horbach, M., Voigt, M., Weidenbach, C.: The universal fragment of presburger arithmetic with unary uninterpreted predicates is undecidable. arXiv (2017). http://arxiv.org/abs/1703.01212 |
| [27] | Jaffar, J.; Maher, MJ, Constraint logic programming: a survey, JLP, 19, 20, 503-581 (1994) · doi:10.1016/0743-1066(94)90033-7 |
| [28] | Komuravelli, A.; Gurfinkel, A.; Chaki, S.; Biere, A.; Bloem, R., SMT-based model checking for recursive programs, Computer Aided Verification, 17-34 (2014), Cham: Springer, Cham · doi:10.1007/978-3-319-08867-9_2 |
| [29] | Korovin, K.; Voronkov, A.; Duparc, J.; Henzinger, TA, Integrating linear arithmetic into superposition calculus, Computer Science Logic, 223-237 (2007), Heidelberg: Springer, Heidelberg · Zbl 1179.03018 · doi:10.1007/978-3-540-74915-8_19 |
| [30] | Kruglov, E.: Superposition modulo theory. Ph.D. thesis, Saarland University (2013). http://scidok.sulb.uni-saarland.de/volltexte/2013/5559/ |
| [31] | Lloyd, JW, Foundations of Logic Programming (1987), Cham: Springer, Cham · Zbl 0668.68004 · doi:10.1007/978-3-642-83189-8 |
| [32] | Loos, R.; Weispfenning, V., Applying linear quantifier elimination, Comput. J., 36, 5, 450-462 (1993) · Zbl 0787.03021 · doi:10.1093/comjnl/36.5.450 |
| [33] | López-García, P.; Darmawan, L.; Klemen, M.; Liqat, U.; Bueno, F.; Hermenegildo, MV, Interval-based resource usage verification by translation into horn clauses and an application to energy consumption, TPLP, 18, 2, 167-223 (2018) · Zbl 1478.68170 · doi:10.1017/S1471068418000042 |
| [34] | McMillan, KL; Biere, A.; Bloem, R., Lazy annotation revisited, Computer Aided Verification, 243-259 (2014), Cham: Springer, Cham · doi:10.1007/978-3-319-08867-9_16 |
| [35] | Mesnard, F.; Payet, É.; Vidal, G., Concolic testing in CLP, TPLP, 20, 5, 671-686 (2020) · Zbl 1468.68055 · doi:10.1017/S1471068420000216 |
| [36] | Oppen, DC, A \(2 \hat{} 2 \hat{} 2 \hat{}\) PN upper bound on the complexity of Presburger arithmetic, JCSS, 16, 3, 323-332 (1978) · Zbl 0381.03021 · doi:10.1016/0022-0000(78)90021-1 |
| [37] | Rümmer, P.; Cervesato, I.; Veith, H.; Voronkov, A., A constraint sequent calculus for first-order logic with linear integer arithmetic, Logic for Programming, Artificial Intelligence, and Reasoning, 274-289 (2008), Heidelberg: Springer, Heidelberg · Zbl 1182.03035 · doi:10.1007/978-3-540-89439-1_20 |
| [38] | Spoto, F.; Mesnard, F.; Payet, É., A termination analyzer for java bytecode based on path-length, TOPLAS, 32, 3, 8:1-8:70 (2010) · doi:10.1145/1709093.1709095 |
| [39] | Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pac. J. Math. 5(2), 285-309 (1955). doi:10.2140/pjm.1955.5.285 · Zbl 0064.26004 |
| [40] | Weidenbach, C.; Meyer, R.; Platzer, A.; Wehrheim, H., Automated reasoning building blocks, Correct System Design, 172-188 (2015), Cham: Springer, Cham · Zbl 1444.68289 · doi:10.1007/978-3-319-23506-6_12 |
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.
