Логическое программирование на языке Visual Prolog. Солдатова О.П - 6 стр.

UptoLike

ВУЗ: 

СГАУ | Самара

Составители: 

Рубрика: 

6
первого порядка в качестве основы для описания предметной области и
осуществления резолюционного логического вывода.
Аксиоматической системой называется способ задания множества
путем указания исходных элементов (аксиом исчисления) и правил вывода,
каждое из которых описывает, как строить новые элементы из исходных
элементов.
Любая аксиоматическая система должна удовлетворять следующим
требованиям:
1. Непротиворечивость
: невозможность вывода отрицания уже
доказанного выражения (которое считается общезначимым);
2. Независимость (минимальность): система не должна содержать
бесполезных аксиом и правил вывода. Некоторое выражение
независимо от аксиоматической системы, если его нельзя вывести с
помощью этой системы. В минимальной системе каждая аксиома
независима от остальной системы, то есть, не выводима из других
аксиом.
3. Полнота (взаимность адекватности): любая тавтология выводима из
системы аксиом. В адекватной системе аксиом любая выводимая
формула есть тавтология, то есть верно, что
⎥
-- P
→
⎥
= P.
Соответственно в полной системе верно:
⎥
= P
→
⎥
--P.
Исчислениями называют наиболее важные из аксиоматических
логических систем – исчисление высказываний и исчисление предикатов.
Исчисление высказываний и исчисление предикатов первого порядка
являются полными аксиоматическими системами.
Под аксиоматическим методом [1] понимают способ построения
научной теории, при котором за ее основу берется ряд основополагающих, не
требующих доказательств положений этой теории, называемыми аксиомами
или
постулатами.
Аксиоматический метод зародился в работах древнегреческих
геометров. Вплоть до начала XIX века единственным образцом применения
этого метода была геометрия Евклида.
В начале XIX века Н.И.Лобачевский и Я.Больяй, независимо друг от
друга, открыли новую неевклидову геометрию, заменив пятый постулат о
параллельных прямых на его отрицание. Их открытие стало отправной
точкой
для развития аксиоматического метода, который лег в основу теории
формальных систем.
Формальная теория строится как четко определенный класс
выражений, формул, в котором некоторым точным способом выделяется
подкласс теорем данной формальной системы. При этом формулы
формальной системы непосредственно не несут в себе никакого
содержательного смысла, они строятся из произвольных знаков или
символов, исходя лишь из соображений удобства.
Формальная теория (система), задаётся четверкой вида M = <T, S, A,
B>. Множество T есть множество базовых элементов, например слов из

Страницы