Reasoning About Cardinalities of Relations with Applications Supported by Proof Assistants
DOI10.1007/978-3-319-57418-9_18zbMath1486.68105OpenAlexW2608071279MaRDI QIDQ5283218
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
Specification and verification (program logics, model checking, etc.) (68Q60) Coloring of graphs and hypergraphs (05C15) Cylindric and polyadic algebras; relation algebras (03G15) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (1)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Cardinality of relations with applications
- Relation algebras
- Isabelle/HOL. A proof assistant for higher-order logic
- Cardinalities of Finite Relations in Coq
- Interacting with Modal Logics in the Coq Proof Assistant
- Tool-Based Verification of a Relational Vertex Coloring Program
- Reasoning About Cardinalities of Relations with Applications Supported by Proof Assistants
- Kleene Algebra with Tests and Coq Tools for while Programs
- On the Cardinality of Relations
- Cardinality of relations and relational approximation algorithms
This page was built for publication: Reasoning About Cardinalities of Relations with Applications Supported by Proof Assistants
