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



страница4/11
Дата03.12.2012
Размер0.93 Mb.
ТипДокументы
1   2   3   4   5   6   7   8   9   10   11

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

Задача унификации: По двум описаниям 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 с требуемым свойством будет следующее выражение: .

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

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


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

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

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

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



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

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

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

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

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

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

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



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



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



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



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

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

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

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



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

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



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

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

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

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



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

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

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

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

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



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

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

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

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

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

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

  1. Исчисление с выводом по аналогии. Отношение подобия.

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

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

Правило прямого вывода (заключения) по аналогии формально может выглядеть так:



где σ – бинарное отношение подобия на множестве термов и формул.

Вывод по аналогии реализуется в рамках базы знаний. База знаний состоит из набора фактов и правил, записанных на линейном языке. Факты представлены предикатными формулами с указанными значениями аргументов; факты утверждают истинность заданной интерпретации предиката. Значением аргументов являются константы. Например: P(a,b).

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

Например: P(A,B) <- P(A,C); P(C,B).

Последнее равносильно:P(A,B)   P(A,C)   P(C,B)

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

Здесь формула α , имеющая свободное вхождение переменной χ , обозначена как α (χ) . Формула α (χ) не имеет свободных вхождений τ . Формула α (τ) получена заменой всех свободных вхождений переменной χ на τ .



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

Подобие - В метрических пространствах так же, как в n-мерных римановых, псевдоримановых и финслеровых пространствах подобие определяется как преобразование, переводящее метрику пространства в себя с точностью до постоянного множителя. Отношение подобия – отношение выполняющие данное преобразования.

  1. Исчисление арифметики. Язык, аксиоматика, правила, теоремы.

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

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

Исчисление арифметики описывает натуральные числа и закономерности операций над натуральными числами. В алфавит языка исчисления арифметики дополнительно вводятся классы следующих символов ,',0+,∗. Аксиоматика кроме аксиомных схем исчисления предикатов содержит шесть аксиом и одну аксиомную схему, формализующую метод математической индукции.



Теоремы: Примерами теорем исчисления арифметики являются следующие формулы.



  1. Теория алгоритмов. Понятие примитивно-рекурсивной функции.

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

Рекурси́вная фу́нкция (от лат. recursio — возвращение) — это числовая функция f(n) числового аргумента, которая в своей записи содержит себя же. Такая запись позволяет вычислять значения f(n) на основе значений , подобно рассуждению по индукции. Чтобы вычисление завершалось для любого n, необходимо, чтобы для некоторых n функция была определена нерекурсивно (например, для n = 0,1). Вот пример рекурсивной функции, дающей n-ое число Фибоначчи:



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

Определение понятия примитивно рекурсивной функции является индуктивным. Оно состоит из указания класса исходных примитивно рекурсивных функций и двух операторов (подстановки и примитивной рекурсии), позволяющих строить новые примитивно рекурсивные функции на основе уже имеющихся. К числу исходных примитивно рекурсивных функций относятся функции следующих трёх видов: 1) Нулевая функция O одного переменного, сопоставляющая любому натуральному числу значение 0. 2) Функция следования S одного переменного, сопоставляющая любому натуральному числу x непосредственно следующее за ним натуральное число x + 1. 3) Функции , где , от n переменных, сопоставляющие любому упорядоченному набору x1,...xn натуральных чисел число xm из этого набора.
1   2   3   4   5   6   7   8   9   10   11

Похожие:

Составляющие формальной системы. Язык формальной теории. Синтаксис формального языка, отношение между формулой и подформулой, сложные и атомарные формулы icon1 формальные теории 1 Основные положения
Мы рассмотрели две логических системы: алгебру высказываний и логику предикатов. Это было содержательное рассмотрение. Попытаемся...
Составляющие формальной системы. Язык формальной теории. Синтаксис формального языка, отношение между формулой и подформулой, сложные и атомарные формулы iconЗаконы (принципы) формальной логики Логическая культура. Значение логики. Язык логики. Семантические категории языка
Отношения между понятиями (сравнимые и несравнимые, совместимые и несовместимые понятия)
Составляющие формальной системы. Язык формальной теории. Синтаксис формального языка, отношение между формулой и подформулой, сложные и атомарные формулы iconФормальные теории
Язык формальной арифметики. Выразимость в этом языке любого разрешимого отношения. β-функция Гёделя
Составляющие формальной системы. Язык формальной теории. Синтаксис формального языка, отношение между формулой и подформулой, сложные и атомарные формулы iconСписок экзаменационных вопросов по курсу «Системное программное обеспечение»
Понятие формальной грамматики и языка. Выводимость. Язык, порождаемый грамматикой
Составляющие формальной системы. Язык формальной теории. Синтаксис формального языка, отношение между формулой и подформулой, сложные и атомарные формулы iconПлан занятий по онтологическому инжинирингу Введение в онтологический инжиниринг
Пропозициональная (ПЛ) или Булева логика (синтаксис: атомарные (пропозициональный символ P, Q, r и т д.) и сложные (на основе простых)...
Составляющие формальной системы. Язык формальной теории. Синтаксис формального языка, отношение между формулой и подформулой, сложные и атомарные формулы iconЭквивалентность двух определений элементарной формальной системы
«Исчисления и формальные системы» (стр. 267) и «Основания математической логики» (стр. 68). Ясно, что эти два определения в некотором...
Составляющие формальной системы. Язык формальной теории. Синтаксис формального языка, отношение между формулой и подформулой, сложные и атомарные формулы iconВычислительные Машины и Системы Математическое Обеспечение Вычислительных Систем Разработка формальной грамматики

Составляющие формальной системы. Язык формальной теории. Синтаксис формального языка, отношение между формулой и подформулой, сложные и атомарные формулы iconСинтаксис английского языка синтаксис
При всех существующих пониманиях предмета синтаксиса раздел соответствующей теории (языкознания, семиотики), занимающийся изучением...
Составляющие формальной системы. Язык формальной теории. Синтаксис формального языка, отношение между формулой и подформулой, сложные и атомарные формулы icon1. Синтаксис и семантика языков программирования. Алфавит языка Borland Pascal. Описание синтаксиса языка: синтаксические диаграммы
Синтаксис языка совокупность правил, определяющих допустимые конструкции (слова, предложения) языка, его форму
Составляющие формальной системы. Язык формальной теории. Синтаксис формального языка, отношение между формулой и подформулой, сложные и атомарные формулы iconОтношение семантического включения в свете аналитических тенденций л. В. Воронина Белгородский гу, Белгород, Россия
Все три подхода нашли отражение в исследованиях по лингвистике, однако чаще ученые обращаются к данной проблеме при исследовании...
Разместите кнопку на своём сайте:
ru.convdocs.org


База данных защищена авторским правом ©ru.convdocs.org 2016
обратиться к администрации
ru.convdocs.org