Главная | Обратная связь | Поможем написать вашу работу!
МегаЛекции

Построение замкнутых семантических таблиц в логике предикатов




Построение начинается с того, что замкнутая помеченная формула ts или fs помещается в корень таблицы. Далее выполняется индуктивная процедура.

Шаг n. Пусть уже построена таблица Tn-1. Особые вершины этой таблицы, которым соответствуют подформулы, не являющиеся атомами, продолжаются атомарными таблицами, соответствующими последней, выполняемой в каждой из таких ветвей, логической связкой. Результатом построения становится новая таблица Tn.

Шаг n+1. Пусть Х – особая вершина[2], которая еще не была раскрыта. Если такой вершины не существует, то семантическая таблица является замкнутой. Если такая вершина есть, строим таблицу Tn+1, продолжая каждую непротиворечивую ветвь, проходящую через вершину Х, присоединением атомарной таблицы, соответствующей находящейся в этой вершине подформуле.

Содержательно, в случаях t("x j(x)) и f($x j(x)) мы хотим избавиться от повторений, и объявляем j(с) истинной (ложной) последовательно для всех новых констант, выбирая их из списка констант, что может продолжаться бесконечно, как показано на рис. 9.

 

Вершина 1   Вершина 2   Вершина 3   Вершина 4     Из вершины 2 для всех с.
t["xA(x,x)&$y(ØA(y,y))ÚB(y,y))]

|

t["xA(x,x)]

|

t[$y(ØA(y,y)ÚB(y,y)]

Для новой с0         из вершины 2 для всех с
|

    t[ØA(c0,c0)] | f[A(c0,c0)] | t[A(c,c)] | Ä
t[ØA(c0,c0)ÚB(c0,c0)]

 
 

 

 


В этом примере левая ветвь противоречива, тогда как правая ветвь продолжается бесконечно.

Замкнутая семантическая таблица в логике предикатов есть объединение всех таблиц Tn из предыдущего построения, т.е. Она может иметь бесконечное число вершин, тогда как семантические таблицы для логики высказываний всегда конечны.

Основные определения:

1. Замкнутая семантическая таблица называется противоречивой, если все ее ветви противоречивы.

2. Предложение s выводимо по Бету (опровержимо по Бету), если существует противоречивая замкнутая семантическая таблица с корнем fs (ts). Тот факт, что предложение s выводимо по Бету обозначается ├В s.

3. Предложение s выводимо по Бету из множества S предложений логики предикатов, если существует противоречивая замкнутая семантическая таблица с корнем fs. и следующей вершиной t P, где Р – конъюнкция предложений множества S. Этот факт обозначается S ├В s.

Поделиться:





Читайте также:





Воспользуйтесь поиском по сайту:



©2015 - 2024 megalektsii.ru Все авторские права принадлежат авторам лекционных материалов. Обратная связь с нами...