查看更多>>摘要：Abstract This paper describes the formalization of the prime number theorem with a remainder term in the Isabelle/HOL proof assistant. First, we formalized several lemmas in complex analysis that were not available in the library, such as the Borel–Carathéodory theorem and the factorization of an analytic function on a compact region. Then, we use these results to formalize a zero-free region of the Riemann zeta function with an explicitly computed constant and deduce the asymptotic growth order of ζ′(s)/ζ(s)\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\zeta '(s) / \zeta (s)$$\end{document} near Re(s)=1\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\textrm{Re}(s) = 1$$\end{document}. Finally, using a specific form of Perron’s formula, we prove the prime number theorem with the classical remainder term, expressed in terms of ψ(x)\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\psi (x)$$\end{document}. We also formalized the result that the prime number theorem stated using ψ(x)\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\psi (x)$$\end{document} can imply the version stated using π(x)\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\pi (x)$$\end{document}. Thus, we can achieve the main result of this paper. Our work extensively utilizes the rich libraries of complex analysis and asymptotic analysis in Isabelle/HOL, including concepts such as the winding number, the residue theorem, and proof automation tools such as the tactic. This is why we chose Isabelle to formalize analytic number theory instead of using other interactive provers.
查看更多>>摘要：Abstract The Lean mathematical library Mathlib features extensive use of the typeclass pattern for organising mathematical structures, based on Lean’s mechanism of instance parameters. Related mechanisms for typeclasses are available in other provers including Agda, Coq and Isabelle with varying degrees of adoption. This paper analyses representative examples of design patterns involving instance parameters in the finalized Lean 3 version of Mathlib, focussing on complications arising at scale and how the Mathlib community deals with them.
查看更多>>摘要：Abstract We provide a computer-assisted approach to ensure that a given discrete-time polynomial system is (asymptotically) stable. Our framework relies on constructive analysis together with formally certified sums of squares Lyapunov functions. The crucial steps are formalized within the proof assistant Minlog\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\texttt {Minlog}$$\end{document}. We illustrate our approach with an example issued from the control system literature.
查看更多>>摘要：Abstract For typical first-order logical theories, satisfying assignments have a straightforward finite representation that can directly serve as a certificate that a given assignment satisfies the given formula. For non-linear real arithmetic augmented with trigonometric and exponential functions (NTA\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathcal {N\hspace{-0.55542pt}T\hspace{-2.22214pt}A}$$\end{document}), however, there is no known direct representation of satisfying assignments that allows for a simple independent check of whether the represented numbers exist and satisfy the given formula. Hence, in this paper, we introduce a different form of satisfiability certificate for NTA\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathcal {N\hspace{-0.55542pt}T\hspace{-2.22214pt}A}$$\end{document}, and formulate the satisfiability problem as the problem of searching for such a certificate. This does not only ease the independent verification of satisfiability, but also allows the design of new algorithms that show satisfiability by systematically searching for such certificates. Computational experiments document that the resulting algorithms are able to prove satisfiability of a substantially higher number of benchmark problems than existing methods. We also characterize the formulas whose satisfiability can be demonstrated by such a certificate, by providing lower and upper bounds in terms of relevant well-known classes. Finally we show the existence of a procedure for checking the satisfiability of NTA\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathcal {N\hspace{-0.55542pt}T\hspace{-2.22214pt}A}$$\end{document}-formulas that terminates for formulas that satisfy certain robustness assumptions.
Ana de Almeida BorgesAnnalí Casanueva ArtísJean-Rémy FalleriEmilio Jesús Gallego Arias...
1.1-1.29页
查看更多>>摘要：Abstract The Coq Community Survey 2022 was an online public survey of users of the Coq proof assistant conducted during February 2022. Broadly, the survey asked about use of Coq features, user interfaces, libraries, plugins, and tools, views on renaming Coq and Coq improvements, and also demographic data such as education and experience with Coq and other proof assistants and programming languages. The survey received 466 submitted responses, making it the largest survey of users of an interactive theorem prover (ITP) so far. We present the design of the survey, a summary of key results, and analysis of answers relevant to ITP technology development and usage. In particular, we analyze user characteristics associated with adoption of tools and libraries and make comparisons to adjacent software communities. Notably, we find that experience has significant impact on Coq user behavior, including on usage of tools, libraries, and integrated development environments (IDEs).
查看更多>>摘要：Abstract The article Interpolation and SAT-Based Model Checking (McMillan in: Proc. CAV 2003, LNCS, Springer [56]) describes a formal-verification algorithm, which was originally devised to verify safety properties of finite-state transition systems. It derives interpolants from unsatisfiable BMC queries and collects them to construct an overapproximation of the set of reachable states. Although 20 years old, the algorithm is still state-of-the-art in hardware model checking. Unlike other formal-verification algorithms, such as or PDR, which have been extended to handle infinite-state systems and investigated for program analysis, McMillan’s interpolation-based model-checking algorithm from 2003 has not been used to verify programs so far. Our contribution is to close this significant, two decades old gap in knowledge by adopting the algorithm to software verification. We implemented it in the verification framework CPAchecker and evaluated the implementation against other state-of-the-art software-verification techniques on the largest publicly available benchmark suite of C safety-verification tasks. The evaluation demonstrates that McMillan’s interpolation-based model-checking algorithm from 2003 is competitive among other algorithms in terms of both the number of solved verification tasks and the run-time efficiency. Our results are important for the area of software verification, because researchers and developers now have one more approach to choose from.
Oskar AbrahamssonMagnus O. MyreenMichael NorrishHrutvik Kanabar...
1.1-1.40页
查看更多>>摘要：Abstract We add an efficient function for computation to the kernels of higher-order logic interactive theorem provers. First, we develop and prove sound our approach for Candle. Candle is a port of HOL Light which has been proved sound with respect to the inference rules of its higher-order logic; we extend its implementation and soundness proof. Second, we replicate our now-verified implementation for HOL4 with only minor changes, and build additional automation for ease of use. The automation exists outside of the HOL4 kernel, and requires no additional trust. We exercise our new computation function and associated automation on the evaluation of the CakeML compiler backend within HOL4’s logic, demonstrating an order of magnitude speedup. This is an extended version of our previous conference paper [2], which described implementation and soundness proofs for Candle. Our HOL4 implementation and automation are new, as are the CakeML benchmarks.
NETL
NSTL
Springer Nature