相关论文: ACL2 Proofs of Nonlinear Inequalities with Imandra

Using an interactive theorem prover to reason about programs involves a sequence of interactions where the user challenges the theorem prover with conjectures. Invariably, many of the conjectures posed are in fact false, and users often…

We describe Imandra, a modern computational logic theorem prover designed to bridge the gap between decision procedures such as SMT, semi-automatic inductive provers of the Boyer-Moore family like ACL2, and interactive proof assistants for…

ACL2(r) is a variant of ACL2 that supports the irrational real and complex numbers. Its logical foundation is based on internal set theory (IST), an axiomatic formalization of non-standard analysis (NSA). Familiar ideas from analysis, such…

ACL2(ml) is an extension for the Emacs interface of ACL2. This tool uses machine-learning to help the ACL2 user during the proof-development. Namely, ACL2(ml) gives hints to the user in the form of families of similar theorems, and…

We present a novel technique for combining statistical machine learning for proof-pattern recognition with symbolic methods for lemma discovery. The resulting tool, ACL2(ml), gathers proof statistics and uses statistical pattern-recognition…

In this paper we give alternate proofs of some well-known matrix inequalities. In particular, we show that under certain conditions the inequality holds \begin{align}\sum \limits_{\lambda_i\in \mathrm{Spec}(ab^{T})}\mathrm{min}\{\log…

We present a mechanical proof of the Cauchy-Schwarz inequality in ACL2(r) and a formalisation of the necessary mathematics to undertake such a proof. This includes the formalisation of $\mathbb{R}^n$ as an inner product space. We also…

Newcomers to ACL2 are sometimes surprised that ACL2 rejects formulas that they believe should be theorems, such as (REVERSE (REVERSE X)) = X. Experienced ACL2 users will recognize that the theorem only holds for intended values of X, and…

Nonlinear interpolants have been shown useful for the verification of programs and hybrid systems in contexts of theorem proving, model checking, abstract interpretation, etc. The underlying synthesis problem, however, is challenging and…

ACL2 was used to prove properties of two simplification procedures. The procedures differ in complexity but solve the same programming problem that arises in the context of a resolution/paramodulation theorem proving system. Term rewriting…

We present our extension of ACL2 with Satisfiability Modulo Theories (SMT) solvers using ACL2's trusted clause processor mechanism. We are particularly interested in the verification of physical systems including Analog and Mixed-Signal…

We examine the convergence properties of sequences of nonnegative real numbers that satisfy a particular class of recursive inequalities, from the perspective of proof theory and computability theory. We first establish a number of results…

Indexed Linear Logic has been introduced by Ehrhard and Bucciarelli, it can be seen as a logical presentation of non-idempotent intersection types extended through the relational semantics to the full linear logic. We introduce an…

When verifying computer systems we sometimes want to study their asymptotic behaviors, i.e., how they behave in the long run. In such cases, we need real analysis, the area of mathematics that deals with limits and the foundations of…

We show that moment inequalities in a wide variety of economic applications have a particular linear conditional structure. We use this structure to construct uniformly valid confidence sets that remain computationally tractable even in…

Being motivated by the problem of deducing $L^p$-bounds on the second fundamental form of an isometric immersion from $L^p$-bounds on its mean curvature vector field, we prove a (nonlinear) Calder\'on-Zygmund inequality for maps between…

This article investigates the convergence properties of a relative-type inexact preconditioned proximal augmented Lagrangian method (rip$^2$ALM) for convex nonlinear programming, a fundamental class of optimization problems with broad…

We discuss here some computational aspects of the Combinatorial Nullstellensatz argument. Our main result shows that the order of magnitude of the symmetry group associated with permutations of the variables in algebraic constraints,…

ACL2 has long supported user-defined simplifiers, so-called metafunctions and clause processors, which are installed when corresponding rules of class :meta or :clause-processor are proved. Historically, such simplifiers could access the…

We present a new approach to verifying contraction and $L_2$-gain of uncertain nonlinear systems, extending the well-known method of integral quadratic constraints. The uncertain system consists of a feedback interconnection of a nonlinear…