Конфлюэнтность преобразований графа: автодоказательство

[malphunction]

Приветствую!

Разрабатываю систему управления знаниями на семантических сетях; возникла следующая проблема: пусть два пользователя редактируют семантическую сеть независимо друг от друга, нужно слить результат в одну сеть.

Формальнее: есть набор операций над графами $OP = \{o_1, o_2, o_3, o_4, \ldots\}$ (например, "соединить две вершины", "удалить вершину", "породить вершину под управлением графа $C$"). Есть граф (семантическая сеть) $G$. Есть управляющий граф $C_G$, который задает разрешенные операции над $G$: при редактировании графа $G$ каждый раз доступны только часть операций, которые могут применяться к определенным частям графа.

Далее, есть две истории редактирования от двух пользователей: $OP_A = $\langle op^a_{i_1}, op^a_{i_2}, op^a_{i_3}, \ldots\rangle$ -- первого пользователя, $OP_B = $\langle op^b_{i_1}, op^b_{i_2}, op^b_{i_3}, \ldots\rangle$ -- второго пользователя. Мне нужно построить последовательность $OP_{AB} = \langle op^x_{i_1}, op^x_{i_2}, op^x_{i_3}, \ldots\rangle$, которая бы совмещала их истории.

Я решил доказать сначала, что истории можно сливать как угодно, лишь бы порядок подысторий сохранялся (т.е. если есть истории $abc$ и $klm$, то допустимы истории $akblcm$, или $abcklm$, или $klambc$, но не $mlabck$). Другими словами мне нужно доказать конфлюэнтность слияния историй: в каком бы порядке истории не сливались, всегд получится одинаковый результат.

Это решаемо: доказываем нётеровость графа возможных операций, доказываем локальную конфлюэнтность, после чего следует, что вся система конфлюэнтна. Но тут возникает проблема разрешения конфликтов: например, в первой истории первый пользователь удаляет вершину, а во второй истории пользователь соединяет её с другой вершиной. Конфликт! Слить истории невозможно. Пример посложнее: под управлением упр.графа $C_G$ можно порождать упорядоченные последовательности вершин. Если оба пользователя создадут две последовательности, то как их потом сливать? Тоже конфликт.

Вопрос: как отыскать наборы операций, которые приводят к конфликту?

Если бы набор операций был фиксированный, то можно было бы сделать вручную: перебрать все их сочетания, найти конфликтные. Тогда остальные сочетания были бы разрешенными.

Поэтому конечный мой вопрос такой: есть ли какой-то алгоритм, который на входе получает набор операций, а на выходе дает наборы конфликтных ситуаций?

Я начал искать автоматизированные системы в области систем переписывания (rewriting systems), нашел пока только Maude (https://en.wikipedia.org/wiki/Maude_system). Подскажите другие подходы и программные системы!

<br/>

Вдогонку: намекните хотя бы, куда рыть? По каким ключевым словам искать математический аппарат?