Abstract
This paper describes a formal theory of undirected (labeled) graphs in higher-order logic developed using the mechanical theoremproving system HOL. It formalizes and proves theorems about such notions as the empty graph, single-node graphs, finite graphs, subgraphs, adjacency relations, walks, paths, cycles, bridges, reachability, connectedness, acyclicity, trees, trees oriented with respect to roots, oriented trees viewed as family trees, top-down and bottom-up inductions in a family tree, distributing associative and commutative operations with identities recursively over subtrees of a family tree, and merging disjoint subgraphs of a graph. The main contribution of this work lies in the precise formalization of these graph-theoretic notions and the rigorous derivation of their properties in higher-order logic. This is significant because there is little tradition of formalization in graph theory due to the concreteness of graphs. A companion paper [2] describes the application of this formal graph theory to the mechanical verification of distributed algorithms.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
N.G. de Bruijn, “Checking Mathematics with Computer Assistance”, in Notices of the American Mathematical Society, Vol. 38, No. 1, pp. 8–15, Jan. 1991.
Ching-Tsun Chou, “Mechanical Verification of Distributed Algorithms in Higher-Order Logic”, in this Proceedings.
Shimon Even, Graph Algorithms, Computer Science Press, 1979.
R.G. Gallager, P.A. Humblet, and P.M. Spira, “A Distributed Algorithm for Minimum-Weight Spanning Trees”, in ACM Trans. on Programming Languages and Systems, Vol. 5, No. 1, pp. 66–77, Jan. 1983.
Michael J.C. Gordon, “HOL: A Proof Generating System for Higher-Order Logic”, pp. 73–128 of G. Birtwistle and P.A. Subrahmanyam (ed.), VLSI Specification, Verification and Synthesis, Kluwer Academic Publishers, 1988.
Michael J.C. Gordon and Tom F. Melham (ed.), Introduction to HOL: A Theorem-Proving Environment for Higher-Order Logic, Cambridge University Press, 1993.
Tom F. Melham, The HOL pred_set Library, University of Cambridge Computer Laboratory, Feb. 1992.
Adrian Segall, “Distributed Network Protocols”, in IEEE Trans. on Information Theory, Vol. 29, No. 1, pp. 23–35, Jan. 1983.
Wai Wong, “A Simple Graph Theory and Its Application in Railway Signalling”, pp. 395–409 of M. Archer et al. (ed.), Proc. of 1991 Workshop on the HOL Theorem Proving System and Its Applications, IEEE Computer Society Press, 1992.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chou, CT. (1994). A formal theory of undirected graphs in higher-order logc. In: Melham, T.F., Camilleri, J. (eds) Higher Order Logic Theorem Proving and Its Applications. HUG 1994. Lecture Notes in Computer Science, vol 859. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58450-1_40
Download citation
DOI: https://doi.org/10.1007/3-540-58450-1_40
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58450-6
Online ISBN: 978-3-540-48803-3
eBook Packages: Springer Book Archive