Reasoning About Cardinalities of Relations with Applications Supported by Proof Assistants

DOI10.1007/978-3-319-57418-9_18zbMath1486.68105OpenAlexW2608071279MaRDI QIDQ5283218

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

Mathematics Subject Classification ID

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)

Reasoning About Cardinalities of Relations with Applications Supported by Proof Assistants

Uses Software

• Coq
• Isabelle
• Isabelle/HOL
• HOL
• Archive Formal Proofs
• Relation Algebra

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