=Paper=
{{Paper
|id=None
|storemode=property
|title=A Proof-checking Experiment on Representing Graphs as Membership Digraphs
|pdfUrl=https://ceur-ws.org/Vol-1068/paper-s01.pdf
|volume=Vol-1068
|dblpUrl=https://dblp.org/rec/conf/cilc/CalligarisOT13
}}
==A Proof-checking Experiment on Representing Graphs as Membership Digraphs==
https://ceur-ws.org/Vol-1068/paper-s01.pdf
A proof-checking experiment on
representing graphs as membership digraphs?
Pierpaolo Calligaris1 , Eugenio G. Omodeo2 , Alexandru I. Tomescu3
1
Università di Trieste (laureando),
email: frenkyo@gmail.com
2
Dipartimento di Matematica e Geoscienze, Università di Trieste,
Via Valerio 12/1, I-34127 – Trieste, Italy
email: eomodeo@units.it
3
Helsinki Institute for Information Technology HIIT,
Department of Computer Science, University of Helsinki,
P.O. 68 (Gustaf Hällströmin katu 2b), FI-00014 – Helsinki, Finland
email: tomescu@cs.helsinki.fi
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 orienta-
tion 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 Hamil-
tonian 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”
4
We call undirected graphs simply graphs, and directed graphs, digraphs.
228 Pierpaolo Calligaris, Eugenio G. Omodeo and Alexandru I. Tomescu
arcs reflect the membership relation. Under this change of perspective, a fully
formal reconstruction of those results became affordable and, once carried out,
was certified correct with the Ref proof-checker [3,4].
Can we, with equal ease, formalize in Ref the Milanič-Tomescu representation
result per se? That resultSis the claim that for every connected claw-free graph
G there exist a set νG ⊇ νG and an injection f from the vertices of G onto νG
such that {x, y} is an edge of G if and only if either f x ∈ f y or f y ∈ f x holds.
The proof articulates as follows:
1. One shows that for any graph G = (V, E) as said, there is a D ⊆ V × V
such that E = {x, y} : [x, y] ∈ D and (V, D) is an acyclic digraph which
is extensional: i.e., no two vertices in V have the same out-neighbors.
2. One decorates vertices by putting f v = {f w : [v, w] ∈ D} à la Mostowski,
for all v ∈ V . Acyclicity ensures that this recursion makes sense; extension-
ality ensures the injectivity of f .
As a preparatory, simpler formalization task, we have proved with Ref that
a graph G whatsoever admits a set νG and an injection f from the vertices of G
onto νG such that {x, y} is an edge of G if and only if either f x ∈ f y or
S fy ∈ fx
holds. We could not have insisted on the transitivity condition νG ⊇ νG here,
because we have nohow restrained G. The proof now articulates as follows:
10 . For any G = (V, E), there is a D ⊆ V × V s.t. E = {x, y} : [x, y] ∈ D
and (V, D) is an acyclic digraph which is weakly extensional: i.e., any
two vertices that share the same out-neighbors have no out-neighbors.
20 . We decorate vertices by putting: f v = {f w : [v, w] ∈ D } for each
v ∈ V endowed with out-neighbors, f z = ∅ for one sink z, and f u =
{V } ∪ V \ {u} for each sink u 6= z.
(Notice that 20 . subsumes 2. altogether, because an extensional digraph has
exactly one sink.)
2 Ingredients of a Ref’s scenario
What one submits to the Ref checker, to have its correctness verified, is a sce-
nario: namely, a script file consisting of definitions and of theorems endowed
with their proofs; a construct, named Theory , enables one to package def-
initions and theorems into reusable proofware components. A variant of the
Zermelo-Fraenkel set theory, postulating global choice, regularity, and infinity,
underlies the logical armory of Ref: this is apparent from the fifteen or so in-
ference rules available in the proof-specification language (see [5, Sec. 3]), of
which only a few sprout directly from first-order predicate calculus, while most
embody some form of set-theoretic reasoning. Multi-level syllogistic [1] acts as
a ubiquitous inference mechanism, while Theorys add a touch of second-order
reasoning ability to Ref’s overall machinery.
Our figures offer a glimpse of the Ref’s language. Fig. 1 shows the definitions
of graph-theoretic notions relevant to the proof-checking experiment on which
A proof-checking experiment on representing graphs as membership digraphs 229
Def acyclic: [Acyclicity] Acyclic(V, D) ↔Def
h∀w ⊆ V | w 6= ∅ → h∃t ∈ w | ∅ = {y ∈ w | [t, y] ∈ D} ii
Def xtens0 : [Extensionality] Extensional(V, D) ↔Def
h∀x ∈ V, y ∈ V, ∃z | ([x, z] ∈ D ↔ [y, z] ∈ D) → x = yi
Def xtens1 : [Weak extensionality] WExtensional(V,
D) ↔Def
Extensional V ∩ domain(D ∩ (V × V)), D ∩ (V × V)
Def orien: [Orientation of a graph] nn h E) ↔Def
o Orientates(D, V, io
E ∩ {{x, y} : x ∈ V, y ∈ V\ {x}} = p[1] , p[2] : p ∈ D | p = p[1] , p[2]
Def Finite : [Finitude] Finite(F) ↔Def
h∀g ∈ P(PF)\ {∅} , ∃m | g ∩ Pm = {m} i
Def maps5 : [Map predicate]
h i Is map(F) ↔Def
h∀p ∈ F | p = p[1] , p[2] i
Def maps6 : [Single-valued map] Svm(F) ↔Def
Is map(F) & h∀p ∈ F, q ∈ F | p[1] = q[1] → p = qi
Fig. 1. Four properties refer to digraphs, the other three to generic sets
Theorem part whole0 . Svm(F) → Finite(F) ↔ Finite(domain(F)) . Proof:
Suppose not(f1 ) ⇒ Auto
Suppose ⇒ Finite(f1 ) n o
APPLY h i finiteImage s0 7→ f1 , f(X) 7→ X[1] ⇒ Finite x[1] : x ∈ f1
Use def(domain) ⇒ false
Discharge ⇒ Auto
hf1 i,→T svm2 ⇒ f1 = {[x, f1 x] : x ∈ domain(f1 )}
APPLY h i finiteImage s0 7→ domain(f1 ), f(X) 7→ [x, f1 x] ⇒
Finite({[x, f1 x] : x ∈ domain(f1 )})
EQUAL ⇒ false
Discharge ⇒ Qed
Fig. 2. Example of a theorem proved in the Ref language
we report, and introduces finitude and the notion of mapping (‘Svm’).5 Fig. 2
5
To enforce a useful distinction, we denote by G(x) the application of a global function
G to an argument x (‘global’ meaning that the domain of G is the class of all sets),
while denoting by f x the application to x of a map f (typically single-valued),
viewed as set of pairs.
230 Pierpaolo Calligaris, Eugenio G. Omodeo and Alexandru I. Tomescu
shows the formal development of a proof, consisting of nine steps, each indicat-
ing which inference rule is employed to get the corresponding statement. This
proof invokes twice a Theory named finiteImage, whose interface is displayed in
Fig. 3. While finiteImage does not return any symbol, the other, subtler The-
ory displayed in the same figure, namely finiteInduction, returns a symbol, finΘ ,
representing an ⊆-minimal set which meets P—given that at least one finite
set satisfying property P exists. Likewise, the Theory finiteAcycLabeling shown
in Fig. 4 returns a labeling of a given acyclic digraph, thereby furnishing the
technique for decorating the graph à la Mostowski.
Theory finiteImage s0 , f(X) Theory finiteInduction s0 , P(S)
Finite(s0 ) Finite(s0 ) & P(s0 )
⇒ ⇒ (finΘ )
Finite {f(x) : x ∈ s0 } h∀S | S ⊆ finΘ → Finite(S) & P(S) ↔ S = finΘ i
End finiteImage End finiteInduction
Fig. 3. Interfaces of two Theorys regarding finitude
Theory finAcycLabeling v0 , d0 , h(s, x)
Acyclic(v0 , d0 ) & Finite(v0 )
⇒ (labΘ )
Svm(labΘ ) & domain(lab n Θ ) = v0 o
h∀x ∈ v0 | labΘ x = h labΘ p[2] : p ∈ d0|{x} | p[2] ∈ v0 , x i
End finAcycLabeling
Fig. 4. Interface of a Theory usable to label an acyclic digraph
3 Our experiment in a nutshell
The two Theorys in which our experiment culminates are shown in Fig. 5; the
key theorem which makes the second of them derivable from the first was stated
in Ref as follows:
Theorem weaXtensionalization0 . Finite(V) & S ∈ V →
h∃d | Orientates(d, V, E) & Acyclic(V, d) & WExtensional(V, d) & S ∈/ range(d)i.
Due to its centrality in our scenario, we wish to briefly sketch the proof of the
orientability theorem just cited. Arguing by contradiction, suppose that there
A proof-checking experiment on representing graphs as membership digraphs 231
Theory finMostowskiDecoration(v0 , d0 )
v0 × v0 ⊇ d0 & v0 6= ∅ & Finite(v0 ) & Acyclic(v0 , d0 ) & WExtensional(v0 , d0 )
⇒ (mskiΘ )
Svm(mskiΘ ) & domain(mskiΘ ) = v0 n o
h∀w | w ∈ domain(d0 ) → mskiΘ w = mskiΘ p[2] : p ∈ d0|{w} & mskiΘ w 6= ∅i
∅ ∈ range(mskiΘ ) & h∀y | y ∈ range(mskiΘ ) → Finite(y)i
h∀x, y | {x, y} ⊆ v0 & mskiΘ x = mskiΘ y → x = yi
h∀y | y ∈ v0 → (mskiΘ y ∈ mskiΘ x ↔ [x, y] ∈ d0 )i
End finMostowskiDecoration
Theory finGraphRepr(v0 , e0 )
e0 ⊆ {{x, y} : x ∈ v0 , y ∈ v0 \ {x}} & v0 6= ∅ & Finite(v0 )
⇒ (wskiΘ )
Svm(wskiΘ ) & domain(wskiΘ ) = v0 & ∅ ∈ range(wskiΘ )
h∀y | y ∈ range(wskiΘ ) → Finite(y)i
h∀x, y | {x, y} ⊆ v0 & wskiΘ x = wskiΘ y → x = yi
h∀x, y | {x, y} ⊆ v0 → (wskiΘ y ∈ wskiΘ x ∨ wskiΘ x ∈ wskiΘ y) ↔ {x, y} ∈ e0 i
h∀x | wskiΘ x ∩ range(wskiΘ ) 6= ∅ → wskiΘ x ⊆ range(wskiΘ )i
End finGraphRepr
Fig. 5. Theorys on Mostowski’s decoration and on graph representation
is a counterexample; then, exploiting the finiteness hypothesis, take a minimal
counterexample v1 , s1 , e0 . We are supposing that there is no acyclic, weakly
extensional orientation of the graph v1 , e0 ∩ {x, y} : x ∈ v1 , y ∈ v1\ {x}
having s1 as a source;whereas, for every v0 ( v1 , one can orient v0 , e0 ∩ {x, y} :
x ∈ v0 , y ∈ v0 \ {x} in an acyclic and weakly extensional way, for any vertex
t ∈ v0 , so that t plays the role of a source. Let, in particular, v0 = v1 \ {s0 }.
Unless s1 is an isolated vertex, an acyclic and weakly extensional orientation
of v0 exists that has as a source a chosen neighbor t1 of s1 . However, that
orientation could trivially be extended to the graph with vertices v1 so that s1
becomes a source; this contradiction shows that s1 cannot have neighbors in v1 ,
which is also untenable: if so, any orientation for v0 would in fact work also as
an orientation for v1 and, as such, would have s0 as a source.
The full Ref scenario can be seen at http://www2.units.it/eomodeo/wERS.
pdf (cf. also http://www2.units.it/eomodeo/ClawFreeness.html).
4 Planned work on representing claw-free graphs
The larger experiment we have in mind will associate with each connected claw-
free graph G = (V, E) an injection f from V onto a transitive, hereditarily finite
set νG so that {x, y} ∈ E if and only if either f x ∈ f y or f y ∈ f x.
232 Pierpaolo Calligaris, Eugenio G. Omodeo and Alexandru I. Tomescu
The new notions entering into play can be rendered formally as follows:
ClawFreeG(V, E) ↔Def h∀w, x, y, z | {w, x, y, z} ⊆ V & {{w, y} , {y, x} , {y, z}} ⊆ E →
(x = z ∨ w ∈ {z, x} ∨ {x, z} ∈ E ∨ {z, w} ∈ E ∨ {w, x} ∈ E)i ,
Connected(E) ↔ Def ∅ ∈
S /E∧
S S
h∀ p | p = E ∧ h∀b ∈ p, c ∈ p | b ∩ c 6= ∅ ↔ b = ci → p = {E}i ,
HerFin(S) ↔Def Finite(S) & h∀x ∈ S | HerFin(x)i .
Here, the first definiens requires that no subgraph of (V, E) induced by four
vertices has the shape of a ‘Y’. The second definiens requires that the set E of
edges can nohow be split into multiple disjoint blocks so that no edge acts as a
‘bridge’ by sharing endpoints with edges in distinct blocks. Hereditary finitude
is a recursive notion.
We aim at getting the analogue, shown in Fig. 6, of Theory finGraphRepr
(cf. Fig. 5). For that, we must again exploit Theory finMostowskiDecoration;
in addition, a key theorem will ensure the acyclic extensional orientability of a
connected and claw-free graph:
Theorem cClawFreeG2 . Finite(V) & Connected(V, E) &
ClawFreeG(V, E) & E ⊆ {{x, y} : x ∈ V, y ∈ V\ {x}} →
h∃d ⊆ V × V | Orientates(d, V, E) & Acyclic(V, d) & Extensional(V, d)i.
Theory herfinCCFGraphRepr(v0 , e0 )
e0 ⊆ {{x, y} : x ∈ v0 , y ∈ v0 \ {x}} & Finite(v0 )
Connected(v0 , e0 ) & ClawFreeG(v0 , e0 )
⇒ (transΘ )
Svm(transΘ ) & domain(transΘ ) = v0
h∀x, y | {X, Y} ⊆ v0 & transΘ X = transΘ Y → X = Yi
h∀x, y | {X, Y} ⊆ v0 →
(transΘ Y ∈ transΘ X ∨ transΘ X ∈ transΘ Y ↔ {X, Y} ∈ e0 )i
{y ∈ range(transΘ ) | y 6⊆ range(transΘ )} = ∅
range(transΘ ) 6= ∅ & HerFin(range(transΘ ))
End herfinCCFGraphRepr
Fig. 6. Theory on representing a connected claw-free graph via membership
Another fact we must exploit is that every connected graph has a vertex
whose removal (along with all edges incident to it) does not disrupt connectivity.
The existence of such a non-cut vertex is easily proved for a tree. So, in order
to cheaply achieve our goal, we will define
S
HankFree(T) ↔Def h∀e ⊆ T | e = ∅ ∨ h∃ a ∈ e | a 6⊆ (e \ {a})ii ,
Is tree(T) ↔Def Connected(T) ∧ HankFree(T)
A proof-checking experiment on representing graphs as membership digraphs 233
and—if only provisionally—recast the connectivity assumption, Connected(v0 , e0 ),
of Theory herfinCCFGraphRepr as the assumption that (v0 , e0 ) has a ‘spanning
tree’: S
h∃t | Is tree(t) & t = v0 & (v0 = {arb(v0 )} ∨ t ⊆ e0 )i .
This eases things: for, any vertex with fewer than 2 incident edges in the spanning
tree of a connected graph will be a non-cut vertex of the graph.
References
1. A. Ferro, E.G. Omodeo, and J.T. Schwartz. Decision procedures for elementary
sublanguages of set theory. I. Multi-level syllogistic and some extensions. Comm.
Pure Applied Math., 33(5):599–608, 1980.
2. M. Milanič and A. I. Tomescu. Set graphs. I. Hereditarily finite sets and extensional
acyclic orientations. Discrete Applied Mathematics, 161(4-5):677–690, 2013.
3. E. G. Omodeo. The Ref proof-checker and its “common shared scenario”. In Martin
Davis and Ed Schonberg, editors, From Linear Operators to Computational Biology:
Essays in Memory of Jacob T. Schwartz, pages 121–131. Springer, 2012.
4. E. G. Omodeo and A. I. Tomescu. Appendix: Claw-free graphs as sets. In Martin
Davis and Ed Schonberg, editors, From Linear Operators to Computational Biology:
Essays in Memory of Jacob T. Schwartz, pages 131–167. Springer, 2012.
5. E.G. Omodeo and A.I. Tomescu. Set graphs. III. Proof Pearl: Claw-free graphs
mirrored into transitive hereditarily finite sets. Journal of Automated Reasoning, In
press. DOI: 10.1007/s10817-012-9272-3.