Структура Herbrand - Википедия - Herbrand structure

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

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

Вселенная Herbrand

Определение

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

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

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

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

Пример

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

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

затем вселенная Herbrand Lσ (или σ) равно {c, ж(c), грамм(c), ж(ж(c)), ж(грамм(c)), грамм(ж(c)), грамм(грамм(c)), ...}.

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

Структура Herbrand

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

Определение

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

  1. U = Т0
  2. ж S(т1, ..., тп) = ж(т1, ..., тп) для каждого псимвол функции ж ∈ σ и т1, ..., тп ∈ Т0
  3. cS = c для каждой постоянной c в σ

Замечания

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

Примеры

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

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

База Herbrand

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

Определение

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

Примеры

Для символа бинарного отношения р, мы получаем с условиями сверху:

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

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

Примечания

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

Рекомендации

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