TY - DATA
T1 - Coq formalisation of Consistent Consequence for Boolean Equation Systems
PY - 2017/06/27
AU - M.E.C. (Myrthe) Van Delft
AU - J.H. (Herman) Geuvers
AU - Tim Willemse
UR - https://data.4tu.nl/articles/dataset/Coq_formalisation_of_Consistent_Consequence_for_Boolean_Equation_Systems/12709115/1
DO - 10.4121/uuid:a06e90c7-9ca1-45df-ad37-e99bdbf75b78
KW - Coq code
KW - Fixpoint Logics
KW - Interactive Theorem Proving
KW - Logic
N2 - 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.
ER -