Document Open Access Logo

Deciding Predicate Logical Theories Of Real-Valued Functions

Author Stefan Ratschan

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2023.76.pdf
  • Filesize: 0.69 MB
  • 15 pages

Document Identifiers

Author Details

Stefan Ratschan
  • Institute of Computer Science of the Czech Academy of Sciences, Prague, Czech Republic

Funding

  • Ratschan, Stefan: This work was supported by the project 21-09458S of the Czech Science Foundation GA ČR and institutional support RVO:67985807.

Cite As Get BibTex

Stefan Ratschan. Deciding Predicate Logical Theories Of Real-Valued Functions. In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 76:1-76:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.MFCS.2023.76

Abstract

The notion of a real-valued function is central to mathematics, computer science, and many other scientific fields. Despite this importance, there are hardly any positive results on decision procedures for predicate logical theories that reason about real-valued functions. This paper defines a first-order predicate language for reasoning about multi-dimensional smooth real-valued functions and their derivatives, and demonstrates that - despite the obvious undecidability barriers - certain positive decidability results for such a language are indeed possible.

Subject Classification

ACM Subject Classification
  • Mathematics of computing → Continuous functions
  • Theory of computation → Automated reasoning
  • Theory of computation → Logic and verification
Keywords
  • decision procedures
  • first-order predicate logical theories
  • real numbers
  • real-valued functions

Metrics

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

Related Versions

