Лекция8_9Основные положения исчислений. Основные положения исчислений Учебные вопросы

Название	Основные положения исчислений Учебные вопросы
Дата	24.05.2023
Размер	2.84 Mb.
Формат файла
Имя файла	Лекция8_9Основные положения исчислений.pptx
Тип	Документы #1155267

Основные положения исчислений

Учебные вопросы

Традиционная логика (Элементы силлогистики)
Основные положения исчислений
Исчисление предикатов первого порядка

1. Традиционная логика (Элементы силлогистики)

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

Индуктивный метод

Индуктивный (от лат. inductio - наведение) метод - это такой метод познания, при котором общий вывод делается из частных посылок. В процессе познания наше мышление совершает восхождение от частного, единичного, конкретного к общему.
В полной индукции мы заключаем от полного перечисления видов известного рода ко всему роду; очевидно, что при подобном способе умозаключения мы получаем вполне достоверное заключение, которое в то же время в известном отношении расширяет наше познание; этот способ умозаключения не может вызвать никаких сомнений. Отождествив предмет логической группы с предметами частных суждений, мы получим право перенести определение на всю группу.
Метод обобщения признаков некоторых элементов для всего множества, в который они входят. Неполная индукция не является доказательной с точки зрения формальной логики, может привести к ошибочным заключениям. Вместе с тем, неполная индукция является основным способом получения новых знаний. Доказательная сила неполной индукции ограничена, заключение носит вероятностный характер, требует приведения дополнительного доказательства.

Схема полной индукции

Множество А состоит из элементов: a1, a2, a3, …, an.

Все элементы от a3 до an также имеют признак В

Следовательно Все элементы множества А имеют признак В.

Пример метода полной индукции

Схема неполной индукции

Схема неполной индукции: Множество А состоит из элементов: a1, a2, a3, … ak, … an.

Все элементы от a3 до ak также имеют признак B

Следовательно Вероятно, ak+1 и остальные элементы множества А имеют признак В.

Пример неполной индукции

Сегодня на лекции интересно
Вчера на лекции было интересно
На первой лекции было интересно
Вывод всегда на лекции интересно

Определение дедукции и дедуктивного метода

Дедукция (лат. deductio — выведение) — метод мышления, при котором частное положение логическим путём выводится из общего, вывод по правилам логики; цепь умозаключений (рассуждений), звенья которой (высказывания) связаны отношением логического следования.
Началом (посылками) дедукции являются аксиомы или просто гипотезы, имеющие характер общих утверждений («общее»), а концом — следствия из посылок, теоремы («частное»). Если посылки дедукции истинны, то истинны и её следствия. Дедукция — основное средство доказательства. Противоположно индукции.

Пример дедуктивного умозаключения:

Все люди смертны.
Сократ — человек.
Следовательно, Сократ смертен.

Понятие «силлогистика» и «силлогизм»

Силлогистика (греч. σιλλογισtικόσ — выводящий умозаключение) — теория логического вывода, исследующая умозаключения, состоящие из категорических высказываний (суждений). В силлогистике рассматриваются, выводы, заключения из одной посылки (непосредственные умозаключения) «сложные силлогизмы», или полисиллогизмы, имеющие не менее трёх посылок). Однако основное внимание силлогистика уделяет теории категорического силлогизма, имеющего ровно две посылки и одно заключение указанного вида.
Умозаключение (силлогизм) – это форма мышления или логическое действие, в результате которого из одного или нескольких известных и определенным образом связанных суждений получается новое суждение, в котором содержится новое знание
Правильным умозаключением называется такое умозаключение, значение которого истинно всякий раз, когда истинны его гипотезы. Правила вывода являются правильными умозаключениями или силлогизмами. Силлогизм записывается в виде:

H1, H2,…, Hn гипотезы
C заключение

Простой категорический силлогизм (др.-греч. συλ-λογισμός «подытоживание, подсчёт, умозаключение» от συλ- (συν-) «вместе» + λογισμός «счёт, подсчёт; рассуждение, размышление») — дедуктивное умозаключение, состоящее из трёх простых атрибутивных высказываний: двух посылок и одного заключения.

Формы силлогизмов

Силлогизмы

Категорический силлогизм

