Структура Herbrand

В логике первого порядка, структура Herbrand S - это структура над словарём σ, которая определяется исключительно синтаксическими свойствами σ. Идея состоит в том, чтобы использовать символы терминов в качестве их значений, например обозначение постоянного символа c - это просто "c" (символ).

Структуры Herbrand играют важную роль в основах логического программирования.

• 1 Вселенная Herbrand
  • 1.1 Определение
  • 1.2 Пример
• 2 Структура Herbrand
  • 2.1 Определение
  • 2.2 Примечания
  • 2.3 Примеры
• 3 База Herbrand
  • 3.1 Определение
  • 3.2 Примеры
• 4 См. Также
• 5 Примечания
• 6 Ссылки

Определение

Вселенная Herbrand служит вселенной в структуре Herbrand.

(1) Вселенная Herbrand языка первого порядка L - это набор всех основных терминов языка L. Если язык не имеет констант, то язык расширяется путем добавления произвольная новая константа.

• Вселенная Эрбранда счетно бесконечна, если σ является счетным и существует функциональный символ арности больше 0.
• В контексте языков первого порядка мы также говорим просто о вселенной Гербрана словаря σ.

(2) Вселенная Эрбрана замкнутой формулы в нормальной форме Сколема F - это набор всех членов без переменных, которые могут быть построены с использованием функциональных символов и констант F. Если F не имеет констант, то F расширяется путем добавления произвольной новой константы.

• Это второе определение важно в контексте разрешения вычислений.

Пример

Пусть L будет языком первого порядка со словарём

• постоянными символами: c
• функциональные символы: f (.), g (.)

тогда вселенная Эрбрана для L (или σ) есть {c, f (c), g (c), f (f (c)), f ( g (c)), g (f (c)), g (g (c)),...}.

Обратите внимание, что символы связи не имеют отношения к юниверсу Herbrand.

Структура Herbrand интерпретирует термины поверх вселенной Herbrand.

Определение

Пусть S будет структурой со словарем σ и универсумом U. Пусть T будет набором всех терминов над σ и T 0 быть подмножеством всех без переменных терминов. S называется структурой Эрбрана, если

1. U = T 0
2. f (t 1,..., t n) = f (t 1,..., t n) для любого n-арного функционального символа f ∈ σ и t 1,..., t n ∈ T 0
3. c = c для каждой константы c в σ

Примечания

1. U - это вселенная Эрбранда для σ.
2. Структура Эрбранда, которая является моделью теории T, называется структурой Эрбранда. модель T.

Примеры

Для постоянного символа c и унарного функционального символа f (.) мы имеем следующую интерпретацию:

• U = {c, fc, ffc, fffc,...}
• fc → fc, ffc → ffc,...
• c → c

В дополнение к вселенной, определенной во вселенной Эрбранда, и обозначения термина, определенные в структуре Herbrand, база Herbrand завершает интерпретацию, обозначая символы отношения.

Определение

База Хербранда - это набор всех основных атомов, членами аргумента которых является вселенная Хербранда.

Примеры

Для символа двоичного отношения R мы получаем с помощью указанных выше терминов:

{R (c, c), R (fc, c), R (c, fc), R (fc, fc), R (ffc, c),...}

• теорему Эрбранда
• Herbrandization
• Интерпретация Herbrand
• Herbrand Вселенная
• База Хербранда

1. ^http://logic.stanford.edu/herbrand/herbrand.html

• Эббингаус, Хайнц-Дитер ; Флум, Йорг; Томас, Вольфганг (1996). Математическая логика. Спрингер. ISBN 978-0387942582.