Reasoning about cardinalities of relations with applications supported by proof assistants
DOI10.1007/978-3-319-57418-9_18zbMATH Open1486.68105OpenAlexW2608071279MaRDI QIDQ5283218FDOQ5283218
Authors: Insa Stucke
Publication date: 21 July 2017
Published in: Relational and Algebraic Methods in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-57418-9_18
Recommendations
Coloring of graphs and hypergraphs (05C15) Specification and verification (program logics, model checking, etc.) (68Q60) Formalization of mathematics in connection with theorem provers (68V20) Cylindric and polyadic algebras; relation algebras (03G15) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Cites Work
- Isabelle/HOL. A proof assistant for higher-order logic
- Title not available (Why is that?)
- Title not available (Why is that?)
- Relation algebras
- Kleene algebra with tests and Coq tools for while programs
- On the Cardinality of Relations
- Interacting with Modal Logics in the Coq Proof Assistant
- Tool-Based Verification of a Relational Vertex Coloring Program
- Cardinality of relations and relational approximation algorithms
- Cardinality of relations with applications
- Reasoning about cardinalities of relations with applications supported by proof assistants
- Cardinalities of Finite Relations in Coq
Cited In (4)
Uses Software
This page was built for publication: Reasoning about cardinalities of relations with applications supported by proof assistants
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5283218)