conformlog

conformlog is a library for certification and reasoning about important inequalities, theorems and programs which arise in control theory. This framework was written in Minlog, an interactive proof system developed by Helmut Schwichtenberg and uses the Minlog's theory of constructive real analysis which aims for the certified program extraction. conformlog adds aditional theorems and extends the functionality of the base system. At the current stage we support:

• Coninuous multivariate and vector-valued functions and their correct approximations
• Certification of positive definite functions
• Lyapunov stability theorem for discrete-time systems

• Chez Scheme 9.5 or later
• Optional: text editor with integrated Terminal (i.e. Emacs or Visual Studio Code)

Computer-assisted proofs for Lyapunov stability via Sums of Squares certificates and Constructive Analysis (arXiv:2006.09884)

Formal proofs for Lyapunov stability theorems in exact real arithmetic (DOI)

Full library

• git clone https://github.com/acsd-tu-chemnitz/conformlog.git && cd conformlog
• "./install.sh"
• Run Minlog: "scheme init.scm"
• Load (minlog-load "./" "sys_as.scm")