%0 Generic
%A Van Delft, M.E.C. (Myrthe)
%A Geuvers, J.H. (Herman)
%A Willemse, Tim
%D 2017
%T Coq formalisation of Consistent Consequence for Boolean Equation Systems
%U https://data.4tu.nl/articles/dataset/Coq_formalisation_of_Consistent_Consequence_for_Boolean_Equation_Systems/12709115/1
%R 10.4121/uuid:a06e90c7-9ca1-45df-ad37-e99bdbf75b78
%K Coq code
%K Fixpoint Logics
%K Interactive Theorem Proving
%K Logic
%X 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.
%I TU Eindhoven