×

Cardinalities of finite relations in Coq. (English) Zbl 1478.68436

Blanchette, Jasmin Christian (ed.) et al., Interactive theorem proving. 7th international conference, ITP 2016, Nancy, France, August 22–25, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9807, 466-474 (2016).
Summary: We present an extension of a Coq library for relation algebras, where we provide support for cardinals in a point-free way. This makes it possible to reason purely algebraically, which is well-suited for mechanisation. We discuss several applications in the area of graph theory and program verification.
For the entire collection see [Zbl 1343.68004].

MSC:

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

Software:

Coq
PDFBibTeX XMLCite
Full Text: DOI HAL

References:

[1] Berghammer, R., Höfner, P., Stucke, I.: Tool-based verification of a relational vertex coloring program. In: Kahl, W., Winter, M., Oliveira, J. (eds.) RAMiCS 2015. LNCS, vol. 9348, pp. 275–292. Springer, Heidelberg (2015). doi: 10.1007/978-3-319-24704-5_17 · Zbl 1471.68054 · doi:10.1007/978-3-319-24704-5_17
[2] Berghammer, R., Stucke, I., Winter, M.: Investigating and computing bipartitions with algebraic means. In: Kahl, W., Winter, M., Oliveira, J. (eds.) RAMiCS 2015. LNCS, vol. 9348, pp. 257–274. Springer, Heidelberg (2015). doi: 10.1007/978-3-319-24704-5_16 · Zbl 1471.08001 · doi:10.1007/978-3-319-24704-5_16
[3] Brunet, P., Pous, D., Stucke, I.: Cardinalities of relations in Coq. Coq Development and full version of this extended abstract (2016). http://media.informatik.uni-kiel.de/cardinal/ · Zbl 1478.68436
[4] Furusawa, H.: Algebraic formalisations of fuzzy relations and their representation theorems. Ph.D. thesis, Department of Informatics, Kyushu University (1998)
[5] Galatos, N., Jipsen, P., Kowalski, T., Ono, H., Lattices, R.: An Algebraic Glimpse at Substructural Logics. Elsevier, Oxford (2007) · Zbl 1171.03001
[6] Kahl, W.: Calculational relation-algebraic proofs in Isabelle/Isar. In: Berghammer, R., Möller, B., Struth, G. (eds.) RelMiCS 2003. LNCS, vol. 3051, pp. 178–190. Springer, Heidelberg (2004) · Zbl 1088.68772
[7] Kahl, W.: Dependently-typed formalisation of relation-algebraic abstractions. In: de Swart, H. (ed.) RAMICS 2011. LNCS, vol. 6663, pp. 230–247. Springer, Heidelberg (2011) · Zbl 1329.68063 · doi:10.1007/978-3-642-21070-9_18
[8] Kawahara, Y.: On the cardinality of relations. In: Schmidt, R.A. (ed.) RelMiCS/AKA 2006. LNCS, vol. 4136, pp. 251–265. Springer, Heidelberg (2006) · Zbl 1134.03318 · doi:10.1007/11828563_17
[9] Pous, D.: Relation Algebra and KAT in Coq. http://perso.ens-lyon.fr/damien.pous/ra/ · Zbl 1317.68229
[10] Pous, D.: Kleene algebra with tests and coq tools for while programs. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 180–196. Springer, Heidelberg (2013) · Zbl 1317.68229 · doi:10.1007/978-3-642-39634-2_15
[11] Schmidt, G., Ströhlein, T.: Relation algebras: concept of points and representability. Discrete Math. 54(1), 83–92 (1985) · Zbl 0575.03040 · doi:10.1016/0012-365X(85)90064-0
[12] Schmidt, G., Ströhlein, T.: Relations and Graphs - Discrete Mathematics for Computer Scientists. EATCS Monographs on Theoretical Computer Science. Springer, Berlin (1993) · Zbl 0900.68328
[13] Sozeau, M.: A new look at generalized rewriting in type theory. J. Formalized Reason. 2(1), 41–62 (2009) · Zbl 1205.68364
[14] Tarski, A.: On the calculus of relations. J. Symbolic Log. 6(3), 73–89 (1941) · JFM 67.0973.02 · doi:10.2307/2268577
[15] Tarski, A., Givant, S.: A Formalization of Set Theory without Variables, vol. 41. Colloquium Publications, AMS, Providence, Rhode Island (1987) · Zbl 0654.03036 · doi:10.1090/coll/041
[16] Wei, V.: A lower bound for the stability number of a simple graph. Bell Laboratories Technical Memorandum 81–11217-9 (1981)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.