Многоагентные временные логики, проблемы унификации и допустимости

Изучается временная многоагентная логика с различными индивидуальными для каждого агента участками потерянного времени. Логика базируется на фермах с основными базисными множествами на всех натуральных числах $N$ как временных состояниях, где каждый агент $j$ может иметь собственные множества $X_j$ недоступных (потерянных, забытых) состояний времени ($\forall j \in J, X_j \subset N$).
Основными математическими задачами исследования являются проблемы унификации и проблема алгоритмического распознавания допустимых правил вывода. Решение проблемы унификации состоит в нахождении конечного вычислимого множества формул, являющегося полным множеством унификаторов. Эта задача решается с применением техники проективных формул, предложенной Сильвио Гиларди. Доказано, что каждая унифицируемая в этой логике формула проективна, и построен алгоритм, конструирующий ее проективный унификатор. Тем самым решена проблема унификации. Это позволяет решить открытую проблему алгоритмического распознавания допустимых правил. Статья завершается введением обобщения определения проективных формул — слабо проективных формул, и простым примером его применения.