Структура Herbrand - Herbrand structure

В логике первого порядка , А структура Эрбран S является структурой над словарным сгом, которая определяется исключительно синтаксическими свойствами а. Идея состоит в том, чтобы использовать символы терминов в качестве их значений, например, обозначение постоянного символа c - это просто « c » (символ). Он назван в честь Жака Эрбрана .

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

Вселенная Herbrand

Определение

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

(1) Универсум Эрбранда языка 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

Эрбрановы структура интерпретирует условия , на вершине вселенной Эрбрана .

Определение

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

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

Замечания

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

Примеры

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

  • U = { с , Ь , FFC , fffc , ...}
  • fc → fc , ffc → ffc , ...
  • с → с

База Herbrand

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

Определение

Эрбрана база представляет собой совокупность всех атомов основания которых аргумент термины являются Эрбрана вселенной.

Примеры

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

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

Смотрите также

Примечания

  1. ^ "Семантика Herbrand" .

использованная литература