Finding finite models in multi-sorted first-order logic. (English) Zbl 1475.68447
Creignou, Nadia (ed.) et al., Theory and applications of satisfiability testing – SAT 2016. 19th international conference, Bordeaux, France, July 5–8, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9710, 323-341 (2016).
Summary: This work extends the existing MACE-style finite model finding approach to multi-sorted first-order logic. This existing approach iteratively assumes increasing domain sizes and encodes the related ground problem as a SAT problem. When moving to the multi-sorted setting each sort may have a different domain size, leading to an explosion in the search space. This paper focusses on methods to tame that search space. The key approach adds additional information to the SAT encoding to suggest which domains should be grown. Evaluation of an implementation of techniques in the Vampire theorem prover shows that they dramatically reduce the search space and that this is an effective approach to find finite models in multi-sorted first-order logic.
For the entire collection see [Zbl 1337.68009].
For the entire collection see [Zbl 1337.68009].
MSC:
| 68V15 | Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) |
| 03C13 | Model theory of finite structures |
| 68T20 | Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) |
References:
| [1] | Barrett, C., Stump, A., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2010). http://www.SMT-LIB.org |
| [2] | Blanchette, J.C., Böhme, S., Popescu, A., Smallbone, N.: Encoding monomorphic and polymorphic types. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 493–507. Springer, Heidelberg (2013) · Zbl 1381.68259 · doi:10.1007/978-3-642-36742-7_34 |
| [3] | Claessen, K., Lillieström, A.: Automated inference of finite unsatisfiability. J. Autom. Reasoning 47(2), 111–132 (2011) · Zbl 1243.68266 · doi:10.1007/s10817-010-9216-8 |
| [4] | Claessen, K., Lillieström, A., Smallbone, N.: Sort it out with monotonicity. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 207–221. Springer, Heidelberg (2011) · Zbl 1341.03017 · doi:10.1007/978-3-642-22438-6_17 |
| [5] | Claessen, K., Sörensson, N.: New techniques that improve MACE-style model finding. In: CADE-19 Workshop: Model Computation - Principles, Algorithms and Applications (2003) |
| [6] | Eén, N., Biere, A.: Effective preprocessing in SAT through variable and clause elimination. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 61–75. Springer, Heidelberg (2005) · Zbl 1128.68463 · doi:10.1007/11499107_5 |
| [7] | Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004) · Zbl 1204.68191 · doi:10.1007/978-3-540-24605-3_37 |
| [8] | Eén, N., Sörensson, N.: Temporal induction by incremental SAT solving. Electr. Notes Theor. Comput. Sci. 89(4), 543–560 (2003) · Zbl 1271.68215 · doi:10.1016/S1571-0661(05)82542-3 |
| [9] | Hoder, K., Kovács, L., Voronkov, A.: Case studies on invariant generation using a saturation theorem prover. In: Batyrshin, I., Sidorov, G. (eds.) MICAI 2011, Part I. LNCS, vol. 7094, pp. 1–15. Springer, Heidelberg (2011) · doi:10.1007/978-3-642-25324-9_1 |
| [10] | Korovin, K.: iProver – an instantiation-based theorem prover for first-order logic (System Description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 292–298. Springer, Heidelberg (2008) · Zbl 1165.68462 · doi:10.1007/978-3-540-71070-7_24 |
| [11] | Kovács, L., Voronkov, A.: First-order theorem proving and vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1–35. Springer, Heidelberg (2013) · doi:10.1007/978-3-642-39799-8_1 |
| [12] | Mccune, W.: A Davis-Putnam Program and its Application to Finite First-Order Model Search: Quasigroup Existence Problems. Technical report, Argonne National Laboratory (1994) |
| [13] | Reynolds, A., Tinelli, C., Goel, A., Krstić, S.: Finite model finding in SMT. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 640–655. Springer, Heidelberg (2013) · doi:10.1007/978-3-642-39799-8_42 |
| [14] | Schulz, S.: A comparison of different techniques for grounding near-propositional CNF formulae. In: Proceedings of the Fifteenth International Florida Artificial Intelligence Research Society Conference, May 14–16, 2002, Pensacola Beach, Florida, USA, pp. 72–76 (2002) |
| [15] | Stump, A., Sutcliffe, G., Tinelli, C.: StarExec, a cross community logic solving service (2012). https://www.starexec.org |
| [16] | Sutcliffe, G.: The TPTP problem library and associated infrastructure. J. Autom. Reasoning 43(4), 337–362 (2009) · Zbl 1185.68636 · doi:10.1007/s10817-009-9143-8 |
| [17] | Tammet, T.: Reasoning. Gandalf. J. Autom 18(2), 199–204 (1997) |
| [18] | Zhang, J., Zhang, H.: SEM: a system for enumerating models. In: Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence, IJCAI 95, Montréal Québec, Canada, August 20–25 1995, vol. 2s, pp. 298–303 (1995) |
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.
