(34.89 kB)

Coq formalisation of Consistent Consequence for Boolean Equation Systems

Download (34.89 kB)
posted on 27.06.2017, 00:00 by M.E.C. (Myrthe) Van Delft, J.H. (Herman) Geuvers, Tim Willemse
This data set contains a computer-checkable formal mathematical proof of the soundness and completeness of a proof system for the "consistent consequence" relation on Boolean equation systems, along with a formalisation of Boolean equation systems, the notion of solution and a formalisation of the relation between a solution of a Boolean equation system and a consistent consequence on such an equation system. The proofs can be machine-checked using the Coq proof assistant, version CoqIDE 8.5pl2; these proofs accompany the paper "A Formalisation of Consistent Consequence for Boolean Equation Systems" by Van Delft, Geuvers & Willemse that is part of the (forthcoming) proceedings of the 8th International Conference on Interactive Theorem Proving.



TU Eindhoven, Department of Mathematics and Computer Science, Section Model Driven Software Engineering (MDSE)


TU Eindhoven


media types: application/zip, text/plain, text/tab-separated-values


Logo branding