Cardinalities of Finite Relations in Coq

DOI10.1007/978-3-319-43144-4_29zbMath1478.68436OpenAlexW2500632430MaRDI QIDQ2829280

Insa Stucke, Damien Pous, Paul Brunet

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) Cylindric and polyadic algebras; relation algebras (03G15) Ordinal and cardinal numbers (03E10) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (3)

Algebraic Investigation of Connected Components ⋮ Reasoning About Cardinalities of Relations with Applications Supported by Proof Assistants ⋮ Cardinalities of Finite Relations in Coq

Uses Software

• Coq

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Residuated lattices. An algebraic glimpse at substructural logics
• Relation algebras: Concept of points and representability
• Cardinalities of Finite Relations in Coq
• Dependently-Typed Formalisation of Relation-Algebraic Abstractions
• Investigating and Computing Bipartitions with Algebraic Means
• Tool-Based Verification of a Relational Vertex Coloring Program
• Kleene Algebra with Tests and Coq Tools for while Programs
• On the Cardinality of Relations
• Relational and Kleene-Algebraic Methods in Computer Science

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