Abstract
We present a new proof procedure for reasoning on schemas of formulas defined over various (decidable) base logics (e.g. propositional logic, Presburger arithmetic etc.). Such schemas are useful to model sequences of formulas defined by induction on some parameter. The approach works by computing an automaton accepting exactly the values of the parameter for which the formula is satisfiable. Its main advantage is that it is completely modular, in the sense that external tools are used as “black boxes” both to reason on base formulas and to detect cycles in the proof search. This makes the approach more efficient and scalable than previous attempts. Experimental results are presented, showing evidence of the practical interest of the proposed method.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Aravantinos, V., Caferra, R., Peltier, N.: Complexity of the satisfiability problem for a class of propositional schemata. In: Dediu, A.-H., Fernau, H., Martín-Vide, C. (eds.) LATA 2010. LNCS, vol. 6031, pp. 58–69. Springer, Heidelberg (2010)
Aravantinos, V., Caferra, R., Peltier, N.: RegSTAB: A SAT solver for propositional schemata. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 309–315. Springer, Heidelberg (2010)
Aravantinos, V., Caferra, R., Peltier, N.: Decidability and undecidability results for propositional schemata. Journal of Artificial Intelligence Research 40, 599–656 (2011)
Aravantinos, V., Peltier, N.: Schemata of SMT-problems. In: Brünnler, K., Metcalfe, G. (eds.) TABLEAUX 2011. LNCS, vol. 6793, pp. 27–42. Springer, Heidelberg (2011)
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press (1998)
Barrett, C., Stump, A., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2010). http://www.SMT-LIB.org
Comon, H., Dauchet, M., Gilleron, R., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree automata techniques and applications (1997). http://www.grappa.univ-lille3.fr/tata
Dershowitz, N., Jouannaud, J.: Rewrite systems. In: Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B), pp. 243–320 (1990)
Hähnle, R.: Tableaux and related methods. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 3, vol. I, pp. 100–178. Elsevier Science (2001)
de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)
Robinson, A., Voronkov, A. (eds.): Handbook of Automated Reasoning. North-Holland (2001)
Wielemakers, J.: SWI-Prolog version 7 extensions. In: WLPE 2014, July 2014
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Peltier, N. (2015). Reasoning on Schemas of Formulas: An Automata-Based Approach. In: Dediu, AH., Formenti, E., Martín-Vide, C., Truthe, B. (eds) Language and Automata Theory and Applications. LATA 2015. Lecture Notes in Computer Science(), vol 8977. Springer, Cham. https://doi.org/10.1007/978-3-319-15579-1_20
Download citation
DOI: https://doi.org/10.1007/978-3-319-15579-1_20
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-15578-4
Online ISBN: 978-3-319-15579-1
eBook Packages: Computer ScienceComputer Science (R0)