Document Open Access Logo

On Synthesizing Computable Skolem Functions for First Order Logic

Authors Supratik Chakraborty , S. Akshay

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2022.30.pdf
  • Filesize: 0.79 MB
  • 15 pages

Document Identifiers

Author Details

Supratik Chakraborty
  • Department of Computer Science and Engineering, IIT Bombay, India
S. Akshay
  • Department of Computer Science and Engineering, IIT Bombay, India

Cite AsGet BibTex

Supratik Chakraborty and S. Akshay. On Synthesizing Computable Skolem Functions for First Order Logic. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 30:1-30:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.MFCS.2022.30

Abstract

Skolem functions play a central role in the study of first order logic, both from theoretical and practical perspectives. While every Skolemized formula in first-order logic makes use of Skolem constants and/or functions, not all such Skolem constants and/or functions admit effectively computable interpretations. Indeed, the question of whether there exists an effectively computable interpretation of a Skolem function, and if so, how to automatically synthesize it, is fundamental to their use in several applications, such as planning, strategy synthesis, program synthesis etc. In this paper, we investigate the computability of Skolem functions and their automated synthesis in the full generality of first order logic. We first show a strong negative result, that even under mild assumptions on the vocabulary, it is impossible to obtain computable interpretations of Skolem functions. We then show a positive result, providing a precise characterization of first-order theories that admit effective interpretations of Skolem functions, and also present algorithms to automatically synthesize such interpretations. We discuss applications of our characterization as well as complexity bounds for Skolem functions (interpreted as Turing machines).

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Skolem functions
  • Automated
  • Synthesis
  • First order logic
  • Computability

Metrics

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

Related Versions

