Instantiation Schemes for Nested Theories

Abstract

This article investigates under which conditions instantiation-based proof procedures can be combined in a nested way, in order to mechanically construct new instantiation procedures for richer theories. Interesting applications in the field of verification are emphasized, particularly for handling extensions of the theory of arrays.

References

1. Abadi, A., Rabinovich, A., and Sagiv, M. 2010. Decidable fragments of many-sorted logic. J. Symbolic Comput. 45, 2, 153--172.
2. Althaus, E., Kruglov, E., and Weidenbach, C. 2009. Superposition modulo linear arithmetic sup(la). In Proceedings of the 7th International Symposium on Frontiers of Combining Systems. S. Ghilardi and R. Sebastiani Eds., Lecture Notes in Computer Science, vol. 5749, Springer, 84--99.
3. Bachmair, L. and Ganzinger, H. 1994. Rewrite-based equational theorem proving with selection and simplification. J. Logic Comput. 3, 4, 217--247.
4. Bachmair, L., Ganzinger, H., and Waldmann, U. 1994. Refutational theorem proving for hierachic first-order theories. Appl. Algebra Eng. Commun. Comput. 5, 193--212.
5. Barrett, C., Stump, A., and Tinelli, C. 2010. The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org.
6. Basin, D. and Ganzinger, H. 2001. Automated complexity analysis based on ordered resolution. J. ACM 48, 70--109.
7. Baumgartner, P. and Tinelli, C. 2003. The model evolution calculus. In Proceedings of the 19th International Conference on Automated Deduction. F. Baader Ed., Lecture Notes in Artificial Intelligence, vol. 2741, Springer, 350--364.
8. Bonacina, M. P., Lynch, C. A., and Moura, L. 2011. On deciding satisfiability by theorem proving with speculative inferences. J. Autom. Reason. 47, 161--189.
9. Bradley, A. R. and Manna, Z. 2007. The Calculus of Computation: Decision Procedures with Applications to Verification. Springer.
10. Bradley, A. R., Manna, Z., and Sipma, H. B. 2006. What’s decidable about arrays? In Proceedings of the Conference on Verification, Model-Checking and Abstract Interpretation. E. A. Emerson and K. S. Namjoshi Eds., Lecture Notes in Computer Science, vol. 3855, Springer, 427--442.
11. Bruttomesso, R., Cimatti, A., Franzén, A., Griggio, A., and Sebastiani, R. 2009. Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: A comparative analysis. Ann. Math. Artif. Intell. 55, 1--2, 63--99.
12. Comon, H. and Delor, C. 1994. Equational formulae with membership constraints. Inf. Comput. 112, 2, 167--216.
13. Comon, H., Dauchet, M., Gilleron, R., Jacquemard, F., Lugiez, D., Tison, S., and Tommasi, M. 1997. Tree automata techniques and applications. http://www.grappa.univ-lille3.fr/tata.
14. de Moura, L. M. and Bjørner, N. 2007. Efficient E-matching for SMT solvers. In Proceedings of the International Conference on Automated Deduction. F. Pfenning Ed., Lecture Notes in Computer Science, vol. 4603, Springer, 183--198.
15. de Moura, L. M. and Bjørner, N. 2009. Generalized, efficient array decision procedures. In Proceedings of the International Conference on Formal Methods in Computer-Aided Design. IEEE, 45--52.
16. Detlefs, D. L., Nelson, G., and Saxe, J. B. 2005. Simplify: a theorem prover for program checking. J. ACM 52, 3, 365--473.
17. Dreben, B. and Goldfarb, W. D. 1979. The Decision Problem, Solvable Classes of Quantificational Formulas. Addison-Wesley.
18. Echenim, M. and Peltier, N. 2010. Instantiation of SMT problems modulo integers. In Proceedings of the 10th International Conference on Artificial Intelligence and Symbolic Computation. Lecture Notes in Computer Science, vol. 6167, Springer, 49--63.
19. Echenim, M. and Peltier. 2011. Modular instantiation schemes. Inf. Process. Lett. 111, 20, 989--993.
20. Echenim, M. and Peltier, 2012. An instantiation scheme for satisfiability modulo theories. J. Automat. Reason. 48, 3.
21. Fontaine, P. 2009. Combinations of theories for decidable fragments of first-order logic. In Proceedings of the 7th International Symposium on Frontiers of Combining Systems. S. Ghilardi and R. Sebastiani Eds. Lecture Notes in Computer Science, vol. 5749, Springer, 263--278.
22. Fontaine, P., Ranise, S., and Zarba, C. G. 2004. Combining lists with non-stably infinite theories. In Proceedings of the International Conference on Logic Programming, Artificial Intelligence and Reasoning. Lecture Notes in Computer Science, vol. 3452, Springer, 51--66.
23. Ganzinger, H. 2001. Relating semantic and proof-theoretic concepts for polynomial time decidability of uniform word problems. In Proceedings of the 16th IEEE Symposium on Logic in Computer Science (LICS’01). 81--92.
24. Ganzinger, H. and Korovin, K. 2003. New directions in instantiation-based theorem proving. In Proceedings of the 18th IEEE Symposium on Logic in Computer Science (LICS’03). IEEE Computer Society Press, 55--64.
25. Ganzinger, H., Sofronie-Stokkermans, V., and Waldmann, U. 2006. Modular proof systems for partial functions with Evans equality. Inf. Comput. 204, 1453--1492.
26. Ge, Y. and de Moura, L. M. 2009. Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In Proceedings of the International Conference on Computer Aided Verification. A. Bouajjani and O. Maler Eds., Lecture Notes in Computer Science, vol. 5643, Springer, 306--320.
27. Ge, Y., Barrett, C. W., and Tinelli, C. 2009. Solving quantified verification conditions using satisfiability modulo theories. Ann. Math. Artif. Intell. 55, 1--2, 101--122.
28. Ghilardi, S. and Ranise, S. 2010. Backward reachability of array-based systems by SMT solving: Termination and invariant synthesis. Logical Methods Comput. Sci. 6, 4.
29. Ghilardi, S., Nicolini, E., Ranise, S., and Zucchelli, D. 2007. Decision procedures for extensions of the theory of arrays. Ann. Math. Artif. Intell. 50, 231--254.
30. Givan, R. 2000. Polynomial-time computation via local inference relations. ACM Trans. Comput. Logic 3, 2002.
31. Givan, R. and McAllester, D. 1992. New results on local inference relations. In Proceedings of the 3rd International Conference on Principles of Knowledge Representation and Reasoning. Morgan Kaufman Press, 403--412.
32. Goel, A., Krstić, S., and Fuchs, A. 2008. Deciding array formulas with frugal axiom instantiation. In Proceedings of the Joint Workshops of the 6th International Workshop on Satisfiability Modulo Theories and 1st International Workshop on Bit-Precise Reasoning (SMT’08/BPR’08). ACM, New York, 12--17.
33. Habermehl, P., Iosif, R., and Vojnar, T. 2008. What else is decidable about integer arrays? In Proceedings of the International Conference on Foundations of Software Science and Computation Structures. R. M. Amadio Ed., Lecture Notes in Computer Science, vol. 4962, Springer, 474--489.
34. Ihlemann, C., Jacobs, S., and Sofronie-Stokkermans, V. 2008. On local reasoning in verification. In Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 4963, Springer, 265--281.
35. Jacobs, S. 2008. Incremental instance generation in local reasoning. In Notes from the 1st CEDAR Workshop, International Conference on Automated Reasoning (IJCAR’08). F. Baader, S. Ghilardi, M. Hermann, U. Sattler, and V. Sofronie-Stokkermans Eds., 47--62.
36. Kapur, D. and Zarba, C. G. 2005. A reduction approach to decision procedures. Tech. rep. http://www.cs.unm.edu/kapur/mypapers/reduction.pdf.
37. Lee, S. and Plaisted, D. A. 1992. Eliminating duplication with the hyper-linking strategy. J. Automat. Reason. 9, 25--42.
38. Loos, R. and Weispfenning, V. 1993. Applying linear quantifier elimination. Comput. J. 36, 5, 450--462.
39. McPeak, S. and Necula, G. C. 2005. Data structure specifications via local equality axioms. In Proceedings of the International Conference on Computer Aided Verification. Springer, 476--490.
40. Nelson, G. and Oppen, D. C. 1979. Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1, 245--257.
41. Ohlbach, H. J. and Koehler, J. 1999. Modal logics, description logics and arithmetic reasoning. Artif. Intell. 109, 1--31.
42. Plaisted, D. A. and Zhu, Y. 2000. Ordered semantic hyperlinking. J. Automat. Reason. 25, 3, 167--217.
43. Sofronie-Stokkermans, V. 2005. Hierarchic reasoning in local theory extensions. In Proceedings of the International Conference on Automated Deduction. R. Nieuwenhuis Ed., Lecture Notes in Computer Science, vol. 3632, Springer, 219--234.
44. Sofronie-Stokkermans, V. 2010. Hierarchical reasoning for the verification of parametric systems. In Proceedings of the International Conference on Automated Reasoning. J. Giesl and R. Hähnle Eds., Lecture Notes in Computer Science, vol. 6173, Springer, 171--187.
45. Tinelli, C. and Harandi, M. 1996. A new correctness proof of the Nelson-Oppen combination procedure. In Frontiers of Combining Systems, Applied Logic Series, vol. 3, Kluwer Academic Publishers, 103--120.

Index Terms

• Computing methodologies

  • Artificial intelligence

    • Knowledge representation and reasoning

  • Symbolic and algebraic manipulation

    • Symbolic and algebraic algorithms

      • Theorem proving algorithms