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 a` 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.

A proof-checking experiment on representing graphs as membership digraphs

OMODEO, EUGENIO;
2013-01-01

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 a` 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.
2013
http://ceur-ws.org/Vol-1068/paper-s01.pdf
https://nbn-resolving.org/resolver?identifier=urn:nbn:de:0074-1068-8
urn:nbn:de:0074-1068-8
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11368/2769411
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? ND
social impact