2 papers
cs.LO2018
Convex Functions in ACL2(r)
Carl Kwan, Mark R. Greenstreet
This paper builds upon our prior formalisation of R^n in ACL2(r) by presenting a set of theorems for reasoning about convex functions. This is a demonstration of the higher-dimensi…
cs.LO2018
Real Vector Spaces and the Cauchy-Schwarz Inequality in ACL2(r)
Carl Kwan, Mark R. Greenstreet
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 formalisatio…