Document Open Access Logo

A Decidable Fragment of Second Order Logic With Applications to Synthesis

Authors P. Madhusudan, Umang Mathur , Shambwaditya Saha, Mahesh Viswanathan

PDF
Thumbnail PDF

File

LIPIcs.CSL.2018.31.pdf
  • Filesize: 0.6 MB
  • 19 pages

Document Identifiers

Author Details

P. Madhusudan
  • University of Illinois, Urbana Champaign, Urbana, IL, USA
Umang Mathur
  • University of Illinois, Urbana Champaign, Urbana, IL, USA
Shambwaditya Saha
  • University of Illinois, Urbana Champaign, Urbana, IL, USA
Mahesh Viswanathan
  • University of Illinois, Urbana Champaign, Urbana, IL, USA

Funding

This work has been supported by NSF grants 1422798, 1329991, 1138994 and 1527395.

Cite AsGet BibTex

P. Madhusudan, Umang Mathur, Shambwaditya Saha, and Mahesh Viswanathan. A Decidable Fragment of Second Order Logic With Applications to Synthesis. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 31:1-31:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.CSL.2018.31

Abstract

We propose a fragment of many-sorted second order logic called EQSMT and show that checking satisfiability of sentences in this fragment is decidable. EQSMT formulae have an exists^*forall^* quantifier prefix (over variables, functions and relations) making EQSMT conducive for modeling synthesis problems. Moreover, EQSMT allows reasoning using a combination of background theories provided that they have a decidable satisfiability problem for the exists^*forall^* FO-fragment (e.g., linear arithmetic). Our decision procedure reduces the satisfiability of EQSMT formulae to satisfiability queries of exists^*forall^* formulae of each individual background theory, allowing us to use existing efficient SMT solvers supporting exists^*forall^* reasoning for these theories; hence our procedure can be seen as effectively quantified SMT (EQSMT) reasoning.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • second order logic
  • synthesis
  • decidable fragment

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Aharon Abadi, Alexander Rabinovich, and Mooly Sagiv. Decidable fragments of many-sorted logic. Journal of Symbolic Computation, 45(2):153-172, 2010. Google Scholar
  2. Wilhelm Ackermann. Solvable cases of the decision problem. North-Holland Publishing Company Amsterdam, 1962. Google Scholar
  3. Francesco Alberti, Silvio Ghilardi, and Natasha Sharygina. Decision procedures for flat array properties. J. Autom. Reason., 54(4):327-352, 2015. URL: http://dx.doi.org/10.1007/s10817-015-9323-7.
  4. Rajeev Alur, Rastislav Bodík, Eric Dallal, Dana Fisman, Pranav Garg, Garvit Juniwal, Hadas Kress-Gazit, P. Madhusudan, Milo M. K. Martin, Mukund Raghothaman, Shambwaditya Saha, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa. Syntax-guided synthesis. In Dependable Software Systems Engineering, pages 1-25. IOS Press, 2015. URL: http://dx.doi.org/10.3233/978-1-61499-495-4-1.
  5. Paul Bernays and Moses Schönfinkel. Zum entscheidungsproblem der mathematischen logik. Mathematische Annalen, 1928. Google Scholar
  6. Dirk Beyer, Thomas A. Henzinger, Rupak Majumdar, and Andrey Rybalchenko. Invariant synthesis for combined theories. In Byron Cook and Andreas Podelski, editors, Verification, Model Checking, and Abstract Interpretation, pages 378-394, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. Google Scholar
  7. Roderick Bloem, Stefan Galler, Barbara Jobstmann, Nir Piterman, Amir Pnueli, and Martin Weiglhofer. Interactive presentation: Automatic hardware synthesis from specifications: A case study. In Proceedings of the Conference on Design, Automation and Test in Europe, DATE '07, 2007. Google Scholar
  8. Egon Börger, Erich Grädel, and Yuri Gurevich. The classical decision problem. Springer Science &Business Media, 2001. Google Scholar
  9. Aaron R. Bradley, Zohar Manna, and Henny B. Sipma. What’s decidable about arrays? In E. Allen Emerson and Kedar S. Namjoshi, editors, Verification, Model Checking, and Abstract Interpretation, pages 427-442, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg. Google Scholar
  10. J Richard Buchi and Lawrence H Landweber. Solving sequential conditions by finite-state strategies. Transactions of the American Mathematical Society, 1969. Google Scholar
  11. Benjamin Caulfield, Markus N. Rabe, Sanjit A. Seshia, and Stavros Tripakis. What’s decidable about syntax-guided synthesis? CoRR, abs/1510.08393, 2015. Google Scholar
  12. Leonardo De Moura and Nikolaj Bjørner. Z3: An efficient smt solver. In TACAS, 2008. Google Scholar
  13. Adrià Gascón, Ashish Tiwari, Brent Carmer, and Umang Mathur. Look for the proof to find the program: Decorated-component-based program synthesis. In Computer Aided Verification, 2017. Google Scholar
  14. Sumit Gulwani. Dimensions in program synthesis. In Proceedings of the 12th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, PPDP '10, pages 13-24, New York, NY, USA, 2010. ACM. URL: http://dx.doi.org/10.1145/1836089.1836091.
  15. Matthias Horbach, Marco Voigt, and Christoph Weidenbach. On the combination of the Bernays-Schönfinkel-Ramsey fragment with simple linear integer arithmetic. In Proceedings of the International Conference on Automated Deduction, pages 202-219, 2017. Google Scholar
  16. Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Aleksandar Nanevski, and Mooly Sagiv. Effectively-propositional reasoning about reachability in linked data structures. In International Conference on Computer Aided Verification, 2013. Google Scholar
  17. Susmit Jha, Sumit Gulwani, Sanjit A Seshia, and Ashish Tiwari. Oracle-guided component-based program synthesis. In Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering-Volume 1, pages 215-224. ACM, 2010. Google Scholar
  18. Deepak Kapur, Rupak Majumdar, and Calogero G. Zarba. Interpolation for data structures. In Proceedings of the 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering, SIGSOFT '06/FSE-14, pages 105-116, New York, NY, USA, 2006. ACM. URL: http://dx.doi.org/10.1145/1181775.1181789.
  19. Donald E Knuth. Textbook examples of recursion. Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy, 1991. Google Scholar
  20. Christof Löding, P. Madhusudan, and Lucas Peña. Foundations for natural proofs and quantifier instantiation. Proc. ACM Program. Lang., 2(POPL):10:1-10:30, 2017. URL: http://dx.doi.org/10.1145/3158098.
  21. Parthasarathy Madhusudan. Synthesizing Reactive Programs. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL, 2011. Google Scholar
  22. Zohar Manna and John McCarthy. Properties of programs and partial function logic. Technical report, Stanford University Computer Science Department, 1969. Google Scholar
  23. Greg Nelson and Derek C Oppen. Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems (TOPLAS), 1(2):245-257, 1979. Google Scholar
  24. Oded Padon, Kenneth L McMillan, Aurojit Panda, Mooly Sagiv, and Sharon Shoham. Ivy: safety verification by interactive generalization. ACM SIGPLAN Notices, 2016. Google Scholar
  25. Edgar Pek, Xiaokang Qiu, and Parthasarathy Madhusudan. Natural proofs for data structure manipulation in c using separation logic. In ACM SIGPLAN Notices, 2014. Google Scholar
  26. Ruzica Piskac, Leonardo de Moura, and Nikolaj Bjørner. Deciding effectively propositional logic with equality. Technical report, Technical Report MSR-TR-2008-181, Microsoft Research, 2008. Google Scholar
  27. Amir Pnueli, Yoav Rodeh, Ofer Strichman, and Michael Siegel. The small model property: How small can it be? Information and computation, 2002. Google Scholar
  28. Xiaokang Qiu, Pranav Garg, Andrei Ştefănescu, and Parthasarathy Madhusudan. Natural proofs for structure, data, and separation. ACM SIGPLAN Notices, 2013. Google Scholar
  29. Xiaokang Qiu and Armando Solar-Lezama. Natural synthesis of provably-correct data-structure manipulations. Proc. ACM Program. Lang., 1(OOPSLA):65:1-65:28, oct 2017. URL: http://dx.doi.org/10.1145/3133889.
  30. Michael O Rabin. Decidability of second-order theories and automata on infinite trees. Transactions of the american Mathematical Society, 1969. Google Scholar
  31. Viorica Sofronie-Stokkermans. Hierarchic reasoning in local theory extensions. In Robert Nieuwenhuis, editor, Automated Deduction - CADE-20, pages 219-234, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg. Google Scholar
  32. Viorica Sofronie-Stokkermans. On combinations of local theory extensions. In Programming Logics: Essays in Memory of Harald Ganzinger, pages 392-413, 2013. Google Scholar
  33. Armando Solar-Lezama, Liviu Tancau, Rastislav Bodik, Sanjit Seshia, and Vijay Saraswat. Combinatorial sketching for finite programs. ACM SIGOPS Operating Systems Review, 2006. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact