Совокупность абстрактных объектов (объектов, никак не связанных с реальным миром), в которой представлены правила оперирования цепочками символов в исключительно синтаксической трактовке без учета какого-либо смыслового содержания

Конечное множество символов, доступных для построения формул формальной системы

Линейная цепочка, построенная из символов алфавита формальной системы с использованием некоторого набора синтаксических правил

Формула формальной системы, выделенная разработчиком формальной системы

Отношение на множестве правильно построенных формул формальной системы

Одна из формул формальной системы, фигурирующих в правиле вывода

Одна из формул формальной системы, фигурирующих в правиле вывода

Формула формальной системы, являющаяся заключением некоторого правила вывода

Правило вывода в формальной системе, применяемое к формулам формальной системы как единому целому

Правило вывода в формальной системе, применяемое к любой отдельной части формулы формальной системы при условии, что эта часть сама является формулой формальной системы

Последовательность формул формальной системы такая, что каждая формула в ней непосредственно выводима из подмножества множества формул, являющегося объединением исходного множества формул, множества аксиом и ранее выведенных формул

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

Формула формальной системы, являющаяся результатом доказательства

Формальная система, для которой существует эффективная процедура, позволяющая для любой формулы определить, является ли данная формула теоремой или нет

Формальная система, используемая для представления знаний в системах искусственного интеллекта

Конечное множество символов, используемых для построения формул ИППП. Состоит из предметных переменных, предметных констант, n-местных предикатных букв, m-местных функциональных букв, символов конъюнкции, дизъюнкции, импликации и отрицания, кванторов общности и существования, круглых скобок и запятой

один из символов алфавита исчисления предикатов первого порядка. Для обозначения предикатных букв обычно используются прописные буквы из середины латинского алфавита (P, Q, R, ...)

один из символов алфавита исчисления предикатов первого порядка. Для обозначения функциональных букв обычно используются строчные буквы из середины латинского алфавита (f, g, h, ...)

один из символов алфавита исчисления предикатов первого порядка. Для обозначения предметных переменных обычно используются строчные буквы из конца латинского алфавита (z, y, x, ...)

один из символов алфавита исчисления предикатов первого порядка. Для обозначения предметных констант обычно используются строчные буквы из начала латинского алфавита (a, b, c, ...)

Предметная переменная или предметная константа или m-местная функциональная буква ИППП, за которой в круглых скобках следует список из m термов (через запятую)

n-местная предикатная буква ИППП, за которой в круглых скобках следует список n термов (через запятую)

Элементарная формула или выражение, скомпонованное из формул, символов конъюнкции, дизъюнкции, импликации и отрицания, кванторов общности и существования, круглых скобок и запятой с использованием набора синтаксических правил

Элементарная формула ИППП или ее отрицание

часть формулы ИППП, содержащаяся в круглых скобках, следующих непосредственно за квантором

Предметная переменная ИППП, не находящаяся в области действия какого-либо квантора формулы

Предметная переменная ИППП, находящаяся в области действия какого-либо квантора формулы

Формула ИППП, содержащая свободные вхождения предметной переменной

Формула ИППП, все предметные переменные которой находятся в области действия кванторов

Бесконечное множество формул ИППП, задаваемое двенадцатью схемами

Отношение на формулах ИППП, позволяющее расширить множество выводимых формул

Одно из базовых правил вывода в ИППП

Одно из базовых правил вывода в ИППП

Одно из базовых правил вывода в ИППП

Одно из базовых правил вывода в ИППП

Одна из теорем ИППП, используемых в качестве дополнительных правил вывода в ИППП

Одна из теорем ИППП, используемых в качестве дополнительных правил вывода в ИППП

Одна из теорем ИППП, используемых в качестве дополнительных правил вывода в ИППП

Одна из теорем ИППП, используемых в качестве дополнительных правил вывода в ИППП

метод доказательства теорем в ИППП, основанный на правиле введения отрицания

Свойство формул ИППП быть синонимами

Трактование формул ИППП как утверждений, характеризующих реальную предметную область. При этом: предметная константа ИППП соответствует конкретному объекту предметной области; предметная переменная может принимать значение любого объекта; предикатная буква соответствует отношению на объектах предметной области; функциональная буква — операции на объектах области

Ситуация, когда каждая п.п.ф. (интерпретируемая как высказывание) в некотором множестве п.п.ф. является истинной при одной и той же подстановке предметных констант на места предметных переменных

Некоторая п.п.ф. F логически следует из множества Ф п.п.ф., если каждая подстановка предметных констант, удовлетворяющая Ф, также удовлетворяет и F

Формальная система, для которой любая п.п.ф., выводимая из множества п.п.ф. с помощью ее правил вывода, также логически следует из этого множества

Формальная система, все теоремы которой также логически следуют из множества формул, являющихся ее аксиомами

Формула ИППП, представляющая собой дизъюнкцию литералов

Правило вывода в ИППП, применяемое к формулам ИППП, имеющим вид предложений

Результат применения правила резолюции к двум родительским формулам

Процесс подстановки термов на места предметных переменных в формулах ИППП с целью приведения этих формул к единому виду

Метод доказательства теорем в ИППП, основанный на систематическом использовании правила резолюции для достижения пустой резольвенты