A graph G = (V, E) is word-representable if there exists a word w over V such that x and y alternate in w if and only if (x,y) is in E. A comprehensive introduction to the theory of word-representable graphs is given in the book "Words and Graphs" by Sergey Kitaev and Vadim Lozin published by

The user-friendly software

WordRepresentation.jar

to work with word-representability of graphs was created by Haoran Sun in 2021, and it is based on the notion of a semi-transitive orientation. A unique feature of this software, compared to that created by Marc Glen RepresentableGraphs.jar (see description here), is that it is capable of producing automatically human-verifiable proofs of non-word-representability (recognising word-representable graphs in an NP-complete poblem). We refer to the paper "Human-verifiable proofs in the theory of word-representable graphs" for a description of the

The software presents a graph in matrix form on the left, and in graphical form on the right. Edges are added/removed by clicking on the appropriate entry in the matrix. The program presents the following functionality:

Controls for manipulating the graph are on the left-hand side panel. There is an "oriented/non-oriented" pair of radio buttons, which toggles which type of edge is placed on the graph. A graph can be

The button "Test" checks whether the given fully-oriented graph is semi-transitively oriented, or whether the given partically orinted graph admits extension of the orientation to semi-transitive one, or whether the given undirected graph admits a semi-transitive orientation. "Test (Smart Version)" has the same functionality as "Test" but uses a more advanced algorithm (Algorithm 2 in the paper "Human-verifiable proofs in the theory of word-representable graphs"). If the graph in question is not word-representable, a pop out window will offer to print a proof of this fact. Such a proof can be used in a research paper to justify non-word-representability of a graph. The time used to find the proof will be printed at the end of the proof. We note that a proof of non-extendability of a partially oriented graph to a semi-transitively oriented graph is a useful feature: when strating from an undirected graph, one can notice symmetries allowing assumptions on orientation of certain edges without loss of generality. Such assumptions can allow finding a semi-transitive orientation quicker, or reduce the length of a non-word-representability proof dramatically.