Towards automated derivation in the theory of allegories
Joel Glanfield · 2008
2.1 Graphs representing the terms 1 n xxO and dom(x)....... 8 2.2 Sample graphs representing the basic graphs 1, 2x, and the operations gllg2, gIilg2, g-l and br(g) in PLIx. The corre-sponding terms are listed to the left of each graph...... 9 2.3 Sample terms in ALL with their respective graphs in PLlx.. 9 2.4 Normalization process of graphs representing terms in ALL 12 3.1 A I-arrow that is difficult to characterize........... 18 3.2 An example of generating the graph h*............ 20 3.3 Some embeddings that occur during the decision procedure (i.e. the solid arrows represent the embeddings, while i.pI,i.p2 represent compositions of I-arrows)................ 21 3.4 Some epimorphisms (e) and rnonomorphisms (m) that occur during the decision procedure that allow us to extract a deriva-tion mechanism........................... 22 3.5 A theoretical example of generating the graph h * where h * is not in PLlx............................. 26 3.6 A concrete example of generating the graph h * where h * is not