2008_ 2009 - определения и теоремы из вариантов (Задания прошлых лет)

5------------------------------------------------

• Логическое следствие множества предложений. Замкнутая формула.

• Теорема компактности Мальцева. Следует ли из него утверждение … ?

• Теорема полноты табличного вывода для классической логики предикатов. Выполнимость формулы в случае отсутствия успешного табличного вывода у обеих семантических таблиц.

• Теорема о логическом следствии для классической логики предикатов.

• Выполнимая семантическая таблица. Является ли выполнимой семантическая таблица … Может ли выполнимая таблица содержать только невыполнимые формулы? Пример невыполнимой семантической таблицы, содержащей только общезначимые формулы.

• Теорема корректности табличного вывода для классической логики предикатов. Корректно ли правило табличного вывода … ?

6------------------------------------------------

• Эрбрановская интерпретация для заданной сигнатуры. Сколько существует различных эрбрановских интерпретаций в сигнатуре, состоящей из … ?

• Равносильные формулы логики предикатов. Докажите, что два предложения являются равносильными тогда и только тогда, когда множество логических следствий формулы одного совпадает с множеством логических следствий другого.

• Теорема об эрбрановских интерпретациях. Каждая непротиворечивая система дизъюнктов имеет хотя бы одну эрбрановскую модель? Сколько эрбрановских моделей в сигнатуре … ? Бесконечна ли предметная область всякой эрбрановской интерпретации сигнатуры … ?

• Теорема о сколемовской стандартной форме. Верно ли, что если формула в предварительной нормальной форме является общезначимой формулой, то и соответствующая ей сколемовская стандартная форма также будет общезначимой формулой?

• Эрбрановский универсум заданной сигнатуры. Сколько различных элементов содержит эрбрановский универсум сигнатуры, состоящей из … ? Каким условиям должна удовлетворять сигнатура для того, чтобы её эрбрановский универсум был конечным множеством?

• Теорема компактности Мальцева. Следует ли из теоремы компактности теорема Эрбрана?

7------------------------------------------------

• Определение SLD-резолютивного вычисления запроса, обращенного к хорновской логической программе. Верно ли, если программа … и запрос … , обращенный к ней, имеет хотя бы одно успешное SLD–резолютивное вычисление? Существуют ли такие хорновские логические программы, которые не имеют ни одного успешного SLD-резолютивного вычисления ни для каких запросов?

• Вычисленный ответ на запрос к хорновской логической программе. Существуют ли такие правильные ответы на запрос к хорновской логической программе, которые не могут быть вычислены?

• Теорема корректности операционной семантики относительно декларативной семантики. Верно ли, что из этой теоремы следует, что для любого атома из наименьшей эрбрановской модели программы запрос, обращенный к этой программе, имеет успешное вычисление?

• Алгоритм вычисления наиболее общего унификатора двух атомов.

• SLD–резольвента запроса и программного утверждения. Выписать все SLD–резольвенты …

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

• Теорема об основном правильном ответе на запрос к хорновской логической программе. Если запрос к хорновской логической программе имеет хотя бы одно успешное вычисление, то этот запрос имеет хотя бы один основной правильный ответ?

• Правильный ответ на запрос к хорновской логической программе. Сколько правильных ответом может иметь запрос G=?A, обращенный к хорновской логической программе P, в том случае, если А – основной атом? Всякий запрос к хорновской логической программе, имеющий правильный ответ, имеет хотя бы одно успешное вычисление, которое вычисляет этот ответ?

• Теорема полноты операционной семантики хроновских логических программ относительно декларативной семантики. Из этой теоремы следует, что для любого основного атома, являющегося следствием программы, любое вычисление запроса, обращенного к этой программе, является успешным?

8------------------------------------------------

• Стратегия вычисления логических программ. Зависит ли ответ на запрос … от того, какая именно стратегия вычисления применяется?

• Допущение замкнутости мира. Верно ли, что …

