Порождение и распознавание языков над термами

Рассматриваются вопросы, связанные с построением логического вывода в системах аксиом, задаваемых хорновскими формулами специального вида. Предлагается метод построения программы, строящей вывод для заданной системы аксиом.