The central aims of this workgroup consist in providing an interdisciplinary forum for exploring the diverse aspects of applied category theory relevant in graph transformation systems and their generalizations, in developing a methodology for formalizing diagrammatic proofs as relevant in rewriting theories via proof assistants such as Coq, and in establishing a community-driven wiki system and repository for mathematical knowledge in our research field (akin to a domain-specific Coq-enabled variant of the nLab). A further research question will explore the possibility of deriving reference prototype implementations of concrete rewriting systems (e.g., over multi- or simple directed graphs) directly from the category-theoretical semantics, in the spirit of the translation-based approaches (utilizing theorem provers such as Microsoft Z3).
SMTCoq is a tool to make the Coq proof assistant and SMT solvers cooperate, with the same degree of confidence as Coq. In this talk, I will give an overview of its potential:
An API to build first-order SMTCoq terms and formulas is also under progress, in order to have an easy access to …