References

  1. Charu C Aggarwal. Neural networks and deep learning. Springer, 10:978-3, 2018. Google Scholar
  2. Eugene Asarin and Ahmed Bouajjani. Perturbed Turing machines and hybrid systems. In Proc. LICS'01, pages 269-278, 2001. Google Scholar
  3. Clark Barrett and Cesare Tinelli. Satisfiability modulo theories. In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking. Springer International Publishing, 2018. Google Scholar
  4. Olivier Bournez and Manuel L. Campagnolo. A survey on continuous time computations. In S.Barry Cooper, Benedikt Löwe, and Andrea Sorbi, editors, New Computational Paradigms, pages 383-423. Springer New York, 2008. Google Scholar
  5. Olivier Bournez and Amaury Pouly. Handbook of Computability and Complexity in Analysis, chapter A Survey on Analog Models of Computation, pages 173-226. Springer, 2018. Google Scholar
  6. Aaron Bradley and Zohar Manna. The Calculus of Computation. Springer, 2007. Google Scholar
  7. Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, and Roberto Sebastiani. Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions. ACM Transactions on Computational Logic (TOCL), 19(3):1-52, 2018. Google Scholar
  8. Pieter Collins and Daniel Silva Graça. Effective computability of solutions of differential inclusions the ten thousand monkeys approach. J. Univers. Comput. Sci., 15(6):1162-1185, 2009. Google Scholar
  9. Pieter Collins, Milad Niqui, and Nathalie Revol. A validated real function calculus. Mathematics in Computer Science, 5(4):437-467, 2011. Google Scholar
  10. Laurent Doyen, Goran Frehse, George J. Pappas, and André Platzer. Verification of hybrid systems. In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking. Springer International Publishing, 2018. Google Scholar
  11. T. A. Driscoll, N. Hale, and L. N. Trefethen. Chebfun guide. Pafnuty Publications, Oxford, 2014. Google Scholar
  12. Andreas Eggers, Martin Fränzle, and Christian Herde. SAT modulo ODE: A direct SAT approach to hybrid systems. In Automated Technology for Verification and Analysis, volume 5311 of LNCS, 2008. Google Scholar
  13. Gerald Farin. Curves and Surfaces for Computer Aided Geometric Design - A Practical Guide. Academic Press, 1988. Google Scholar
  14. Charles Fefferman and Arie Israel. Fitting Smooth Functions to Data. AMS, 2020. Google Scholar
  15. Simon Foster, Jonathan Julián Huerta y Munive, Mario Gleirscher, and Georg Struth. Hybrid systems verification with Isabelle/HOL: Simpler syntax, better models, faster proofs. In International Symposium on Formal Methods, pages 367-386. Springer, 2021. Google Scholar
  16. Martin Fränzle. Analysis of hybrid systems: An ounce of realism can save an infinity of states. In J. Flum and M. Rodriguez-Artalejo, editors, Computer Science Logic (CSL'99), number 1683 in LNCS. Springer, 1999. Google Scholar
  17. Sicun Gao, Jeremy Avigad, and Edmund Clarke. δ-decidability over the reals. In LICS, pages 305-314. IEEE, 2012. Google Scholar
  18. Sicun Gao, Soonho Kong, and Edmund M Clarke. Satisfiability modulo ODEs. In 2013 Formal Methods in Computer-Aided Design, pages 105-112. IEEE, 2013. Google Scholar
  19. Ernst Hairer, Syvert Paul Nørsett, and Gerhard Wanner. Solving Ordinary Differential Equations I. Springer-Verlag, 1987. Google Scholar
  20. Hyejin Han, Mohamed Maghenem, and Ricardo G. Sanfelice. Certifying the LTL formula p until q in hybrid systems. IEEE Transactions on Automatic Control, 68(7), 2023. Google Scholar
  21. Timothy J. Hickey. Analytic constraint solving and interval arithmetic. In Proc. of the 27th ACM SIGACT-SIGPLAN Symp. on Principles of Progr. Lang., pages 338-351. ACM Press, 2000. Google Scholar
  22. Hassan K. Khalil. Nonlinear Systems. Prentice Hall, 3rd edition, 2002. Google Scholar
  23. Ker-I Ko. Computational complexity of real functions. In Complexity Theory of Real Functions, Progress in Theoretical Computer Science, pages 40-70. Birkhäuser Boston, 1991. Google Scholar
  24. Peter D. Lax. Functional Analysis. Wiley-Interscience, 2002. Google Scholar
  25. Angus Macintyre and A.J. Wilkie. On the decidability of the real exponential field. In Piergiorgie Odifreddi, editor, Kreiseliana - About and Around Georg Kreisel, pages 441-467. A K Peters, 1996. Google Scholar
  26. Raghavan Narasimhan. Analysis on Real and Complex Manifolds. Elsevier, 2nd edition edition, 1973. Google Scholar
  27. Greg Nelson and Derek C. Oppen. Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst., 1(2):245-257, 1979. Google Scholar
  28. Greg Nelson and Derek C. Oppen. Fast decision procedures based on congruence closure. J. ACM, 27(2):356-364, April 1980. Google Scholar
  29. André Platzer. Logical Foundations of Cyber-Physical Systems, volume 662. Springer, 2018. Google Scholar
  30. Stephen Prajna and Ali Jadbabaie. Safety verification of hybrid systems using barrier certificates. In Rajeev Alur and George J. Pappas, editors, HSCC'04, number 2993 in LNCS. Springer, 2004. Google Scholar
  31. Stephen Prajna and Anders Rantzer. Convex programs for temporal verification of nonlinear dynamical systems. SIAM Journal on Control and Optimization, 46(3):999-1021, 2007. Google Scholar
  32. Stefan Ratschan. Continuous first-order constraint satisfaction. In J. Calmet, B. Benhamou, O. Caprotti, L. Henocque, and V. Sorge, editors, Artificial Intelligence, Automated Reasoning, and Symbolic Computation, number 2385 in LNCS, pages 181-195. Springer, 2002. Google Scholar
  33. Stefan Ratschan. Quantified constraints under perturbations. Journal of Symbolic Computation, 33(4):493-505, 2002. Google Scholar
  34. Stefan Ratschan. Simulation based computation of certificates for safety of dynamical systems. In Alessandro Abate and Gilles Geeraerts, editors, Formal Modeling and Analysis of Timed Systems: 15th International Conference, FORMATS 2017, volume 10419, pages 303-317. Springer International Publishing, 2017. Google Scholar
  35. Hadi Ravanbakhsh and Sriram Sankaranarayanan. Learning control Lyapunov functions from counterexamples and demonstrations. Autonomous Robots, pages 1-33, 2018. Google Scholar
  36. Junuthula Narasimha Reddy. Introduction to the Finite Element Method. McGraw-Hill Education, 2019. Google Scholar
  37. Robert M Solovay, RD Arthan, and John Harrison. Some new results on decidability for elementary algebra and geometry. Annals of Pure and Applied Logic, 163(12):1765-1802, 2012. Google Scholar
  38. A. Tarski. A Decision Method for Elementary Algebra and Geometry. Univ. of California Press, Berkeley, 1951. Google Scholar
  39. Cesare Tinelli and Mehdi Harandi. A new correctness proof of the Nelson-Oppen combination procedure. In Frontiers of Combining Systems, pages 103-119. Springer, 1996. Google Scholar
  40. A. Yu. Veretennikov and E. V. Veretennikova. On partial derivatives of multivariate Bernstein polynomials. Siberian Advances in Mathematics, 26(4):294-305, 2016. Google Scholar
  41. Joachim von zur Gathen and Jürgen Gerhard. Modern Computer Algebra. Cambridge University Press, 2003. 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-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact