Coq formalisation of Consistent Consequence for Boolean Equation Systems

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.