Въпрос 18

Термове и формули на предикатното смятане от първи ред. Хорнови клаузи. Унификация. Mетод на резолюцията в предикатното смятане от първи ред.

Table of Contents

Анотация

Дефинират се синтактичните понятия терм и формула от даден език на предикатното смятане. Дава се семантика на термовете и формулите в дадена структура за езика. Доказва се, че множество от затворени универсални формули има модел точно тогава, когато множеството от частните му случаи е булево изпълнимо. Дефинира се понятието съждителен резолютивен извод и се доказва теоремата за коректност и пълнота на резолютивната изводимост. Описва се метода на резолюцията. Дефинира се понятието хорнов дизюнкт и се доказва, че изпълнимите множества от хорнови дизюнкти имат най-малък модел.

Примерни типове задачи, свързани с въпроса:

  1. Практически задачи – за дефиниране на предикат с помощта на Пролог; за проследяване на изпълнението на програма на Пролог.
  2. Теоретични задачи – за определимост и неопределимост на свойства в дадена структура; показване на изпълнимост на множество от предикатни формули чрез посочване на структура; доказване на неизпълнимост на множество от предикатни формули с помощта на метода на резолюцията.

Литература: [11], [12], [18], [26].

Unless otherwise stated, the content of this page is licensed under Creative Commons Attribution-NonCommercial-ShareAlike 3.0 License