Open Collections

Automated reasoning in first-order real vector spaces

University of British Columbia

We present a formal first-order theory of arbitrary dimensional real vector spaces in ACL2(r). This includes methods for reasoning about real vectors, metric spaces, continuity, and multivariate convex functions, which, by necessity, involves the formalisation of a selection of classically significant and useful mathematical theorems. Notable formalisations include the first mechanical proof of the Cauchy-Schwarz inequality in a first-order logic and a theorem attributed to Yurii Nesterov for characterising convex functions with Lipschitz continuous gradients. One motivation for this work is to further contribute to the automated deduction of theorems involving such mathematical objects. Another motivation is the potential applications in the verification of analog circuits, cyberphysical systems, and machine learning algorithms. Indeed, common techniques in these areas involve reasoning about the algebraic properties of higher dimensional structures over the reals or the extremal values, monotonicity, and convexity properties of functions over these structures. These applications, along with Nesterov's theorem, demonstrate that our formalisation serves as a useful foundation in the space of reasoning and verification research.

Text

2019-08-26

Attribution-NonCommercial-NoDerivatives 4.0 International

http://hdl.handle.net/2429/71452

Computer Science

University of British Columbia

UBCV

http://creativecommons.org/licenses/by-nc-nd/4.0/