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)