В математической логике , интерпретация Herbrand является интерпретация , в которой все константы и функциональные символы назначаются очень простой смысл. [1] В частности, каждая константа интерпретируется как сама по себе, а каждый символ функции интерпретируется как функция, которая его применяет. Интерпретация также определяет предикатные символы как обозначающие подмножество соответствующей базы Эрбранда , эффективно определяя, какие основные атомы являются истинными в интерпретации. Это позволяет интерпретировать символы в наборе предложений чисто синтаксически , отдельно от любого реального экземпляра.
Важность интерпретаций Хербрана состоит в том, что если какая-либо интерпретация удовлетворяет заданному набору пунктов S, то существует интерпретация Хербрана, которая им удовлетворяет. Кроме того, теорема Эрбран утверждает , что если S невыполним , то есть конечное невыполнимо множество основных экземпляров из вселенной Эрбрана определенной S . Поскольку это множество конечно, его невыполнимость можно проверить за конечное время. Однако таких наборов для проверки может быть бесконечное количество.
Он назван в честь Жака Эрбрана .
См. Также [ править ]
Заметки [ править ]
- ^ Бен Coppin (2004). Освещенный искусственный интеллект . Джонс и Бартлетт Обучение. п. 231. ISBN. 978-0-7637-3230-1.