Abstract
In this paper we prove the correctness of a program for computing vertex colorings in undirected graphs. In particular, we focus on the approximation ratio which is proved by using a cardinality operation for heterogeneous relations based on Y. Kawaharas characterisation.
All proofs are mechanised by using the two proof assistants Coq and Isabelle/HOL. Our Coq formalisation builds on existing libraries providing tools for heterogeneous relation algebras and cardinalities. To formalise the proofs in Isabelle/HOL we have to change over to untyped relations. Thus, we present an axiomatisation of a cardinality operation to reason about cardinalities algebraically also in homogeneous relation algebras and implement this new theoretical framework in Isabelle/HOL. Furthermore, we study the advantages and disadvantages of both systems in our context.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Berghammer, R., Danilenko, N., Höfner, P., Stucke, I.: Cardinality of relations with applications. Discret. Math. 339(12), 3089–3115 (2016)
Berghammer, R., Höfner, P., Stucke, I.: Tool-based verification of a relational vertex coloring program. In: Kahl, W., Winter, M., Oliveira, J.N. (eds.) RAMICS 2015. LNCS, vol. 9348, pp. 275–292. Springer, Cham (2015). doi:10.1007/978-3-319-24704-5_17
Berghammer, R., Höfner, P., Stucke, I.: Cardinality of relations and relational approximation algorithms. J. Log. Algebraic Methods Program. 85(2), 269–286 (2016)
Bertot, Y., Castéran, P., Huet, G., Paulin-Mohring, C.: Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of iInductive Constructions. Texts in Theoretical Computer Science. Springer, Heidelberg (2004)
Brunet, P., Pous, D., Stucke, I.: Cardinalities of finite relations in Coq. In: Blanchette, J.C., Merz, S. (eds.) ITP 2016. LNCS, vol. 9807, pp. 466–474. Springer, Cham (2016). doi:10.1007/978-3-319-43144-4_29
Freyd, P., Scedrov, A.: Categories, Allegories. Elsevier Science, Amsterdam (1990). North-Holland Mathematical Library
Furusawa, H.: Algebraic formalisations of fuzzy relations and their representation theorems. Ph.D. thesis, Department of Informatics, Kyushu University (1998)
Isabelle. https://isabelle.in.tum.de/
Kawahara, Y.: On the cardinality of relations. In: Schmidt, R.A. (ed.) RelMiCS 2006. LNCS, vol. 4136, pp. 251–265. Springer, Heidelberg (2006). doi:10.1007/11828563_17
Maddux, R.D.: Relation Algebras. Studies in Logic and the Foundations of Mathematics, vol. 150. Elsevier, Amsterdam (2006)
Nipkow, T.: Hoare logics in Isabelle/HOL. In: Schwichtenberg, H., Steinbrüggen, R. (eds.) Proof and System-Reliability, pp. 341–367. Kluwer, Dordrecht (2002)
Nipkow, T., Wenzel, M., Paulson, L.C.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)
Pous, D.: Relation Algebra and KAT in Coq. http://perso.ens-lyon.fr/damien.pous/ra/
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). doi:10.1007/978-3-642-39634-2_15
Schmidt, G.: Relational Mathematics, vol. 132. Cambridge University Press, Cambridge (2011). Encyclopedia of Mathematics and Its Applications
Schmidt, G., Ströhlein, T.: Relations and Graphs - Discrete Mathematics for Computer Scientists. EATCS Monographs on Theoretical Computer Science. Springer, Heidelberg (1993)
Struth, G., Weber, T.: Relation Algebra. Archive of Formal Proofs (2014). https://www.isa-afp.org/entries/Relation_Algebra.shtml
Stucke, I.: Reasoning about Cardinalities Supported by Proof Assistants, Proof Scripts. http://www.rpe.informatik.uni-kiel.de/en/Staff/ist/ramics-2017
Tarski, A.: On the calculus of relations. J. Symb. Log. 6(3), 73–89 (1941)
The Coq Proof Assistant. https://coq.inria.fr
Acknowledgement
I thank Walter Guttmann and Damien Pous for their help concerning the use of proof assistants and Rudolf Berghammer for helpful discussions and his support, in general. I thank the unknown referees and Michael Winter for their comments and suggestions which helped to improve the paper.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Appendix
Appendix
In this appendix we show that the third formula of the invariant is maintained stated in the following lemma.
Lemma
Let E, C and M be relations so that and
hold and p, q points with
,
. Then
holds.
Proof
Since holds, we have
and hence
The inclusion
is shown by the following calculation:
Furthermore, we have the following:
We now show that the inclusion above on the right-hand side is true where we use that p, q are points and thus again:
\(\square \)
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Stucke, I. (2017). Reasoning About Cardinalities of Relations with Applications Supported by Proof Assistants. In: Höfner, P., Pous, D., Struth, G. (eds) Relational and Algebraic Methods in Computer Science. RAMICS 2017. Lecture Notes in Computer Science(), vol 10226. Springer, Cham. https://doi.org/10.1007/978-3-319-57418-9_18
Download citation
DOI: https://doi.org/10.1007/978-3-319-57418-9_18
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-57417-2
Online ISBN: 978-3-319-57418-9
eBook Packages: Computer ScienceComputer Science (R0)