cff-version: 1.2.0
abstract: "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."
authors:
  - family-names: Van Delft
    given-names: M.E.C. (Myrthe)
  - family-names: Geuvers
    given-names: J.H. (Herman)
    orcid: "https://orcid.org/0000-0003-2522-2980"
  - family-names: Willemse
    given-names: Tim
    orcid: "https://orcid.org/0000-0003-3049-7962"
title: "Coq formalisation of Consistent Consequence for Boolean Equation Systems"
keywords:
version: 1
identifiers:
  - type: doi
    value: 10.4121/uuid:a06e90c7-9ca1-45df-ad37-e99bdbf75b78
license: 4TU General Terms of Use
date-released: 2017-06-27