• Теорема Черча о проблеме общезначимости в классической логике предикатов. Следует ли из теоремы, что не существует алгоритма, проверяющего выполнимость формул логики предикатов? Существует ли алгоритм, проверяющий противоречивость конечных множеств замкнутых формул логики предикатов?

• Теорема сильной полноты для хорновских логических программ? Сохраняет ли она справедливость для логических программ, содержащих оператор not?

• Дерево SLD-резолютивных вычисления запроса, обращенного к хорновской логической программе. Зависит ли устройство дерева от правила выбора подцелей?

• Правило SLDNF-резолюций. Какой ответ будет получен на запрос … к программе … ?

• Алгоритмическая универсальность хорновского логического программирования. для любой логической программы с операторами отсечения и отрицания существует такая хорновская логическая программа (без отсечений и отрицаний), которая вычисляет точно такое же множество ответов?

• Как определяется отношение выполнимости … для формулы вида … в темпоральной логиче линейного времени PLTL? Выберите всевозможные пары равносильных формул из множества формул PLTL {…}.

9------------------------------------------------

• Частичная корректность программы относительно предусловия и постусловия в интерпретации. Является ли программа … частично корректной относительно предусловия … и постусловия … в стандартной интерпретации арифметики целых числе?

• Отношение выполнимости в темпоральной логике PLTL. Являются ли формулы … равносильными?

• Задача верификации моделей программ. К каким задачам теории графов сводится задача model-checking в темпоральной логике PLTL?

• Отношение выполнимости в интуиционистской логике. Какие из формул … являются общезначимыми в интуиционистской логике?

• Интерпретация интуиционистской логики высказываний. Является ли формула … общезначимой в интуиционистской логике высказываний?

• Отношение выполнимости в модальной логике. Для любой модели Крипке и для любого состояния если …, то … ?

10------------------------------------------------

• Модель для формулы. Замкнутая формула. Логическое следствие. Успешный табличный вывод из таблицы

• Успешный табличный вывод из семантической таблицы. Выполнимая таблица.

• Непротиворечивые множества. Общезначимые формулы.

• Бесконечная предметная область модели множества формул. (Не)противоречивая формула.

• Общая модель формул.

• Эрбрановская интерпретация.

11------------------------------------------------

• Резолютивно выводимая формула.

• Правило резолюции. Резольвента формулы. Унификатор. Теорема корректности резолютивного вывода. Теорема полноты резолютивного вывода.

• Резолютивный вывод (пустого дизъюнкта).

• Предваренная нормальная форма формулы. Сколемовская стандартная форма формулы. Процедура сколемизации. Общезначимая формула. Выполнимая формула.

• Эрбрановская интерпретация.

• Формула логики предикатов первого порядка выполнима тогда и только тогда, когда … .

• (Не)противоречивый дизъюнкт.

• Атом. Хорновская логическая программа. Эрбрановская модель. Успешное вычисление.

12------------------------------------------------

• Хорновская логическая программа. Успешное SLD-резолютивное вычисление. Факт в программе. Противоречивая система формул.

• Успешное SLD-резолютивное опровержение. Подстановка. Атом.

• Оператор непосредственного логического следования. Эбрановская интерпретация.

• Правильный ответ.

• Эрбрановский базис.

• Наименьшая эрбрановская модель.

• Замкнутая формула. Сколемовская стандартная форма. Общезначимая формула. Интерпретация.

• Эрбрановская интерпретация.

• Удаление из программы операторов отсечения и отрицания.

13------------------------------------------------

• Арифметическая функция, вычислимая на машине Тьюринга. (Не)стандартная стратегия. Хорновская логическая программа.

• Запрос к программе не имеет успешных вычислений.

• Из программы удалены все операторы отсечения. Вычисление запроса.

• Инвариант цикла. выполнимые формулы. Общезначимые формулы.

• Преобразование программы: в конце каждого программного утверждения был поставлен оператор отсечения. Стандартная стратегия.

• Алгоритм проверки общезначимости формул логики предикатов, предварительная нормальная форма которых имеет вид … .

• Формула PLTL. Конечная модель LTS. Система Хинтикки. Ориентированный граф с количеством вершин … .