Условно-категорически силлогизм (одна посылка-условное суждение, другая и следствие категорические суждения

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

Разделительно-категорический силлогизм (одна посылка разделительная, другая –категорическое суждение, заключение-категорическое суждение)

Категорический силлогизм

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

Р – большой термин;
М – средний термин;
S – малый термин.

Каждое высказывание объединяет два термина из трех.
Посылки силлогизма разделяются на бо́льшую (которая содержит предикат заключения) и меньшую (которая содержит субъект заключения). По положению среднего термина силлогизмы делятся на фигуры, а последние по логической форме посылок и заключения — на модусы.
Модусы – набор суждений, входящих в силлогизм

Пример силлогизма

Всякий человек смертен
Сократ – человек
Следовательно Сократ смертен

beingman(sokrat).

beingimmortal(X):-beingman(X).

Быть человеком

Быть смертным

Быть Сократом

Общие правила простого категорического силлогизма (Википедия)

Правила терминов

В каждом силлогизме должно быть ровно три термина.
Средний термин должен быть распределён хотя бы в одной из посылок.
Крайний термин, не распределённый в посылке, не должен быть распределён в заключении.

Правила посылок

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

Фигуры силлогизма

	Фигура 1	Фигура 2	Фигура 3	Фигура 4
Бо́льшая посылка:	M—P	P—M	M—P	P—M
Меньшая посылка:	S—M	S—M	M—S	M—S
Заключение:	S—P	S—P	S—P	S—P

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

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

Например, в силлогизме:

Все небесные тела движутся.

Все планеты — это небесные тела.

------------

Все планеты движутся.

Классификация высказываний (суждений, пропозиций)

A — от лат. affirmo (утверждать, уверять— Общие («Все люди смертны»)
I — от лат. affirmo — Частноутвердительные («Некоторые люди — студенты»)
E — от лат. nego — Общеотрицательные («Ни один из китов не рыба»)
O — от лат. nego (отрицать)— Частноотрицательные («Некоторые люди не являются студентами»)
Примечание. Для условного буквенного обозначения высказываний используются гласные из латинских слов affirmo (я утверждаю, говорю да) и nego (я отрицаю, говорю нет).

Связь между высказываниями

Типы высказываний (суждений)

Общеутвердительное суждение : «Все предметы класса S обладают свойством P». («Все S суть P».)

Символически: SaP — с первой буквой affirmo -A;

2. Общеотрицательного суждения «Ни один предмет класса S не обладает свойством P». («Ни один S не есть P».)

Символически: SeP — с первой гласной буквой nego - E;

3. Частноутвердительного суждения: «Некоторые предметы класса S обладают свойством P». («Некоторые S суть P».)

Символически: SiP — с буквой i слова affirm - I;

4. Частноотрицательного суждения: «Некоторые предметы класса S не обладают свойством P». («Некоторые S не суть P».)

Символически: SoP — с буквой o слова nego - O.

Логический квадрат

Логические связи между высказываниями

Контрарность –противоположность (исключается их одновременная истинность, но не исключается их одновременная ложность. Высказывания А, Е не могут быть одновременно истинными, но могут быть одновременно ложными. Поэтому они называются противоречивыми.

Контрадикторность – противоречие (одно является отрицанием другого. Высказывания А, О; I, E – являются отрицаниями друг друга;

Субконтрарность –частичное совпадение, суждения могут быть одновременно истинными, но не могут быть одновременно ложны. Высказывания I, O могут быть одновременно истинными, но не могут быть одновременно ложными. Поэтому они называются антипротиворечивыми.

Подчинение . Высказывания I, O являются следствием высказываний А, Е.

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

Фигура 1	Фигура 2	Фигура 3	Фигура 4
Barbara AAA	Cesare EAE	Darapti AAI	Bramantip AAI
Celarent EAE	Camestres AEE	Disamis EIO	Camenes AEE
Darii AII	Festino EIO	Datisi IAI	Dimaris IAI
Ferio EIO	Baroco AOO	Felapton OAO	Fesapo EAO
Celaront EAO	Camestros AEO	Bocardo AII	Fresison EII
Barbari AAI	Cesaro EAO	Ferison EAO	Camenos AEO

Для каждой фигуры 4^3=64 возможных силлогизма. Всего 4^4=256 силлогизмов. только 24 (19 сильных и 5 слабых) дают достоверные выводы: из истинных посылок выводится необходимо истинное заключение. Заключение сделанное по остальным модусам может оказаться как истинным так и ложным; истинность будет зависеть исключительно от конкретного содержания посылок и заключения.

Курсивом выделены слабые модусы — модусы которые содержат частное заключение при возможности общего.

Примеры правильных модусов

Barbara

Все животные смертны. A

Все люди — животные. A

Все люди смертны. A

Celarent

Ни одна рептилия не имеет меха. E

Все змеи — рептилии. A

Ни одна змея не имеет меха. E

Darii

Все котята игривые. A

Некоторые домашние животные — котята. I

Некоторые домашние животные — игривые. I

Ferio

Ни одна домашняя работа не весела. E

Некоторое чтение — домашняя работа. I

Некоторое чтение не весело. O

Zesare

Ни одна здоровая еда не полнит. E

Все торты полнят. A

Ни один торт не здоровая еда. E

Camestres

Все лошади имеют вздутие живота. A

Ни один человек не имеет вздутия живота. E

Ни один человек не лошадь. E

Festino

Ни один ленивый человек не сдаёт экзамены. E

Некоторые студенты сдают экзамены. I

Некоторые студенты не ленивы. O

Baroco

Все информативные вещи полезны. A

Некоторые сайты не полезны. O

Некоторые сайты не информативны. O

Обозначение умозаключения

Пример слабого силлогизма

Barbari

Все животные смертны. A

Все люди — животные. A

некоторые люди смертны. I

Диаграммы Эйлера

Фигуры условно-категорического силлогизма

ФИгура	1 фигура	2 фигура	3 фигура	4 фигура
Условное суждение	A->B	A->B	A->B	A->B
Категорическое суждение	A	B	Не B	Не A
Категорическое суждение	B	? A (не достоверное суждение)	Не A	?Не B (не достоверное суждение)

Условно-категорический силлогизм

2. Основные положения исчислений

2.1. Определение формальной системы (исчисления)

Определение формальной системы

Формальная система (исчисление, дедуктивная система, формальная теория) определяется четверкой
где T – алфавит формальной системы;
F –множество формул (правильно построенных формул), построенных с помощью набора синтаксических правил из алфавита;
A – множество формул (аксиом);
R – множество правил вывода.
Язык логики высказываний определяется грамматикой

Формальные языки и формальные грамматики

Формальная грамматика или просто грамматика в теории формальных языков — способ описания формального языка, то есть выделения некоторого подмножества из множества всех слов некоторого конечного алфавита. Различают порождающие и распознающие (или аналитические) грамматики — первые задают правила, с помощью которых можно построить любое слово языка, а вторые позволяют по данному слову определить, входит ли оно в язык или нет.
Конечное множество символов называется алфавитом, символы ai буквами, последовательность символов – словом. Множество слов A*

Порождающая грамматика

Нотация Бекуса-Наура

Форма Бэкуса — Наура (Бэкуса — Наура форма) — формальная система описания синтаксиса, в которой одни синтаксические категории последовательно определяются через другие категории.

<определяемый символ> ::= <посл.1> | <посл.2> | . . . | <посл.n>

Пример нотаций Бекуса

https://swish.swi-prolog.org/example/render_graphviz.swinb

Вывод формулы

Основные понятия исчислений

Требования к аксиомам

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

Теорема о неполноте Геделя

В любой непротиворечивой, формальной системе, содержащей минимум математики («+», «*», кванторы и обычные правила обращения с ними) найдется формально неразрешимое суждение т.е. такая замкнутая формула А, что ни А, ни А не являются выводимыми в системе.
Эта теорема знаменовала неудачу первоначального понимания программы, предусматривающей полную формализацию всей существующей математики, и обоснования полученной формальной системы путем финитного доказательства ее непротиворечивости. Теорема показала, что даже если финитными считаются все средства формализованной арифметики, этого не хватит для доказательства непротиворечивости арифметики.

2.2 Исчисление высказываний

Логика высказываний, пропозициональная логика (лат. propositio — «высказывание» ) или исчисление высказываний, также логика нулевого порядка — это раздел символической логики, изучающий сложные высказывания, образованные из простых, и их взаимоотношения. В отличие от логики предикатов, пропозициональная логика не рассматривает внутреннюю структуру простых высказываний, она лишь учитывает, с помощью каких союзов и в каком порядке простые высказывания сочленяются в сложные

Состав формальной системы

где T – алфавит формальной системы;
F –множество формул (правильно построенных формул), построенных с помощью набора синтаксических правил из алфавита;
A – множество формул (аксиом);
R – множество правил вывода.

Исчисление высказываний

Системы аксиом исчисления высказываний

Правила вывода исчисления высказываний

2.3. Методы доказательства теорем

Методы доказательства теорем

С помощью таблицы истинности
С помощью логических преобразований
Метод Вонга
Метод резолюции

С помощью таблицы истинности

A	B	A->B	A->B,A	(A->B,A)->B
F	F	T	F	T
F	T	T	F	T
T	F	F	F	T
T	T	T	T	T

С помощью логических преобразований

С помощью таблицы истинности

A	B	B->A	A->(B->A)
F	F	T	T
F	T	F	T
T	F	T	T
T	T	T	T

Методы доказательства теорем. Метод Вонга

Пусть дана клауза в своей наиболее общей форме:

В1, В2, …, Вn  А1, А2, …,Am

Шаг 1. Снятие отрицаний с посылок и заключений. С этой целью нужно опустить знак отрицаний у Ai и Bj и перенести их в противоположные стороны относительно символа .

Шаг 2. Если слева от символа  встречается конъюнкция, а справа дизъюнкция, то их следует заменить на запятые.

Шаг 3. Если после предыдущих шагов оказалось, что связкой, расположенной слева от, является дизъюнкция, а справа – конъюнкция, то образуются две новые клаузы, каждая из которых содержит одну из двух подформул, заменяющих исходную клаузу. Шаг 4. Если одна и та же буква находится с обеих сторон символа, то такая строка считается доказанной. Исходная клауза является теоремой, если все ветви оканчиваются истинными клаузами. В противном случае переходим к шагу 3.

Пример доказательства методом Вонга

Пример доказательства

Метод резолюции

1. Запишем формулу связи импликации и выводимости логической формулы:

 (А&В&С&…Ф)

2.Избавимся от импликации:

 ((А&В&С&…)Ф)

3.Применим закон де Моргана:

 ( (А&В&С&…)Ф))

4.Поскольку данная формула выводима (знак ), верна формула

 (А&В&С&…Ф)=T,

следовательно, отрицание (А&B&C&…Ф)=F.

Алгоритм вывода по методу резолюции

Шаг 1: принять отрицание заключения, т.е. ¬Ф,

Шаг 2: привести все формулы посылок и отрицания заключения в КНФ,

Шаг 3: сформировать множество К дизъюнктов всех посылок и отрицания заключения: K = {D1, D2, …, Dk},

Шаг 4: выполнить анализ пар множества K по правилу: если существует пара элементов, содержащих контрарные атомы, то соединить эту пару логической связкой дизъюнкции и сформировать новый дизъюнкт - резольвенту, исключив из нее контрарные атомы, Шаг 5: если в результате соединения дизъюнктов будет получена пустая резольвента – аналог ложности формулы (обозначается ), то конец, т.к. доказательство подтвердило истинность заключения. Иначе включить резольвенту в множество дизъюнктов K и перейти к шагу 4. При этом по закону идемпотентности любой дизъюнкт и любую резольвенту можно использовать неоднократно, т.е. из множества К не следует удалять использованные в соединении дизъюнкты.

Силлогизм Modus ponens

Метод линейной резолюции

Дизъюнкты Хорна

Фразы Хорна. В прямом методе вывод проводился исходя из свойств связок и из того, что предметная область описывалась через импликацию, конъюнкцию, дизъюнкцию и отрицание.

Дизъюнктом Хорна называется дизъюнкт, содержащий не более одного положительного литерала.

Дизъюнкт ровно с одним положительным литералом – определенный дизъюнкт.

Дизъюнкт – ровно с одним отрицательным литералом – целевой дизъюнкт.

Этот способ удобен для представления человеком – специалистом, потому что ему проще выражать свои знания через высказывания ЕСЛИ…, ТО…. («ЕСЛИ температура >39, слабость и покраснение, ТО необходимо принять лекарство, лечь в постель и пить большое количество воды».

Язык Prolog (википедия)

Пролог уходит своими корнями в логику первого порядка, формальную логику , и в отличие от многих других языков программирования, Пролог задуман прежде всего как язык декларативного программирования.
Язык был разработан и реализован в Марселе, Франция, в 1972 году Аленом Кольмерауэром и Филиппом Русселем на основе процедурной интерпретации предложений Хорна Робертом Ковальски .
Пролог был одним из первых языков логического программирования и остается самым популярным из них сегодня, с несколькими доступными бесплатными и коммерческими реализациями. Язык использовался для доказательства теорем, экспертных систем , переписывания терминов , систем типов , и автоматизированного планирования , а также его первоначальной предполагаемой области использования, обработки естественного языка.
Современные среды Prolog поддерживают создание графических пользовательских интерфейсов, а также административные и сетевые приложения.

Язык логического программирования Prolog

Пролог (англ. Prolog) — язык и система логического программирования, основанные на языке предикатов математической логики дизъюнктов Хорна, представляющей собой подмножество логики предикатов первого порядка.

Prolog является декларативным языком программирования: логика программы выражается в терминах отношений, представленных в виде фактов и правил.

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

Дизъюнкты Хорна

% Some simple test Prolog programs

% --------------------------------

% Knowledge bases

loves(vincent, mia).

loves(marcellus, mia).

loves(pumpkin, honey_bunny).

loves(honey_bunny, pumpkin).

jealous(X, Y) :-

loves(X, Z),

loves(Y, Z).

/**

?- loves(X, mia).

?- jealous(X, Y).

*/

https://swish.swi-prolog.org/example/kb.pl#tabbed-tab-4

Prolog-program

% Constraint Logic Programming

:- use_module(library(dif)). % Sound inequality

:- use_module(library(clpfd)). % Finite domain constraints

:- use_module(library(clpb)). % Boolean constraints

:- use_module(library(chr)). % Constraint Handling Rules

:- use_module(library(when)). % Coroutining

%:- use_module(library(clpq)). % Constraints over rational numbers

% Your program goes here

x1.

x2.

x3:-x1.

/** Your example queries go here, e.g.

?- x3.

*/

https://swish.swi-prolog.org/p/%D0%98%D1%81%D1%87%D0%B8%D1%81%D0%BB%D0%B5%D0%BD%D0%B8%D0%B5.pl

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

3.1 Определение предиката

Понятие предиката

Предикат (лат. praedicatum «сказанное») в логике и лингвистике — сказуемое суждения, то, что высказывается (утверждается или отрицается) о субъекте. Предикат находится с субъектом в предикативном отношении и показывает наличие (отсутствие) у предмета некоторого признака.

Предикаты могут принадлежать к следующим семантическим типам:

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

Определение предиката

Классификация предикатов

Интерпретация предикатов

Логические операции над предикатами

Операции связывания предикатов

Примеры предикатов

Пример 1: «Всякий человек смертен» - х (Человек(х)  Смертен(х))

Пример 2: «Всякий студент изучает какую-нибудь предмет» - х (Студент(х)  у Наука(у)&Изучает(х,у))

Пример 3: «Квадрат любого четного числа больше 1»- х(Четное_число(х)>(Квадрат(х),1)).

Типы суждений (высказываний)

Все суждения классической логики могут быть представлены в логике предикатов первого порядка

Законы алгебры предикатов

Имя закона	Равносильные формулы
Коммутативности	∀x∀y(F(x, y))≡∀y∀x(F(x, y)) ∃x∃y(F(x, y))≡∃y∃x(F(x, y))
Дистрибутивности	∀x(F1(x))&∀x(F2(x))≡∀x(F1(x)&F2(x)) – для формул с кванторами всеобщности по одной переменной х ∃x(F1(x))∨∃x(F2(x))≡∃x(F1(x)∨F2(x)) – для формул с кванторами существования по одной переменной х
Идемпотентности	x(F(x))∨x(F(x))≡x(F(x)) x(F(x))&x(F(x))≡x(F(x)) x(F(x))∨x(F(x))≡x(F(x)) x(F(x))&x(F(x))≡x(F(x))
Исключения третьего	x(F(x))∨¬x(F(x))=и x(F(x))∨¬x(F(x))=и
Противоречия	x(F(x))&¬x(F(x))=л x(F(x))&¬x(F(x))=л
Отрицание кванторов	∀x(¬F(x))≡¬∃x(F(x)) ∀x(F(x))≡¬∃x(¬F(x)) ∃x(¬F(x))≡¬∀x(F(x)) ∃x(F(x))≡¬∀x(¬F(x))
Дополнения	¬(¬x(F(x)))≡ x(F(x)) ¬(¬x(F(x)))≡ x(F(x))

Примеры использования кванторов

3.2. Определение формальной системы предикатов первого порядка

Алфавит формальной системы Исчисление предикатов

Алфавит формальной системы.

x1, x2, …, xn, … – предметные переменные;
a1, a2, …, an, … – предметные константы;
A11, A22, …, Alm, P11,… – предикатные буквы;
f11, f22, …, flk,… – функциональные буквы.

В логике предикатов существует понятие терма:

Любую предметную переменную и предметную постоянную предиката называют термом - ti.
Если fi - функциональный символ и t1,t2,..., tn – его аргументы-термы, то fi(t1,t2,…,tn) также есть терм.
Никаких иных термов нет.

Формулы формальной системы

Введем понятие формулы в исчислении предикатов:

Если Pi – предикатный символ и t1,t2,...,tn – термы, то F=Pi(t1,t2,...,tn ) - элементарная формула.
Если F1 и F2 - формулы, то ¬F1, ¬F2, (F1&F2), (F1∨F2), (F1→F2), (F1↔F2) - также формулы.
Если F - формула, a x - предметная переменная, входящая в формулу F, то ∀x(F) и ∃x(F) - также формулы.
Никаких иных формул нет.

Аксиомы исчисления предикатов

Правила вывода

Правила для кванторов

Правила преобразования формул

3.3. Метод резолюции

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

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

Алгоритм приведения к предваренной нормальной форме

Пример приведения к предваренной нормальной форме

Преобразовать формулу:

∀x(P(x) & ∀y¬∃x(¬ Q(x, y) → ∀y (R(a, x, y))) )

Шаг 1. Исключим импликацию

∀x(P(x) & ∀y ¬∃x ((Q(x, y)  ∀y R(a, x, y)))

Шаг 2. Перенесем отрицание

∀x(P(x) & ∀y ∀ x (¬(Q(x, y)  ∀y R(a, x, y))) = ∀x(P(x) & ∀y ∀ x (¬Q(x, y) &¬ ∀y (R(a, x, y)))= ∀x(P(x) & ∀y ∀ x (¬Q(x, y) &∃y (¬ R(a, x, y))) )

Шаг 3.Переименуем связанную переменную x=t, y=q

∀x(P(x) & ∀y ∀ t (¬Q(t, y) & ∃q¬R(a, t, q)))

Перенесем кванторы влево

∀x ∀ y∀t ∃q (P(x) & (¬Q(t, y) & ¬ R(a, t, q)).

Алгоритм приведения к ССФ:

Шаг 1: представить формулу F в виде ПНФ, т. е. F=ℜx1ℜx2…ℜxn(M), где ℜi∈{∀, ∃}, а М=D1&D2&D3&…,
Шаг 2: найти в префиксе самый левый квантор существования и заменить его по правилу:
a) если квантор существования находится на первом месте префикса, то вместо переменной, связанной этим квантором, подставить в матрице всюду предметную постоянную, отличную от встречающихся постоянных, а квантор существования удалить,
b) если квантор существования находится на i-м месте префикса, т.е.∀x1∀x2…∀xi-1∃xi ..., то выбрать (i-1)- местную сколемовскую функцию f(x1, x2,..xi-1), отличную от функций матрицы М, и выполнить замену предметной переменной xi, связанной квантором существования, на функцию f(x1, x2,..., xi-1), а квантор существования из префикса удалить.
Шаг 3: найти в префиксе следующий слева квантор существования и перейти к исполнению шага 2, иначе конец.
Формулу ПНФ, полученную в результате введения сколемовских функций, называют сколемовской стандартной формой (ССФ). Преобразованная таким образом матрица может быть допущена к анализу истинности суждения по принципу резолюции

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

∀x ∃ y∀t ∃q (P(x) & (¬Q(t, y) & ¬ R(a, t, q)).

∀x ∀t ∃q (P(x) & (¬Q(t, f1(x)) & ¬ R(a, t, q)).
∀x ∀t (P(x) & (¬Q(t, f1(x)) & ¬ R(a, t, f2(x,t)).