References

  1. S. Akshay, J. Arora, S. Chakraborty, S. Krishna, D. Raghunathan, and S. Shah. Knowledge compilation for Boolean functional synthesis. In Formal Methods in Computer Aided Design, FMCAD 2019, San Jose, CA, USA, pages 161-169. IEEE, 2019. Google Scholar
  2. S. Akshay and S. Chakraborty. On synthesizing Skolem functions for first order logic formulae. CoRR, abs/2102.07463, 2021. URL: http://arxiv.org/abs/2102.07463.
  3. S. Akshay, S. Chakraborty, S. Goel, S. Kulal, and S. Shah. What’s hard about Boolean functional synthesis? In Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I, volume 10981 of Lecture Notes in Computer Science, pages 251-269. Springer, 2018. Google Scholar
  4. S. Akshay, S. Chakraborty, S. Goel, S. Kulal, and S. Shah. Boolean functional synthesis: hardness and practical algorithms. Form Methods Syst Des., 57(1):53-86, 2021. Google Scholar
  5. S. Akshay, S. Chakraborty, A. K. John, and S. Shah. Towards parallel boolean functional synthesis. In TACAS 2017 Proceedings, Part I, pages 337-353, 2017. URL: https://doi.org/10.1007/978-3-662-54577-5_19.
  6. J. Avigad. Eliminating definitions and Skolem functions in first-order logic. ACM Trans. Comput. Log., 4(3):402-415, 2003. URL: https://doi.org/10.1145/772062.772068.
  7. M. Baaz, S. Hetzl, and D. Weller. On the complexity of proof deskolemization. J. Symb. Log., 77(2):669-686, 2012. URL: https://doi.org/10.2178/jsl/1333566645.
  8. L. Berman. The complexity of logical theories. Theoretical Computer Science, 11(1):71-77, 1980. URL: https://doi.org/10.1016/0304-3975(80)90037-7.
  9. E. Börger, E. Grädel, and Y. Gurevich. The Classical Decision Problem. Perspectives in Mathematical Logic. Springer, 1997. Google Scholar
  10. T. Dao and K. Djelloul. Solving first-order constraints in the theory of the evaluated trees. In Proceedings of the Constraint Solving and Contraint Logic Programming 11th Annual ERCIM International Conference on Recent Advances in Constraints, CSCLP'06, pages 108-123. Springer-Verlag, 2006. Google Scholar
  11. M. Davis, Y. Matijasevic, and J. Robinson. Hilbert’s tenth problem. Diophantine equations: positive aspects of a negative solution. In Proceedings of symposia in pure mathematics, volume 28, pages 323-378, 1976. Google Scholar
  12. K. Fazekas, M. J. H. Heule, M. Seidl, and A. Biere. Skolem function continuation for quantified Boolean formulas. In International Conference on Tests and Proofs (TAP), volume 10375 of Lecture Notes in Computer Science, pages 129-138. Springer, 2017. Google Scholar
  13. D. Fried, L. M. Tabajara, and M. Y. Vardi. BDD-based boolean functional synthesis. In Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II, pages 402-421, 2016. Google Scholar
  14. P. Golia, S. Roy, and K. S. Meel. Manthan: A data-driven approach for boolean function synthesis. In Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II, volume 12225 of Lecture Notes in Computer Science, pages 611-633. Springer, 2020. Google Scholar
  15. C. Haase. A survival guide to presburger arithmetic. ACM SIGLOG News, 5(3):67-82, 2018. Google Scholar
  16. M. Heule, M. Seidl, and A. Biere. Efficient Extraction of Skolem Functions from QRAT Proofs. In Formal Methods in Computer-Aided Design , FMCAD 2014, Lausanne, Switzerland, pages 107-114, 2014. Google Scholar
  17. J.-H. R. Jiang. Quantifier elimination via functional composition. In Proc. of CAV, pages 383-397. Springer, 2009. Google Scholar
  18. A. John, S. Shah, S. Chakraborty, A. Trivedi, and S. Akshay. Skolem functions for factored formulas. In Formal Methods in Computer-Aided Design, FMCAD 2015, pages 73-80, 2015. Google Scholar
  19. V. Kuncak, M. Mayer, R. Piskac, and P. Suter. Complete functional synthesis. In Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2010, Toronto, Ontario, Canada, June 5-10, 2010, pages 316-329. ACM, 2010. Google Scholar
  20. M. Preiner, A. Niemetz, and A. Biere. Counterexample-guided model synthesis. In TACAS (1), volume 10205 of Lecture Notes in Computer Science, pages 264-280, 2017. Google Scholar
  21. M. N. Rabe. Incremental determinization for quantifier elimination and functional synthesis. In Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II, pages 84-94, 2019. Google Scholar
  22. M. N. Rabe and S. A. Seshia. Incremental determinization. In Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings, pages 375-392, 2016. URL: https://doi.org/10.1007/978-3-319-40970-2_23.
  23. M. N. Rabe, L. Tentrup, C. Rasmussen, and S. A. Seshia. Understanding and extending incremental determinization for 2QBF. In Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part II, pages 256-274, 2018. Google Scholar
  24. Preey Shah, Aman Bansal, S. Akshay, and Supratik Chakraborty. A normal form characterization for efficient boolean skolem function synthesis. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, pages 1-13. IEEE, 2021. Google Scholar
  25. A. Spielmann and V. Kuncak. Synthesis for unbounded bit-vector arithmetic. In Automated Reasoning - 6th International Joint Conference, IJCAR 2012, Manchester, UK, June 26-29, 2012. Proceedings, volume 7364 of Lecture Notes in Computer Science, pages 499-513. Springer, 2012. Google Scholar
  26. S. Srivastava, S. Gulwani, and J. S. Foster. From program verification to program synthesis. SIGPLAN Not., 45(1):313-326, 2010. URL: https://doi.org/10.1145/1707801.1706337.
  27. L. M. Tabajara and M. Y. Vardi. Factored boolean functional synthesis. In Formal Methods in Computer Aided Design, FMCAD 2017, Vienna, Austria, October 2-6, 2017, pages 124-131, 2017. Google Scholar
  28. S. Verma and S. Roy. Debug-localize-repair: a symbiotic construction for heap manipulations. Formal Methods Syst. Des., 58(3):399-439, 2021. URL: https://doi.org/10.1007/s10703-021-00387-z.
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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact