A Proof-checking Experiment on Representing Graphs as Membership Digraphs.
Pierpaolo Calligaris, Eugenio Giovanni Omodeo, Alexandru Ioan Tomescu · ArTS Archivio della ricerca di Trieste (University of Trieste https://www.units.it/) · 2013
Abstract. We developed, and computer-checked by means of the Ref verifier, a formal proof that every weakly extensional, acyclic (finite) digraph can be decorated injectively à la Mostowski by finite sets so that its arcs mimic membership. We managed to have one sink decorated with ∅ by this injection. We likewise proved that a graph whatsoever admits a weakly extensional and acyclic orientation; consequently, and in view of what precedes, one can regard its edges as membership arcs, each deprived of the direction assigned to it by the orientation. These results will be enhanced in a forthcoming scenario, where every connected claw-free graph G will receive an extensional acyclic orientation and will, through such an orientation, be represented as a transitive set T so that the membership arcs between members of T will correspond to the edges of G. Key words: Theory-based automated reasoning; proof checking; Referee aka ÆtnaNova; graphs and digraphs; Mostowski’s decoration. 1 Can graphs be represented as membership digraphs? One usually views the edges of a graph as vertex doubletons; 4 but various ways of representing graphs can be devised (as quickly surveyed in [5, Sec. 2]). Thanks to a convenient choice on how to represent connected claw-free graphs, Milanič and Tomescu [2] proved with relative ease two classical results on graphs of that kind, namely that any such graph owns a near-perfect matching and has a Hamiltonian cycle in its square. Those results are, in fact, legitimately transferred to a special class of digraphs, whose vertices are hereditarily finite sets and whose Work partially supported by the INdAM/GNCS 2013 project “Strumenti basati sulla teoria degli insiemi per la verifica di algoritmi”