Читаю про Maude и переписывание термов здесь http://www.cs.swan.ac.uk/~csneal/MaudeCourse/termrewriting.html (другие ссылки можно взять отсюда http://en.wikipedia.org/wiki/Maude_system).
И не могу понять, переписывание термов - это по сути Datalog с наследованием типов? Возможности унификации, как в прологе, отсутствуют, сопоставления с образцом, как в рефале, отсутствуют. Зато большая эффективность и заточенность на декларативное описание модели. Я прав?