diff --git a/ontologies/graphs/conversions/P3covered.in b/ontologies/graphs/conversions/P3covered.in new file mode 100644 index 00000000..80ba86e4 --- /dev/null +++ b/ontologies/graphs/conversions/P3covered.in @@ -0,0 +1,5 @@ +formulas(sos). +(all x all y ((all z (adj(x,z) <-> adj(y,z))) -> =(x,y))). +(all x adj(x,x)). +(all x all y (adj(x,y) -> adj(y,x))). +end_of_list. diff --git a/ontologies/graphs/conversions/bipartite_graph.in b/ontologies/graphs/conversions/bipartite_graph.in new file mode 100644 index 00000000..083db55a --- /dev/null +++ b/ontologies/graphs/conversions/bipartite_graph.in @@ -0,0 +1,6 @@ +formulas(sos). +(all x all y (cycle(x,y) -> even_cycle(x,y))). +(all x -(adj(x,x))). +(all x all y (adj(x,y) -> adj(y,x))). +(all x -(adj(x,x))). +end_of_list. diff --git a/ontologies/graphs/conversions/chordal_graph.in b/ontologies/graphs/conversions/chordal_graph.in new file mode 100644 index 00000000..39f82b4a --- /dev/null +++ b/ontologies/graphs/conversions/chordal_graph.in @@ -0,0 +1,6 @@ +formulas(sos). +(all x all y all z all w (cycle(x,y,z,w) -> (exists u exists v (path(x,u,w) & path(x,v,w) & adj(u,v))))). +(all x -(adj(x,x))). +(all x all y (adj(x,y) -> adj(y,x))). +(all x -(adj(x,x))). +end_of_list. diff --git a/ontologies/graphs/conversions/cograph.in b/ontologies/graphs/conversions/cograph.in new file mode 100644 index 00000000..bbfc6ef2 --- /dev/null +++ b/ontologies/graphs/conversions/cograph.in @@ -0,0 +1,5 @@ +formulas(sos). +(all x all y all z all w ((adj(x,y) & adj(y,z) & adj(z,w)) -> (adj(x,z) | adj(x,w) | adj(y,w)))). +(all x -(adj(x,x))). +(all x all y (adj(x,y) -> adj(y,x))). +end_of_list. diff --git a/ontologies/graphs/conversions/comparability_graph.in b/ontologies/graphs/conversions/comparability_graph.in new file mode 100644 index 00000000..987bff97 --- /dev/null +++ b/ontologies/graphs/conversions/comparability_graph.in @@ -0,0 +1,6 @@ +formulas(sos). +(all x all y ((cycle(x,y) & odd_cycle(x,y)) -> (exists z exists w exists u (cycle(x,z,w,u,y) & adj(z,u))))). +(all x -(adj(x,x))). +(all x all y (adj(x,y) -> adj(y,x))). +(all x -(adj(x,x))). +end_of_list. diff --git a/ontologies/graphs/conversions/complete_bipartite.in b/ontologies/graphs/conversions/complete_bipartite.in new file mode 100644 index 00000000..5d46b4d1 --- /dev/null +++ b/ontologies/graphs/conversions/complete_bipartite.in @@ -0,0 +1,6 @@ +formulas(sos). +(all x all y all z ((adj(x,y) & adj(y,z)) -> -(adj(x,z)))). +(all x all y all w ((adj(x,y) & -(adj(y,w))) -> adj(x,w))). +(all x -(adj(x,x))). +(all x all y (adj(x,y) -> adj(y,x))). +end_of_list. diff --git a/ontologies/graphs/conversions/complete_graph.in b/ontologies/graphs/conversions/complete_graph.in new file mode 100644 index 00000000..04f5e9f1 --- /dev/null +++ b/ontologies/graphs/conversions/complete_graph.in @@ -0,0 +1,4 @@ +formulas(sos). +(all x all y adj(x,y)). +(all x all y (adj(x,y) -> adj(y,x))). +end_of_list. diff --git a/ontologies/graphs/conversions/complete_simple_graph.in b/ontologies/graphs/conversions/complete_simple_graph.in new file mode 100644 index 00000000..39b3674f --- /dev/null +++ b/ontologies/graphs/conversions/complete_simple_graph.in @@ -0,0 +1,5 @@ +formulas(sos). +(all x all y (-(=(x,y)) -> adj(x,y))). +(all x -(adj(x,x))). +(all x all y (adj(x,y) -> adj(y,x))). +end_of_list. diff --git a/ontologies/graphs/conversions/cycle_path.in b/ontologies/graphs/conversions/cycle_path.in new file mode 100644 index 00000000..cb1283d1 --- /dev/null +++ b/ontologies/graphs/conversions/cycle_path.in @@ -0,0 +1,9 @@ +formulas(sos). +(all x all y all z ((pendant(x) & pendant(y) & pendant(z)) -> (=(x,y) | =(x,z) | =(y,z)))). +(all x (pendant(x) <-> (leaf(x) & -(isolated_vertex(x))))). +(all x (leaf(x) <-> (all y all z ((adj(x,y) & -(=(x,y)) & -(=(x,z)) & adj(x,z)) -> =(y,z))))). +(all x all y (adj(x,y) -> adj(y,x))). +(all x (isolated_vertex(x) <-> (all y (adj(x,y) -> =(y,x))))). +(all x all y all z all w ((adj(x,y) & adj(x,z) & adj(x,w)) -> (=(y,z) | =(y,w) | =(z,w)))). +(all x -(adj(x,x))). +end_of_list. diff --git a/ontologies/graphs/conversions/cyclic_graph.in b/ontologies/graphs/conversions/cyclic_graph.in new file mode 100644 index 00000000..5fe7cf46 --- /dev/null +++ b/ontologies/graphs/conversions/cyclic_graph.in @@ -0,0 +1,6 @@ +formulas(sos). +(all x all y all z all w ((adj(x,y) & adj(x,z) & adj(x,w)) -> (=(y,z) | =(y,w) | =(z,w)))). +(all x all y (adj(x,y) -> adj(y,x))). +(all x (exists y exists z (adj(x,y) & adj(x,z) & -(=(y,z))))). +(all x -(adj(x,x))). +end_of_list. diff --git a/ontologies/graphs/conversions/double_leaf.in b/ontologies/graphs/conversions/double_leaf.in new file mode 100644 index 00000000..dd3df664 --- /dev/null +++ b/ontologies/graphs/conversions/double_leaf.in @@ -0,0 +1,7 @@ +formulas(sos). +(all x all y all z ((pendant(x) & pendant(y) & pendant(z)) -> (=(x,y) | =(x,z) | =(y,z)))). +(all x (pendant(x) <-> (leaf(x) & -(isolated_vertex(x))))). +(all x (leaf(x) <-> (all y all z ((adj(x,y) & -(=(x,y)) & -(=(x,z)) & adj(x,z)) -> =(y,z))))). +(all x all y (adj(x,y) -> adj(y,x))). +(all x (isolated_vertex(x) <-> (all y (adj(x,y) -> =(y,x))))). +end_of_list. diff --git a/ontologies/graphs/conversions/empty_graph.in b/ontologies/graphs/conversions/empty_graph.in new file mode 100644 index 00000000..96467f87 --- /dev/null +++ b/ontologies/graphs/conversions/empty_graph.in @@ -0,0 +1,4 @@ +formulas(sos). +(all x all y -(adj(x,y))). +(all x all y (adj(x,y) -> adj(y,x))). +end_of_list. diff --git a/ontologies/graphs/conversions/endloop_graph.in b/ontologies/graphs/conversions/endloop_graph.in new file mode 100644 index 00000000..8b1e38c9 --- /dev/null +++ b/ontologies/graphs/conversions/endloop_graph.in @@ -0,0 +1,5 @@ +formulas(sos). +(all x all y all z all w ((adj(x,y) & adj(x,z) & adj(x,w)) -> (=(y,z) | =(y,w) | =(z,w)))). +(all x all y (adj(x,y) -> adj(y,x))). +(all x (exists y exists z (adj(x,y) & adj(x,z) & -(=(y,z))))). +end_of_list. diff --git a/ontologies/graphs/conversions/graph_loops.in b/ontologies/graphs/conversions/graph_loops.in new file mode 100644 index 00000000..eaae6948 --- /dev/null +++ b/ontologies/graphs/conversions/graph_loops.in @@ -0,0 +1,4 @@ +formulas(sos). +(all x adj(x,x)). +(all x all y (adj(x,y) -> adj(y,x))). +end_of_list. diff --git a/ontologies/graphs/conversions/interval_graph.in b/ontologies/graphs/conversions/interval_graph.in new file mode 100644 index 00000000..69ff5600 --- /dev/null +++ b/ontologies/graphs/conversions/interval_graph.in @@ -0,0 +1,11 @@ +formulas(sos). +(all x all y ((complement_cycle(x,y) & complement_odd(x,y)) -> (exists z exists w exists u (complement_cycle(x,z,w,u,y) & -(adj(z,u)))))). +(all x all y all z (complement_path(x,y,z) <-> (complement_path(x,y) & -(adj(y,z))))). +(all x all y (complement_cycle(x,y) <-> (complement_path(x,y) & -(adj(x,y))))). +(all x all y (complement_odd(x,y) <-> (-(adj(x,y)) | (exists z (-(adj(x,z)) & complement_even(z,y)))))). +(all x all y (complement_even(x,y) <-> (-(adj(x,y)) | (exists z (-(adj(x,z)) & complement_odd(z,y)))))). +(all x all y all z all w (cycle(x,y,z,w) -> (exists u exists v (path(x,u,w) & path(x,v,w) & adj(u,v))))). +(all x -(adj(x,x))). +(all x all y (adj(x,y) -> adj(y,x))). +(all x -(adj(x,x))). +end_of_list. diff --git a/ontologies/graphs/conversions/nobranch.in b/ontologies/graphs/conversions/nobranch.in new file mode 100644 index 00000000..f5f24e0c --- /dev/null +++ b/ontologies/graphs/conversions/nobranch.in @@ -0,0 +1,4 @@ +formulas(sos). +(all x all y all z all w ((adj(x,y) & adj(x,z) & adj(x,w)) -> (=(y,z) | =(y,w) | =(z,w)))). +(all x all y (adj(x,y) -> adj(y,x))). +end_of_list. diff --git a/ontologies/graphs/conversions/path_graph.in b/ontologies/graphs/conversions/path_graph.in new file mode 100644 index 00000000..a218b79a --- /dev/null +++ b/ontologies/graphs/conversions/path_graph.in @@ -0,0 +1,10 @@ +formulas(sos). +(exists x exists y (pendant(x) & pendant(y) & -(=(x,y)))). +(all x (pendant(x) <-> (leaf(x) & -(isolated_vertex(x))))). +(all x (leaf(x) <-> (all y all z ((adj(x,y) & -(=(x,y)) & -(=(x,z)) & adj(x,z)) -> =(y,z))))). +(all x all y (adj(x,y) -> adj(y,x))). +(all x (isolated_vertex(x) <-> (all y (adj(x,y) -> =(y,x))))). +(all x all y all z ((pendant(x) & pendant(y) & pendant(z)) -> (=(x,y) | =(x,z) | =(y,z)))). +(all x all y all z all w ((adj(x,y) & adj(x,z) & adj(x,w)) -> (=(y,z) | =(y,w) | =(z,w)))). +(all x -(adj(x,x))). +end_of_list. diff --git a/ontologies/graphs/conversions/permutation_graph.in b/ontologies/graphs/conversions/permutation_graph.in new file mode 100644 index 00000000..97a3b733 --- /dev/null +++ b/ontologies/graphs/conversions/permutation_graph.in @@ -0,0 +1,7 @@ +formulas(sos). +(all x all y ((complement_cycle(x,y) & complement_odd_cycle(x,y)) -> (exists z exists w exists u (complement_cycle(x,z,w,u,y) & -(adj(z,u)))))). +(all x all y ((cycle(x,y) & odd_cycle(x,y)) -> (exists z exists w exists u (cycle(x,z,w,u,y) & adj(z,u))))). +(all x -(adj(x,x))). +(all x all y (adj(x,y) -> adj(y,x))). +(all x -(adj(x,x))). +end_of_list. diff --git a/ontologies/graphs/conversions/polycyclic_graph.in b/ontologies/graphs/conversions/polycyclic_graph.in new file mode 100644 index 00000000..a92895e8 --- /dev/null +++ b/ontologies/graphs/conversions/polycyclic_graph.in @@ -0,0 +1,5 @@ +formulas(sos). +(all x -(adj(x,x))). +(all x all y (adj(x,y) -> adj(y,x))). +(all x (exists y exists z (adj(x,y) & adj(x,z) & -(=(y,z))))). +end_of_list. diff --git a/ontologies/graphs/conversions/polycyclic_loop.in b/ontologies/graphs/conversions/polycyclic_loop.in new file mode 100644 index 00000000..e9123832 --- /dev/null +++ b/ontologies/graphs/conversions/polycyclic_loop.in @@ -0,0 +1,5 @@ +formulas(sos). +(all p1 all p2 all p4 ((adj(p1,p2) & adj(p1,p4) & -(=(p2,p4))) -> (exists p3 (adj(p2,p3) & -(=(p3,p1)))))). +(all x all y (adj(x,y) -> adj(y,x))). +(all x -(adj(x,x))). +end_of_list. diff --git a/ontologies/graphs/conversions/pseudocyclic_graph.in b/ontologies/graphs/conversions/pseudocyclic_graph.in new file mode 100644 index 00000000..92a152b1 --- /dev/null +++ b/ontologies/graphs/conversions/pseudocyclic_graph.in @@ -0,0 +1,4 @@ +formulas(sos). +(all x (exists y exists z (adj(x,y) & adj(x,z) & -(=(y,z))))). +(all x all y (adj(x,y) -> adj(y,x))). +end_of_list. diff --git a/ontologies/graphs/conversions/quasicyclic_graph.in b/ontologies/graphs/conversions/quasicyclic_graph.in new file mode 100644 index 00000000..abd15004 --- /dev/null +++ b/ontologies/graphs/conversions/quasicyclic_graph.in @@ -0,0 +1,6 @@ +formulas(sos). +(all p1 all p2 all p4 ((adj(p1,p2) & adj(p1,p4) & -(=(p2,p4))) -> (exists p3 (adj(p2,p3) & -(=(p3,p1)))))). +(all x all y (adj(x,y) -> adj(y,x))). +(all x all y all z all w ((adj(x,y) & adj(x,z) & adj(x,w)) -> (=(y,z) | =(y,w) | =(z,w)))). +(all x -(adj(x,x))). +end_of_list. diff --git a/ontologies/graphs/conversions/ray_graph.in b/ontologies/graphs/conversions/ray_graph.in new file mode 100644 index 00000000..4c960456 --- /dev/null +++ b/ontologies/graphs/conversions/ray_graph.in @@ -0,0 +1,10 @@ +formulas(sos). +(exists x pendant(x)). +(all x (pendant(x) <-> (leaf(x) & -(isolated_vertex(x))))). +(all x (leaf(x) <-> (all y all z ((adj(x,y) & -(=(x,y)) & -(=(x,z)) & adj(x,z)) -> =(y,z))))). +(all x all y (adj(x,y) -> adj(y,x))). +(all x (isolated_vertex(x) <-> (all y (adj(x,y) -> =(y,x))))). +(all x all y all z ((pendant(x) & pendant(y) & pendant(z)) -> (=(x,y) | =(x,z) | =(y,z)))). +(all x all y all z all w ((adj(x,y) & adj(x,z) & adj(x,w)) -> (=(y,z) | =(y,w) | =(z,w)))). +(all x -(adj(x,x))). +end_of_list. diff --git a/ontologies/graphs/conversions/scattered_edge.in b/ontologies/graphs/conversions/scattered_edge.in new file mode 100644 index 00000000..cb2d9830 --- /dev/null +++ b/ontologies/graphs/conversions/scattered_edge.in @@ -0,0 +1,5 @@ +formulas(sos). +(all x all y all z ((adj(x,y) & adj(x,z)) -> =(y,z))). +(all x -(adj(x,x))). +(all x all y (adj(x,y) -> adj(y,x))). +end_of_list. diff --git a/ontologies/graphs/conversions/simple_graph.in b/ontologies/graphs/conversions/simple_graph.in new file mode 100644 index 00000000..46558825 --- /dev/null +++ b/ontologies/graphs/conversions/simple_graph.in @@ -0,0 +1,4 @@ +formulas(sos). +(all x -(adj(x,x))). +(all x all y (adj(x,y) -> adj(y,x))). +end_of_list. diff --git a/ontologies/graphs/conversions/simple_nobranch.in b/ontologies/graphs/conversions/simple_nobranch.in new file mode 100644 index 00000000..7ef8296a --- /dev/null +++ b/ontologies/graphs/conversions/simple_nobranch.in @@ -0,0 +1,5 @@ +formulas(sos). +(all x all y all z all w ((adj(x,y) & adj(x,z) & adj(x,w)) -> (=(y,z) | =(y,w) | =(z,w)))). +(all x all y (adj(x,y) -> adj(y,x))). +(all x -(adj(x,x))). +end_of_list. diff --git a/ontologies/graphs/conversions/split_graph.in b/ontologies/graphs/conversions/split_graph.in new file mode 100644 index 00000000..11d54cca --- /dev/null +++ b/ontologies/graphs/conversions/split_graph.in @@ -0,0 +1,9 @@ +formulas(sos). +(all x all y all z all w (complement_cycle(x,y,z,w) -> (exists u exists v (complement_path(x,u,w) & complement_path(x,v,w) & -(adj(u,v)))))). +(all x all y all z (complement_path(x,y,z) <-> (complement_path(x,y) & -(adj(y,z))))). +(all x all y (complement_cycle(x,y) <-> (complement_path(x,y) & -(adj(x,y))))). +(all x all y all z all w (cycle(x,y,z,w) -> (exists u exists v (path(x,u,w) & path(x,v,w) & adj(u,v))))). +(all x -(adj(x,x))). +(all x all y (adj(x,y) -> adj(y,x))). +(all x -(adj(x,x))). +end_of_list. diff --git a/ontologies/graphs/conversions/star_graph.in b/ontologies/graphs/conversions/star_graph.in new file mode 100644 index 00000000..a945b219 --- /dev/null +++ b/ontologies/graphs/conversions/star_graph.in @@ -0,0 +1,6 @@ +formulas(sos). +(exists x (all y (adj(x,y) | =(x,y)))). +(all x all y all z ((adj(x,y) & adj(y,z) & adj(x,z)) -> =(x,z))). +(all x -(adj(x,x))). +(all x all y (adj(x,y) -> adj(y,x))). +end_of_list. diff --git a/ontologies/graphs/conversions/trivially_perfect.in b/ontologies/graphs/conversions/trivially_perfect.in new file mode 100644 index 00000000..69a74bdf --- /dev/null +++ b/ontologies/graphs/conversions/trivially_perfect.in @@ -0,0 +1,6 @@ +formulas(sos). +(all x all y all z all w ((adj(x,y) & adj(y,z) & adj(z,w) & adj(w,x)) -> (adj(x,z) | adj(y,w)))). +(all x all y all z all w ((adj(x,y) & adj(y,z) & adj(z,w)) -> (adj(x,z) | adj(x,w) | adj(y,w)))). +(all x -(adj(x,x))). +(all x all y (adj(x,y) -> adj(y,x))). +end_of_list. diff --git a/ontologies/graphs/conversions/undirected_cyclic_graph.in b/ontologies/graphs/conversions/undirected_cyclic_graph.in new file mode 100644 index 00000000..26a0fc4b --- /dev/null +++ b/ontologies/graphs/conversions/undirected_cyclic_graph.in @@ -0,0 +1,5 @@ +formulas(sos). +(all v all y all z ((adj(v,'x') & adj(v,y) & adj(v,z)) -> (=('x',y) | =('x',z) | =(y,z)))). +(all x (exists y exists z (adj(x,y) & adj(x,z)))). +(all x all y (adj(x,y) -> adj(y,x))). +end_of_list. diff --git a/ontologies/graphs/conversions/undirected_graph.in b/ontologies/graphs/conversions/undirected_graph.in new file mode 100644 index 00000000..f6e9b37d --- /dev/null +++ b/ontologies/graphs/conversions/undirected_graph.in @@ -0,0 +1,3 @@ +formulas(sos). +(all x all y (adj(x,y) -> adj(y,x))). +end_of_list. diff --git a/ontologies/graphs/conversions/weak_pseudocyclic_graph.in b/ontologies/graphs/conversions/weak_pseudocyclic_graph.in new file mode 100644 index 00000000..6314a5df --- /dev/null +++ b/ontologies/graphs/conversions/weak_pseudocyclic_graph.in @@ -0,0 +1,4 @@ +formulas(sos). +(all p1 all p2 all p4 ((adj(p1,p2) & adj(p1,p4) & -(=(p2,p4))) -> (exists p3 (adj(p2,p3) & -(=(p3,p1)))))). +(all x all y (adj(x,y) -> adj(y,x))). +end_of_list.