Title
Automatic Proof of Graph Nonisomorphism.
Abstract
We describe automated methods for constructing nonisomorphism proofs for pairs of graphs. The proofs can be human-readable or machine-readable. We have developed a proof generator for graph nonisomorphism, which allows users to input graphs and construct a proof of (non)isomorphism. With the growth in computer power and internet access, an increasing number of prob- lems are solved on remote machines by programs written by experts in a particular field. In this situation, the user may have no knowledge of the algorithm used, its implementa- tion, or indeed how the remote machine is maintained. A mere yes-or-no answer cannot be trusted: we need additional verification that the answer is correct. For mathematical problems, the most obvious form of verification is a proof of correctness. In this article, we construct such proofs for the problem of graph isomorphism. If two graphs are isomorphic, and we are given an isomorphism, then it is easy to prove this by checking the isomorphism. Proving that a pair of graphs are not isomorphic is more dicult. We show how to generate such a proof automatically. Our proofs are
Year
DOI
Venue
2008
10.1007/s11786-008-0052-8
Mathematics in Computer Science
Keywords
Field
DocType
internet access,graph isomorphism
Discrete mathematics,Graph,Combinatorics,Graph isomorphism,Mathematical proof,Isomorphism,Zero-knowledge proof,Mathematics,Proof assistant
Journal
Volume
Issue
ISSN
2
2
1661-8289
Citations 
PageRank 
References 
0
0.34
11
Authors
3
Name
Order
Citations
PageRank
Arjeh M. Cohen17615.45
Jan Willem Knopper200.68
Scott H. Murray3143.13