Reasoning about cardinalities of relations with applications supported by proof assistants

DOI10.1007/978-3-319-57418-9_18MaRDI QIDQ5283218zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

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)

Recommendations

• Cardinality of relations and relational approximation algorithms
• Cardinalities of Finite Relations in Coq
• Tool-Based Verification of a Relational Vertex Coloring Program
• Cardinality of relations with applications
• scientific article; zbMATH DE number 1927415

Cites work

• scientific article; zbMATH DE number 45228 (Why is no real title available?)
• scientific article; zbMATH DE number 234018 (Why is no real title available?)
• Cardinalities of Finite Relations in Coq
• Cardinality of relations and relational approximation algorithms
• Cardinality of relations with applications
• Interacting with Modal Logics in the Coq Proof Assistant
• Isabelle/HOL. A proof assistant for higher-order logic
• Kleene algebra with tests and Coq tools for while programs
• On the Cardinality of Relations
• Reasoning about cardinalities of relations with applications supported by proof assistants
• Relation algebras
• Tool-Based Verification of a Relational Vertex Coloring Program

Cited in

(4)

• How helpers hasten \(h\)-relations
• Reasoning about cardinalities of relations with applications supported by proof assistants
• Cardinality of relations and relational approximation algorithms
• Cardinalities of Finite Relations in Coq

Describes a project that uses

Uses Software

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

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)