Resource map retrieved at 2019-04-21T06:26:10.32+02:00
2019-02-11T12:32:49.555Z
Coq formalisation of Consistent Consequence for Boolean Equation Systems
text/html
TU Eindhoven, Department of Mathematics and Computer Science, Section Model Driven Software Engineering (MDSE)
Van Delft, M.E.C. (Myrthe)
Geuvers, J.H. (Herman)
orcid:0000-0003-2522-2980
Willemse, T.A.C. (Tim)
orcid:0000-0003-3049-7962
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.
uuid:a06e90c7-9ca1-45df-ad37-e99bdbf75b78
en
TU Eindhoven
Coq code
Fixpoint Logics
Interactive Theorem Proving
Logic
Coq formalisation of Consistent Consequence for Boolean Equation Systems
2016-01-01 through 2017-04-10
2017-06-27
2017
Coq formalisation of Consistent Consequence for Boolean Equation Systems
2017-06-27T11:24:33.799Z
tsv=text/tab-separated-values v=text/plain
text/tab-separated-values
text/plain
application/zip
A formalisation of consistent consequence for boolean equation systems (ITP 2017)