data.zip (34.89 kB)

Coq formalisation of Consistent Consequence for Boolean Equation Systems

Download (34.89 kB)
dataset
posted on 27.06.2017 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.

History

Contributors

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

Publisher

TU Eindhoven

Format

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

Exports

Logo branding

Exports