Неинтерпретированная функция
- Неинтерпретируемые функции или функциональные символы в математической логике не обладают другими свойствами, кроме своего названия и n-образной формы.
- Функциональные символы используются вместе с константами и переменными для формирования терминов.
- Теория неинтерпретируемых функций иногда называется свободной теорией, так как она свободно генерируется и является свободным объектом.
- Проблемы выполнимости свободных теорий решаются с помощью синтаксической унификации, которая используется интерпретаторами для компьютерных языков.
- Синтаксическая унификация также используется в алгоритмах для решения проблемы выполнимости некоторых других уравнительных теорий.
- Проблема решения для свободных теорий важна, так как с ее помощью можно сократить многие теории.
- Свободные теории могут быть решены путем поиска общих подвыражений для формирования замыкания конгруэнтности.
Полный текст статьи: