Применение искинов - шоссе империализма (Стенгазета русификаторов ИТ)

Информация о пользователе

Привет, Гость! Войдите или зарегистрируйтесь.

1965, J. A. Robinson, A Machine-Oriented Logic Based on the Resolution

Страница: 1

Сообщений 1 страница 3 из 3

1

  • Автор: Лис [К]
  • Сочувствующий
  • Лис [К]
  • Зарегистрирован: 2019-05-16
  • Приглашений: 0
  • Сообщений: 1009
  • Уважение: [+1/-0]
  • Позитив: [+0/-0]
  • Провел на форуме:
    6 дней 3 часа
  • Последний визит:
    2021-02-04 17:36:28

1965, John Alan Robinson, A Machine-Oriented Logic Based on the Resolution

Нашел .pdf на сайте Microsoft Academics, 19 страниц

John Alan Robinson
https://en.wikipedia.org/wiki/John_Alan_Robinson
https://ru.wikipedia.org/wiki/Робинсон,_Джон_Алан

На эту книгу все ссылаются, кто про унификацию пишет.

А унификация нужна для FCG.

Ещё
«Syntactical first-order unification is used in logic programming and programming language type system implementation, especially in Hindley–Milner based type inference algorithms.»
алгоритм Хиндли — Милнера (Hindley–Milner type inference algorithm)

Предлагаю обсудить содержание (ну или прочитать хотя бы самому).

Отредактировано Лис (2019-11-23 21:35:00)

0

2

  • Автор: Лис [К]
  • Сочувствующий
  • Лис [К]
  • Зарегистрирован: 2019-05-16
  • Приглашений: 0
  • Сообщений: 1009
  • Уважение: [+1/-0]
  • Позитив: [+0/-0]
  • Провел на форуме:
    6 дней 3 часа
  • Последний визит:
    2021-02-04 17:36:28

fundamental theorem of Herbrand
фундаментальная теорема Эрбрана
https://en.wikipedia.org/wiki/Herbrand%27s_theorem
(в русской википедии такой страницы нет, украинцы обгоняют нас в it-развитии)

Отредактировано Лис (2019-11-23 21:48:17)

0

3

  • Автор: Лис [К]
  • Сочувствующий
  • Лис [К]
  • Зарегистрирован: 2019-05-16
  • Приглашений: 0
  • Сообщений: 1009
  • Уважение: [+1/-0]
  • Позитив: [+0/-0]
  • Провел на форуме:
    6 дней 3 часа
  • Последний визит:
    2021-02-04 17:36:28

resolution principle

Правило резолюций предложено в 1930 году в докторской диссертации Жака Эрбрана для доказательства теорем в формальных системах первого порядка. Правило разработано Джоном Аланом Робинсоном в 1965 году.

While a resolution rule for propositional logic had been presented earlier in Davis and Putnam [1960],
Robinson’s contribution is generalizing resolution to the first-order setting,
which he accomplishes by giving an algorithm for finding the most general unifying substitution of a set of literals.

https://ru.wikipedia.org/wiki/Правило_резолюций

Отредактировано Лис (2019-11-23 22:20:38)

0

Страница: 1