формальная система
формальная теория
исчисление
Совокупность абстрактных объектов (объектов, никак не связанных с реальным миром), в которой представлены правила оперирования цепочками символов в исключительно синтаксической трактовке без учета какого-либо смыслового содержания
алфавит формальной системы
Конечное множество символов, доступных для построения формул формальной системы
формула формальной системы
правильно построенная формула
п.п.ф.
Линейная цепочка, построенная из символов алфавита формальной системы с использованием некоторого набора синтаксических правил
аксиома формальной системы
Формула формальной системы, выделенная разработчиком формальной системы
правило вывода в формальной системе
Отношение на множестве правильно построенных формул формальной системы
посылка правила вывода
заключение правила вывода
следствие правила вывода
непосредственно выводимая формула
Формула формальной системы, являющаяся заключением некоторого правила вывода
правило продукции
продукция
Правило вывода в формальной системе, применяемое к формулам формальной системы как единому целому
правило переписывания
Правило вывода в формальной системе, применяемое к любой отдельной части формулы формальной системы при условии, что эта часть сама является формулой формальной системы
вывод формулы в формальной системе
Последовательность формул формальной системы такая, что каждая формула в ней непосредственно выводима из подмножества множества формул, являющегося объединением исходного множества формул, множества аксиом и ранее выведенных формул
доказательство формулы в формальной системе
Вывод формулы в формальной системе, в котором в качестве исходного множества формул используются только аксиомы
теорема в формальной системе
Формула формальной системы, являющаяся результатом доказательства
разрешимая формальная система
Формальная система, для которой существует эффективная процедура, позволяющая для любой формулы определить, является ли данная формула теоремой или нет
исчисление предикатов первого порядка
ИППП
Формальная система, используемая для представления знаний в системах искусственного интеллекта
алфавит исчисления предикатов первого порядка
Конечное множество символов, используемых для построения формул ИППП. Состоит из предметных переменных, предметных констант, n-местных предикатных букв, m-местных функциональных букв, символов конъюнкции, дизъюнкции, импликации и отрицания, кванторов общности и существования, круглых скобок и запятой
предикатная буква ИППП
один из символов алфавита исчисления предикатов первого порядка. Для обозначения предикатных букв обычно используются прописные буквы из середины латинского алфавита (P, Q, R, ...)
функциональная буква ИППП
один из символов алфавита исчисления предикатов первого порядка. Для обозначения функциональных букв обычно используются строчные буквы из середины латинского алфавита (f, g, h, ...)
предметная переменная ИППП
один из символов алфавита исчисления предикатов первого порядка. Для обозначения предметных переменных обычно используются строчные буквы из конца латинского алфавита (z, y, x, ...)
предметная константа ИППП
один из символов алфавита исчисления предикатов первого порядка. Для обозначения предметных констант обычно используются строчные буквы из начала латинского алфавита (a, b, c, ...)
терм ИППП
Предметная переменная или предметная константа или m-местная функциональная буква ИППП, за которой в круглых скобках следует список из m термов (через запятую)
элементарная формула ИППП
атом ИППП
n-местная предикатная буква ИППП, за которой в круглых скобках следует список n термов (через запятую)
формула ИППП
правильно построенная формула ИППП
п.п.ф. ИППП
Элементарная формула или выражение, скомпонованное из формул, символов конъюнкции, дизъюнкции, импликации и отрицания, кванторов общности и существования, круглых скобок и запятой с использованием набора синтаксических правил
литерал ИППП
область действия квантора
часть формулы ИППП, содержащаяся в круглых скобках, следующих непосредственно за квантором
свободная предметная переменная ИППП
Предметная переменная ИППП, не находящаяся в области действия какого-либо квантора формулы
связанная предметная переменная ИППП
Предметная переменная ИППП, находящаяся в области действия какого-либо квантора формулы
незамкнутая формула ИППП
замкнутая формула ИППП
Формула ИППП, все предметные переменные которой находятся в области действия кванторов
аксиомы ИППП
Бесконечное множество формул ИППП, задаваемое двенадцатью схемами
правило вывода в ИППП
Отношение на формулах ИППП, позволяющее расширить множество выводимых формул
правило заключения
modus ponens
Одно из базовых правил вывода в ИППП
правило обобщения
правило введения квантора всеобщности
Одно из базовых правил вывода в ИППП
правило введения квантора существования
Одно из базовых правил вывода в ИППП
правило подстановки
Одно из базовых правил вывода в ИППП
правило переименования связанных переменных
Одна из теорем ИППП, используемых в качестве дополнительных правил вывода в ИППП
правило переименования свободных переменных
Одна из теорем ИППП, используемых в качестве дополнительных правил вывода в ИППП
теорема дедукции
Одна из теорем ИППП, используемых в качестве дополнительных правил вывода в ИППП
правило введения отрицания
Одна из теорем ИППП, используемых в качестве дополнительных правил вывода в ИППП
доказательство от противного
метод доказательства теорем в ИППП, основанный на правиле введения отрицания
эквивалентность формул ИППП
эквивалентность п.п.ф. ИППП
Свойство формул ИППП быть синонимами
интерпретация ИППП
Трактование формул ИППП как утверждений, характеризующих реальную предметную область. При этом: предметная константа ИППП соответствует конкретному объекту предметной области; предметная переменная может принимать значение любого объекта; предикатная буква соответствует отношению на объектах предметной области; функциональная буква — операции на объектах области
удовлетворимость множества формул
Ситуация, когда каждая п.п.ф. (интерпретируемая как высказывание) в некотором множестве п.п.ф. является истинной при одной и той же подстановке предметных констант на места предметных переменных
логическое следование
Некоторая п.п.ф. F логически следует из множества Ф п.п.ф., если каждая подстановка предметных констант, удовлетворяющая Ф, также удовлетворяет и F
логичная формальная система
Формальная система, для которой любая п.п.ф., выводимая из множества п.п.ф. с помощью ее правил вывода, также логически следует из этого множества
полная формальная система
Формальная система, все теоремы которой также логически следуют из множества формул, являющихся ее аксиомами
дизъюнкт в ИППП
предложение в ИППП
Формула ИППП, представляющая собой дизъюнкцию литералов
правило резолюции
резольвента
Результат применения правила резолюции к двум родительским формулам
унификация
Процесс подстановки термов на места предметных переменных в формулах ИППП с целью приведения этих формул к единому виду
метод резолюции
опровержение на основе резолюции
Метод доказательства теорем в ИППП, основанный на систематическом использовании правила резолюции для достижения пустой резольвенты