3 papers
cs.LO2018
Smtlink 2.0
Yan Peng, Mark R. Greenstreet
Smtlink is an extension of ACL2 with Satisfiability Modulo Theories (SMT) solvers. We presented an earlier version at ACL2'2015. Smtlink 2.0 makes major improvements over the initi…
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…