Составляющие формальной системы. Язык формальной теории. Синтаксис формального языка, отношение между формулой и подформулой, сложные и атомарные формулы (стр. 6 )

В результате применения метода резолюций к двум хорновским дизъюнктам с заголовками вновь получается хорновский дизъюнкт с заголовком. Известно, что пустой дизъюнкт не имеет заголовка. Следовательно, если все дизъюнкты имеют заголовки, то из них могут быть получены только дизъюнкты с заголовками. Таким образом, для того чтобы из исходных дизъюнктов, отрицая доказываемое высказывание, можно было бы вывести пустой дизъюнкт, необходимо наличие, по крайней мере, одного дизъюнкта без заголовка. Если среди исходных имеется несколько дизъюнктов без заголовка, то доказательство каждого нового дизъюнкта методом резолюций может быть преобразовано в доказательство, в котором используется не более чем один дизъюнкт без заголовка. Если пустой дизъюнкт следует из заданного множества исходных, то он следует и из его подмножества, содержащего дизъюнкты с заголовками и не более одного дизъюнкта без заголовка. Любая задача, которая может быть выражена с помощью хорновских дизъюнктов, должна иметь только один дизъюнкт без заголовка (целевой); все остальные дизъюнкты должны быть с заголовками (гипотезы). Хорновские дизъюнкты были выбраны в качестве основы для создания программных систем автоматического доказательства теорем.

Моделью называется интерпретация, которая удовлетворяет множеству предикатных выражений S для всех значений переменных. Существует несколько определений минимальной модели. Минимальная модель - модель, для которой не существует подмоделей, удовлетворяющих множеству выражений S при всех значениях переменных.

24.  Унификация. Унифицирующая подстановка, унификатор. Наибольший общий унификатор.

Задача унификации: По двум описаниям X и Y определить, можно ли найти объект Z, который удовлетворяет обоим описаниям. Обычно уточняется как задача нахождения по данным двум термам, содержащим переменные, такой подстановки термов вместо переменных, которая превратила бы исходные термы в идентичные. В том случае, когда такая подстановка для термов существует, она называется унификатором, а термы называются унифицируемыми. Если термы унифицируемы, то у них может быть много унификаторов, но всегда существует и единствен наибольший общий унификатор, из которого с помощью композиций подстановок можно получить все другие унификаторы. Этот унификатор, обладает таким свойством, что для всякого другого унификатора q для того же множества выражений существует такая подстановка t, что q = zt, где zt - композиция подстановок r и t.

Унификация (сопоставление) является основной операцией в методе резолюций. Пусть даны два дизъюнкта и , принадлежащие множеству S. Предположим, что литеры l1 и l2 являются унифицируемыми, т. е. обладают общей фундаментальной конкретизацией. Из каждой пары фундаментальных конкретизаций и ,

таких, что l1'=l1'=l1' получается резольвента . Каждый дизъюнкт такого типа является логическим следствием из С1 и С2 . Задача состоит в том, чтобы найти такой дизъюнкт R, фундаментальные конкретизации которого были бы в точности конкретизациями того же самого типа, как и для R' . Обозначим через lU наибольшую нижнюю границу пары {l1 , l2} относительно порядка < . Наиболее общим унификатором литер l1 и l2, ,будем называть подстановку sU, такую, что sU [l1]= sU [l2]=lU. Резольвентным дизъюнктом (резольвентой) R с требуемым свойством будет следующее выражение: .

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

25.  Прикладные исчисления предикатов и их отличие от чистого исчисления предикатов и теорий второго порядка и выше.

Предикат – высказывательная функция, определенная на некотором множестве М, т. е. такая n-местная функция Р, которая каждому упорядоченному набору <a1,a2, …, an> элементов множества М сопоставляет некоторое высказывание, обозначаемое P(a1,a2, …, an).

Исчисление предикатов — формальное исчисление, допускающее высказывания относительно переменных, фиксированных функций, и предикатов. Расширяет логику высказываний.

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

Логика второго порядка — расширяет логику первого порядка, позволяя проводить квантификацию общности и существования не только над атомами, но и над предикатами. Нечёткое множество второго порядка может быть определено следующим образом, т. е. областью определения для него выступает множество первого порядка.

Таким образом, областью определения множества следующего порядка является множество предыдущего порядка. Логика второго порядка не упрощается к логике первого порядка.

26.  Исчисление с равенством. Язык, аксиоматика, правила вывода, свойства отношения равенства.

Предикат – высказывательная функция, определенная на некотором множестве М, т. е. такая n-местная функция Р, которая каждому упорядоченному набору <a1,a2, …, an> элементов множества М сопоставляет некоторое высказывание, обозначаемое P(a1,a2, …, an).

Исчисление предикатов — формальное исчисление, допускающее высказывания относительно переменных, фиксированных функций, и предикатов. Расширяет логику высказываний.

Исчисление с равенством – исчисление, которое описывает, формализует свойства бинарного отношения эквивалентности (равенства).

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

Аксиоматика исчисления с равенством может быть выстроена на основе аксиоматики логики предикатов с добавлением следующей аксиомной схемы и аксиомы. Здесь формула получена из формулы заменой некоторых свободных вхождений переменной χ на λ.

Теоремами исчисления с равенством являются свойства симметричности и транзитивности соответственно.

Кроме правила прямого заключения в логике предикатов используются ещё два правила вывода. Для любого множества формул G языка логики предикатов, для любых формул α (χ) и β (χ) , содержащих свободную переменную χ , и любой формулы γ , которая не содержит свободной переменной χ , справедливы следующие правила (правило обобщения и конкретизации соответственно).

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

27.  Исчисления частичного и линейного порядка. Язык, аксиоматика, правила, теоремы.

Предикат – высказывательная функция, определенная на некотором множестве М, т. е. такая n-местная функция Р, которая каждому упорядоченному набору <a1,a2, …, an> элементов множества М сопоставляет некоторое высказывание, обозначаемое P(a1,a2, …, an).

Исчисление предикатов — формальное исчисление, допускающее высказывания относительно переменных, фиксированных функций, и предикатов. Расширяет логику высказываний.

Исчисление порядка – исчисление, которое описывает, формализует свойства бинарных отношений порядка. В дополнение к аксиома логики исчисления с равенством, следующие две аксиомы используются во всех исчислениях порядка, описывающих отношение (предпорядка) порядка, специальный символ для обозначения которого вводится, как предикатная константа, в алфавит языка исчисления порядка. Этими аксиомами соответственно являются аксиома антисимметричности и аксиома транзитивности. Ђ.

Исчисление частичного порядка:

Включение в аксиоматику исчисления порядка (для отношения Ђ) следующей аксиомы приводит к исчислению частичного порядка.

В качестве правил вывода используются все правила исчисления предикатов.

Исчисление линейного порядка:

Включение в аксиоматику исчисления порядка (для отношения Ђ)

следующей аксиомы приводит к исчислению полного порядка.