Van Delft, M.E.C. (Myrthe); Geuvers, J.H. (Herman); Willemse, Tim (2017): Coq formalisation of Consistent Consequence for Boolean Equation Systems. Version 1. 4TU.ResearchData. dataset. https://doi.org/10.4121/uuid:a06e90c7-9ca1-45df-ad37-e99bdbf75b78

Dataset

• Information Systems

Coq code, Fixpoint Logics, Interactive Theorem Proving, Logic

4TU General Terms of Use

RefWorks, BibTeX, Reference Manager, Endnote, DataCite, NLM, DC, CFF

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.

• 2017-06-27 first online, published, posted

TU Eindhoven

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

• https://doi.org/10.1007/978-3-319-66107-0_29

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