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

Usage statistics

Categories

• Information Systems

Keywords

Coq code Fixpoint Logics Interactive Theorem Proving Logic

Licence

4TU General Terms of Use

Export as...

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.

History

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

Publisher

TU Eindhoven

Format

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

References

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

Organizations

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