ВУЗ: Не указан
Категория: Не указан
Дисциплина: Не указана
Добавлен: 29.11.2023
Просмотров: 85
Скачиваний: 1
СОДЕРЖАНИЕ
1. Традиционная логика (Элементы силлогистики)
Схема классического представления связи между теорией, эмпиризмом, индукцией и дедукцией.
Множество А состоит из элементов: a1, a2, a3, …, an.
Все элементы от a3 до an также имеют признак В
Следовательно Все элементы множества А имеют признак В.
Схема неполной индукции: Множество А состоит из элементов: a1, a2, a3, … ak, … an.
Все элементы от a3 до ak также имеют признак B
Следовательно Вероятно, ak+1 и остальные элементы множества А имеют признак В.
Определение дедукции и дедуктивного метода
Понятие «силлогистика» и «силлогизм»
Общие правила простого категорического силлогизма (Википедия)
Классификация высказываний (суждений, пропозиций)
Правильные модусы простого категорического силлогизма
Ни одна рептилия не имеет меха. E
Некоторые домашние животные — котята. I
Некоторые домашние животные — игривые. I
Ни одна домашняя работа не весела. E
Некоторое чтение — домашняя работа. I
Фигуры условно-категорического силлогизма
Условно-категорический силлогизм
2. Основные положения исчислений
2.1. Определение формальной системы (исчисления)
Определение формальной системы
Формальные языки и формальные грамматики
Системы аксиом исчисления высказываний
Правила вывода исчисления высказываний
2.3. Методы доказательства теорем
С помощью логических преобразований
Методы доказательства теорем. Метод Вонга
Пусть дана клауза в своей наиболее общей форме:
Пример доказательства методом Вонга
1. Запишем формулу связи импликации и выводимости логической формулы:
4.Поскольку данная формула выводима (знак ), верна формула
следовательно, отрицание (А&B&C&…Ф)=F.
Алгоритм вывода по методу резолюции
Шаг 1: принять отрицание заключения, т.е. ¬Ф,
Шаг 2: привести все формулы посылок и отрицания заключения в КНФ,
Шаг 3: сформировать множество К дизъюнктов всех посылок и отрицания заключения: K = {D1, D2, …, Dk},
Дизъюнктом Хорна называется дизъюнкт, содержащий не более одного положительного литерала.
Дизъюнкт ровно с одним положительным литералом – определенный дизъюнкт.
Дизъюнкт – ровно с одним отрицательным литералом – целевой дизъюнкт.
Язык логического программирования Prolog
% Some simple test Prolog programs
% --------------------------------
% 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 example queries go here, e.g.
3. Исчисление предикатов первого порядка
Предикаты могут принадлежать к следующим семантическим типам:
Логические операции над предикатами
Операции связывания предикатов
Пример 1: «Всякий человек смертен» - х (Человек(х) Смертен(х))
Пример 2: «Всякий студент изучает какую-нибудь предмет» - х (Студент(х) у Наука(у)&Изучает(х,у))
Пример 3: «Квадрат любого четного числа больше 1»- х(Четное_число(х)>(Квадрат(х),1)).
Примеры использования кванторов
3.2. Определение формальной системы предикатов первого порядка
Алфавит формальной системы Исчисление предикатов
Введем понятие формулы в исчислении предикатов:
Предваренная нормальная форма формулы исчисления предикатов
Алгоритм приведения к предваренной нормальной форме
Пример приведения к предваренной нормальной форме
Пример получения сколемовской стандартной формы
∀x ∃ y∀t ∃q (P(x) & (¬Q(t, y) & ¬ R(a, t, q)).
Пример. Найти НОУ для W = {P(y, g(z), f(x)), P(a, x, f(g(y)))}.
2) так как W0 не является одноэлементным множеством, то перейти к пункту 3.
4) 1 =0{а/у} = {а/у} = {а/у}.
W1= W0 {а/у} = { P(a, g(z), f(x)), P(a, x, f(g(a)))}.
5) так как W1 опять неодноэлементно, то множество рассогласований будет {g(z),x}, т. е. {g(z)/x}.
6) 2 =1{g(z)/x} = {а/у, g(z)/x},
W2= W1 { g(z)/x } = { P(a, g(z), f(g(z))), P(a, g(z), f(g(a)))}.
8) 3 =2{z, a} = {а/у, g(z)/x, a/z},
W3= W2 {a/z } = { P(a, g(a), f(g(a))), P(a, g(a), f(g(a)))}= { P(a, g(a), f(g(a)))},
Пример слабого силлогизма
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 является декларативным языком программирования: логика программы выражается в терминах отношений, представленных в виде фактов и правил.
- Для того чтобы инициировать вычисления, выполняется специальный запрос к базе знаний, на которые система логического программирования генерирует ответы «истина» и «ложь».
- Для обобщённых запросов с переменными в качестве аргументов созданная система Пролог выводит конкретные данные в подтверждение истинности обобщённых сведений и правил вывода.