Cardinalities of Finite Relations in Coq

DOI10.1007/978-3-319-43144-4_29MaRDI QIDQ2829280zbMATH OpenOpenAlexFDO

Authors Paul Brunet, Damien Pous, Insa Stucke

Publication date 27 October 2016

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-43144-4_29

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Ordinal and cardinal numbers (03E10) Cylindric and polyadic algebras; relation algebras (03G15) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Cardinality of relations with applications
• Finite-cofinite program relations
• On the Cardinality of Relations
• Reasoning about cardinalities of relations with applications supported by proof assistants
• scientific article; zbMATH DE number 495470
• Relational structures having finitely many full-cardinality restrictions
• scientific article; zbMATH DE number 404408
• Finite quantifier hierarchies in relational algebras
• Algebras of co-relations on a finite set

Cites work

• scientific article; zbMATH DE number 193143 (Why is no real title available?)
• scientific article; zbMATH DE number 234018 (Why is no real title available?)
• A new look at generalized rewriting in type theory
• Cardinalities of Finite Relations in Coq
• Dependently-typed formalisation of relation-algebraic abstractions
• Investigating and computing bipartitions with algebraic means
• Kleene algebra with tests and Coq tools for while programs
• On the Cardinality of Relations
• Relation algebras: Concept of points and representability
• Relational and Kleene-Algebraic Methods in Computer Science
• Residuated lattices. An algebraic glimpse at substructural logics
• Tool-Based Verification of a Relational Vertex Coloring Program

Cited in

(6)

• Cardinality of relations with applications
• Algebraic investigation of connected components
• Reasoning about cardinalities of relations with applications supported by proof assistants
• On the Cardinality of Relations
• Cardinality of relations and relational approximation algorithms
• Cardinalities of Finite Relations in Coq

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Cardinalities of Finite Relations in Coq

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2829280)