Самостоятельная работа По предмету: искусственный интеллект

Аксиомы теорий первого порядка разбиваются на логические и собственные. Логические аксиомы (аксиомы исчисления предикатов) - это бесконечное множество формул, построенных с помощью следующих пяти схем аксиом:

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