zbMATH — the first resource for mathematics

Relational characterisations of paths. (English) Zbl 1462.05198
Summary: Binary relations are one of the standard ways to encode, characterise and reason about graphs. Relation algebras provide equational axioms for a large fragment of the calculus of binary relations. Although relations are standard tools in many areas of mathematics and computing, researchers usually fall back to point-wise reasoning when it comes to arguments about paths in a graph. We present a purely algebraic way to specify different kinds of paths in Kleene relation algebras, which are relation algebras equipped with an operation for reflexive transitive closure. We study the relationship between paths with a designated root vertex and paths without such a vertex. Since we stay in first-order logic this development helps with mechanising proofs. To demonstrate the applicability of the algebraic framework we verify the correctness of three basic graph algorithms. All results of this paper are formally verified using the interactive proof assistant Isabelle/HOL.
05C38 Paths and cycles
03B35 Mechanization of proofs and logical operations
03G15 Cylindric and polyadic algebras; relation algebras
05C85 Graph algorithms (graph-theoretic aspects)
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
Full Text: DOI arXiv
[1] Armstrong, A.; Foster, S.; Struth, G.; Weber, T., Relation algebra (2014), Formal proof development
[2] Backhouse, R.; van den Eijnde, J. P.H. W.; van Gasteren, A. J.M., Calculating path algorithms, Sci. Comput. Program., 22, 3-19 (1994) · Zbl 0818.68117
[3] Backhouse, R. C.; Carré, B. A., Regular algebra applied to path-finding problems, J. Inst. Math. Appl., 15, 161-186 (1975) · Zbl 0304.68082
[4] Berge, C., The Theory of Graphs (2001), Dover Publications
[5] Berghammer, R., Combining relational calculus and the Dijkstra-Gries method for deriving relational programs, Inf. Sci., 119, 155-171 (1999) · Zbl 0943.68032
[6] Berghammer, R.; Danilenko, N.; Höfner, P.; Stucke, I., Cardinality of relations with applications, Discrete Math., 339, 3089-3115 (2016) · Zbl 1403.03132
[7] Berghammer, R.; Fischer, S., Combining relation algebra and data refinement to develop rectangle-based functional programs for reflexive-transitive closures, J. Log. Algebraic Methods Program., 84, 341-358 (2015) · Zbl 1329.68062
[8] Berghammer, R.; Hoffmann, T., Calculating a relational program for transitive reductions of strongly connected graphs, (de Swart, H., Relational Methods in Computer Science (RelMiCS 2001) (2001), Springer), 258-275 · Zbl 1027.68644
[9] Berghammer, R.; Hoffmann, T., Relational depth-first search with applications, Inf. Sci., 139, 167-186 (2001) · Zbl 1004.68125
[10] Berghammer, R.; Höfner, P.; Stucke, I., Automated verification of relational while-programs, (Höfner, P.; Jipsen, P.; Kahl, W.; Müller, M. E., Relational and Algebraic Methods in Computer Science (RAMiCS 2014) (2014), Springer), 173-190 · Zbl 1405.68070
[11] Berghammer, R.; Höfner, P.; Stucke, I., Tool-based verification of a relational vertex coloring program, (Kahl, W.; Oliveira, J. N.; Winter, M., Relational and Algebraic Methods in Computer Science (RAMiCS 2015) (2015), Springer), 275-292 · Zbl 1471.68054
[12] Berghammer, R.; Höfner, P.; Stucke, I., Cardinality of relations and relational approximation algorithms, J. Log. Algebraic Methods Program., 85, 269-286 (2016) · Zbl 1351.68152
[13] Berghammer, R.; Struth, G., On automated program construction and verification, (Bolduc, C.; Desharnais, J.; Ktari, B., Mathematics of Program Construction (MPC 2010) (2010), Springer), 22-41 · Zbl 1286.68068
[14] Bertot, Y.; Castéran, P., Interactive Theorem Proving and Program Development, Texts in Theoretical Computer Science (2004), Springer · Zbl 1069.68095
[15] Blanchette, J. C.; Böhme, S.; Paulson, L. C., Extending Sledgehammer with SMT solvers, J. Automat. Reason., 51, 109-128 (2013) · Zbl 1314.68272
[16] Cormen, T. H.; Leiserson, C. E.; Rivest, R. L., Introduction to Algorithms (1990), MIT Press · Zbl 1158.68538
[17] Crvenković, S.; Madarász, R. S., On Kleene algebras, Theor. Comput. Sci., 108, 17-24 (1993) · Zbl 0778.03006
[18] Dang, H. H.; Höfner, P., First-order theorem prover evaluation w.r.t. relation- and Kleene algebra, (Berghammer, R.; Möller, B.; Struth, G., Relations and Kleene Algebra in Computer Science: PhD Programme at RelMiCS10/AKA5 (2008), Institut für Informatik, Universität Augsburg), 48-52
[19] (de Swart, H.; Orłowska, E.; Schmidt, G.; Roubens, M., Theory and Applications of Relational Structures as Knowledge Instruments. Theory and Applications of Relational Structures as Knowledge Instruments, Lecture Notes in Computer Science, vol. 2929 (2003), Springer) · Zbl 1029.00017
[20] (de Swart, H.; Orłowska, E.; Schmidt, G.; Roubens, M., Theory and Applications of Relational Structures as Knowledge Instruments II. Theory and Applications of Relational Structures as Knowledge Instruments II, Lecture Notes in Computer Science, vol. 4342 (2006), Springer) · Zbl 1151.68001
[21] Desharnais, J.; Möller, B.; Struth, G., Algebraic notions of termination, Log. Methods Comput. Sci., 7, 1-29 (2011) · Zbl 1214.68185
[22] Diestel, R., Graph Theory (2005), Springer · Zbl 1074.05001
[23] Doornbos, H.; Backhouse, R.; van der Woude, J., A calculational approach to mathematical induction, Theor. Comput. Sci., 179, 103-135 (1997) · Zbl 0901.68124
[24] Foster, S.; Struth, G.; Weber, T., Automated engineering of relational and algebraic methods in Isabelle/HOL, (de Swart, H., Relational and Algebraic Methods in Computer Science (2011), Springer), 52-67 · Zbl 1329.68230
[25] Frias, M. F.; Aguayo, N.; Novak, B., Development of graph algorithms with fork algebras, (XIX Conferencia Latinoamericana de Informática (1993)), 529-554
[26] Glück, R., Algebraic investigation of connected components, (Höfner, P.; Pous, D.; Struth, G., Relational and Algebraic Methods in Computer Science (RAMiCS 2017) (2017), Springer), 109-126 · Zbl 06750818
[27] Guttmann, W., An algebraic approach to computations with progress, J. Log. Algebraic Methods Program., 85, 520-539 (2016) · Zbl 1344.68076
[28] Guttmann, W., An algebraic framework for minimum spanning tree problems, Theor. Comput. Sci., 744, 37-55 (2018) · Zbl 1401.68246
[29] Guttmann, W., Verifying minimum spanning tree algorithms with Stone relation algebras, J. Log. Algebraic Methods Program., 101, 132-150 (2018) · Zbl 1401.68247
[30] Guttmann, W.; Höfner, P., Relational characterisations of paths (2020), Formal proof development
[31] Harary, F., Graph Theory (1969), Addison-Wesley Publishing Company · Zbl 0182.57702
[32] Hirsch, R.; Hodkinson, I., Relation Algebras by Games, Studies in Logic and the Foundations of Mathematics, vol. 147 (2002), Elsevier Science B.V. · Zbl 1018.03002
[33] Hoare, C. A.R., An axiomatic basis for computer programming, Commun. ACM, 12, 576-580/583 (1969) · Zbl 0179.23105
[34] Höfner, P.; Struth, G., On automating the calculus of relations, (Armando, A.; Baumgartner, P.; Dowek, G., Automated Reasoning (IJCAR 2008) (2008), Springer), 50-66 · Zbl 1165.68460
[35] Huntington, E. V., Boolean algebra. A correction to: “New sets of independent postulates for the algebra of logic, with special reference to Whitehead and Russell”s Principia mathematica”, Trans. Am. Math. Soc., 35, 557-558 (1933)
[36] Huntington, E. V., New sets of independent postulates for the algebra of logic, Trans. Am. Math. Soc., 35, 274-304 (1933) · JFM 59.0050.06
[37] Jónsson, B.; Tarski, A., Boolean algebras with operators, part II, Am. J. Math., 74, 127-162 (1952) · Zbl 0045.31601
[38] Kahn, A. B., Topological sorting of large networks, Commun. ACM, 5, 558-562 (1962) · Zbl 0106.32602
[39] Kawahara, Y., On the cardinality of relations, (Schmidt, R. A., Relations and Kleene Algebra in Computer Science (2006), Springer), 251-265 · Zbl 1134.03318
[40] Kozen, D., A completeness theorem for Kleene algebras and the algebra of regular events, Inf. Comput., 110, 366-390 (1994) · Zbl 0806.68082
[41] MacCaull, W.; Orłowska, E., Correspondence results for relational proof systems with application to the Lambek calculus, Stud. Log., 71, 389-414 (2002) · Zbl 1020.03017
[42] Maddux, R., A sequent calculus for relation algebras, Ann. Pure Appl. Log., 25, 73-101 (1983) · Zbl 0528.03016
[43] Maddux, R.; Tarski, A., A sufficient condition for the representability of relation algebras, Not. Am. Math. Soc., 23, A-477 (1976)
[44] Maddux, R. D., Pair-dense relation algebras, Trans. Am. Math. Soc., 328, 83-131 (1991) · Zbl 0746.03055
[45] Maddux, R. D., Relation algebras, (Brink, C.; Kahl, W.; Schmidt, G., Relational Methods in Computer Science (1997), Springer), 22-38 · Zbl 0885.03047
[46] Maddux, R. D., Relation Algebras (2006), Elsevier · Zbl 1197.03051
[47] McCune, W., Prover9 and Mace4 (2005-2010)
[48] Meng, J.; Paulson, L. C., Translating higher-order clauses to first-order clauses, J. Automat. Reason., 40, 35-60 (2008) · Zbl 1203.68188
[49] Möller, B., Modal knowledge and game semirings, Comput. J., 56, 53-69 (2013)
[50] Möller, B.; Roocks, P.; Endres, M., An algebraic calculus of database preferences, (Gibbons, J.; Nogueira, P., Mathematics of Program Construction (2012), Springer), 241-262 · Zbl 1358.68087
[51] Müller, M. E., Relational Knowledge Discovery (2012), Cambridge University Press · Zbl 1267.68015
[52] Ng, K. C., Relation Algebras with Transitive Closure (1984), University of California: University of California Berkeley, Ph.D. thesis
[53] Nipkow, T., Winskel is (almost) right: towards a mechanized semantics textbook, Form. Asp. Comput., 10, 171-186 (1998) · Zbl 0910.68138
[54] Nipkow, T., Hoare logics in Isabelle/HOL, (Schwichtenberg, H.; Steinbrüggen, R., Proof and System-Reliability (2002), Kluwer Academic Publishers), 341-367 · Zbl 1097.68632
[55] Nipkow, T.; Paulson, L. C.; Wenzel, M., Isabelle/HOL: A Proof Assistant for Higher-Order Logic, Lecture Notes in Computer Science, vol. 2283 (2002), Springer · Zbl 0994.68131
[56] Okuma, H.; Kawahara, Y., Relational aspects of relational database dependencies, Bull. Inform. Cybern., 32, 91-104 (2000) · Zbl 1058.68049
[57] Paulson, L. C.; Blanchette, J. C., Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers, (Sutcliffe, G.; Schulz, S.; Ternovska, E., International Workshop on the Implementation of Logics (IWIL 2010), EasyChair (2010)), 1-11
[58] Pous, D., Automata for relation algebra and formal proofs (2016), ENS Lyon, Habilitation à diriger des recherches
[59] RelView, RelView system (1989-2016)
[60] Schmidt, G., Relational Mathematics (2010), Cambridge University Press
[61] Schmidt, G., Relational concepts in social choice, (Kahl, W.; Griffin, T., Relational and Algebraic Methods in Computer Science (2012), Springer), 278-293 · Zbl 1364.91051
[62] Schmidt, G.; Berghammer, R., Relational measures and integration in preference modeling, J. Log. Algebraic Program., 76, 112-129 (2008) · Zbl 1140.68495
[63] Schmidt, G.; Ströhlein, T., Relation algebras: concept of point and representability, Discrete Math., 54, 83-92 (1985) · Zbl 0575.03040
[64] Schmidt, G.; Ströhlein, T., Relations and Graphs: Discrete Mathematics for Computer Scientists (1993), Springer · Zbl 0900.68328
[65] Schulz, S., System description: E 1.8, (McMillan, K.; Middeldorp, A.; Voronkov, A., Logic for Programming Artificial Intelligence and Reasoning (LPAR 19) (2013), Springer), 735-743 · Zbl 1407.68442
[66] Scollo, G.; Franco, G.; Manca, V., A relational view of recurrence and attractors in state transition dynamics, (Schmidt, R. A., Relations and Kleene Algebra in Computer Science (2006), Springer), 358-372 · Zbl 1134.68461
[67] Tarski, A., On the calculus of relations, J. Symb. Log., 6, 73-89 (1941) · JFM 67.0973.02
[68] Tinhofer, G., Methoden der angewandten Graphentheorie (1976), Springer · Zbl 0338.05101
[69] Wenzel, M., Isar — a generic interpretative approach to readable formal proof documents, (Bertot, Y.; Dowek, G.; Théry, L.; Hirschowitz, A.; Paulin, C., Theorem Proving in Higher Order Logics (1999), Springer), 167-183
[70] Wenzel, M., Isabelle, Isar - A Versatile Environment for Human Readable Formal Proof Documents (2002), Technical University Munich: Technical University Munich Germany, Ph.D. thesis
[71] Wenzel, M., The Isabelle/Isar reference manual (2019)
[72] von Wright, J., Towards a refinement algebra, Sci. Comput. Program., 51, 23-45 (2004) · Zbl 1091.68030
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.