Гибридная логика

Оглавление:

Гибридная логика
Гибридная логика

Видео: Гибридная логика

Видео: Гибридная логика
Видео: Железная логика 1 мая 2020. Мишустина не уберегли, православный социализм и гибридная Третья мировая 2024, Март
Anonim

Входная навигация

  • Содержание входа
  • Библиография
  • Академические инструменты
  • Friends PDF Preview
  • Информация об авторе и цитировании
  • Вернуться к началу

Гибридная логика

Впервые опубликовано вт 13 июня 2006 г.; существенная редакция пт мар 24, 2017

Гибридная логика - это логика, которая получается путем добавления дополнительной выразительной силы к обычной модальной логике. Самая базовая гибридная логика получается путем добавления так называемых номиналов, которые являются пропозициональными символами нового рода, каждый из которых является истинным только в одном возможном мире. История гибридной логики восходит к работе Артура Н. Приора в 1960-х годах.

  • 1. Мотивации для гибридной логики
  • 2. Формальная семантика
  • 3. Переводы
  • 4. Артур Н. Приор и гибридная логика
  • 5. Развитие гибридной логики со времен Приора
  • 6. Аксиомы для гибридной логики
  • 7. Аналитические методы доказательства для гибридной логики
  • Библиография
  • Академические инструменты
  • Другие интернет-ресурсы
  • Связанные Записи

1. Мотивации для гибридной логики

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

идет дождь

который явно имеет разные истинностные значения в разное время. Теперь некоторые утверждения на естественном языке верны ровно в одно время, в возможном мире или что-то еще. Примером является утверждение

пять часов 15 марта 2006 г.

что верно в то время в пять часов 15 марта 2006 года, но ложно во всех других случаях. Первый тип операторов естественного языка может быть формализован в обычной модальной логике, но второй тип не может.

Основной мотивацией для гибридной логики является добавление дополнительной выразительной силы к обычной модальной логике с целью возможности формализовать утверждения второго типа. Это достигается добавлением к обычной модальной логике второго вида пропозициональных символов, называемых номиналами, так что в семантике Крипке каждый номинал истинен относительно ровно одной точки. Оператор естественного языка второго типа (например, пример примера со временем пять часов 15 марта 2006 г.) затем формализуется с использованием номинального, а не обычного пропозиционального символа (который будет использоваться для формализации примера выражения с дождливой погодой), Тот факт, что номинал является истинным относительно ровно одной точки, подразумевает, что номинал можно считать термином, относящимся к точке, например, если (mathtt {a}) является номиналом, который означает «это пять «Часы 15 марта 2006 года»,тогда этот номинал можно считать термином, относящимся ко времени пять часов 15 марта 2006 года. Таким образом, в гибридной логике термин является особым видом пропозиционального символа, тогда как в логике первого порядка он является аргументом предиката.

Большинство гибридных логик требуют дополнительных дополнительных механизмов, чем номинальные. Существует несколько вариантов добавления дополнительной техники; здесь мы рассмотрим так называемые операторы удовлетворения. Мотивация для добавления операторов удовлетворения заключается в том, чтобы иметь возможность формализовать утверждение, являющееся истинным в конкретное время, возможный мир или что-то еще. Например, мы хотим иметь возможность формализовать, что утверждение «идет дождь» верно в то время, когда пять часов 15 марта 2006 года, то есть

в пять часов 15 марта 2006 года идет дождь.

Это формализуется формулой (mathtt {@_ a p}), где номинал (mathtt {a}) означает «это пять часов 15 марта 2006 года», как указано выше, и где (mathtt {p}) - это обычный пропозициональный символ, который означает «идет дождь». Это часть (mathtt {@_ a}) формулы (mathtt {@_ a p}), которая называется оператором удовлетворения. В общем, если (mathtt {a}) является номинальным, а (mathtt { phi}) - произвольной формулой, то новая формула (mathtt {@_ a / phi}) называется a Заявление об удовлетворении может быть построено. Утверждение об удовлетворении (mathtt {@_ a / phi}) выражает, что формула (mathtt { phi}) верна относительно одной конкретной точки, а именно той точки, в которой номинальное число (mathtt {a }) относится.

Подводя итог, мы теперь добавили дополнительную выразительную силу к обычной модальной логике в форме номиналов и операторов удовлетворения. Неформально, номинал (mathtt {a}) имеет условие истинности

(mathtt {a}) истинно относительно точки (w)

тогда и только тогда, когда ссылка на (mathtt {a}) идентична (w)

и утверждение удовлетворенности (mathtt {@_ a / phi}) имеет условие истинности

(mathtt {@_ a / phi}) истинно относительно точки (w)

тогда и только тогда, когда

(mathtt { phi}) истинно относительно ссылки (mathtt {a })

Обратите внимание, что на самом деле точка (w) не имеет значения в условии истинности для (mathtt {@_ a / phi}), поскольку оператор удовлетворения (mathtt {@_ a}) перемещает точку оценки на ссылку (mathtt {a}) независимо от тождества (w).

Примечательно, что номиналы вместе с операторами удовлетворенности позволяют нам выразить, что две точки идентичны: если номиналы (mathtt {a}) и (mathtt {b}) относятся к точкам (w) и (v), то формула (mathtt {@_ a b}) выражает, что (w) и (v) идентичны. Следующая строка рассуждений показывает почему.

(mathtt {@_ a b}) истинно относительно точки (w)

тогда и только тогда, когда

(mathtt {b}) истинно относительно ссылки (mathtt {a})

тогда и только тогда, когда

(mathtt {b}) истинно относительно (w)

тогда и только тогда, когда ссылка на (mathtt {b}) идентична (w)

тогда и только тогда если

(v) совпадает с (w)

Тождественное отношение на множестве обладает общеизвестными свойствами рефлексивности, симметрии и транзитивности, что отражается в том, что формулы

(begin {align *} & / mathtt {@_ a a} & / mathtt {@_ a b / rightarrow @_b a} & (mathtt {@_ a b / amp @_b c) rightarrow @ _a c} end {align *})

действительны формулы гибридной логики. Также формула

[(mathtt {@_ ab / amp @_a / phi) rightarrow @_b / phi})

действует. Это правило замены.

Помимо номиналов и операторов удовлетворения, в дальнейшем мы рассмотрим так называемые связующие (mathtt { forall}) и (mathtt { downarrow}), позволяющие строить формулы (mathtt { forall a / phi}) и (mathtt {{ downarrow} a / phi}). Связыватели связывают номиналы с точками двумя различными способами: Связыватель (mathtt { forall}) количественно определяет точки, аналогичные стандартному универсальному квантификатору первого порядка, то есть (mathtt { forall a / phi}) истинно относительно (w) тогда и только тогда, когда на любую точку, на которую ссылается номинал (mathtt {a}), это тот случай, когда (mathtt { phi}) истинно относительно (ш). Связыватель (mathtt { downarrow}) связывает номинал с точкой оценки, то есть (mathtt {{ downarrow} a / phi}) является истинным относительно (w), если и только если (mathtt { phi}) истинно относительно (w), когда (mathtt {a}) ссылается на (w). Оказывается, связыватель (mathtt { downarrow}) определим в терминах (mathtt { forall}) (как показано ниже).

2. Формальная семантика

Язык, который мы рассматриваем, является языком обычной модальной логики, построенным на обычных пропозициональных символах (mathtt {p}, / mathtt {q}, / mathtt {r},…), а также на номиналах (mathtt {a}, / mathtt {b}, / mathtt {c},…) и расширены с операторами удовлетворения и связывателями. Мы считаем пропозициональные связки (mathtt { wedge}) и (mathtt { neg}) примитивными; другие пропозициональные связки определяются как обычно. Аналогично, мы принимаем модальный оператор (mathtt { Box}) примитивным и определяем модальный оператор (mathtt { Diamond}) как (mathtt { neg / Box / neg}), Как следует из названия, связующие связывают номиналы, а понятия свободного и связанного вхождений номиналов определяются аналогично логике первого порядка. Операторы удовлетворенности не связывают номиналы, то естьсвободные номинальные вхождения в формуле (mathtt {@_ a / phi}) - это свободные номинальные вхождения в (mathtt { phi}) вместе с вхождением (mathtt {a}). Пусть (mathtt { phi [c / a]}) - формула (mathtt { phi}), где номинал (mathtt {c}) заменен на все свободные вхождения номинальный (mathtt {a}). Если номинал (mathtt {a}) встречается свободно в (mathtt { phi}) в рамках (mathtt { forall c}) или (mathtt {{ downarrow} c}), тогда связанный номинал (mathtt {c}) в (mathtt { phi}) будет соответствующим образом переименован. Если номинал (mathtt {a}) встречается свободно в (mathtt { phi}) в рамках (mathtt { forall c}) или (mathtt {{ downarrow} c}), тогда связанный номинал (mathtt {c}) в (mathtt { phi}) будет соответствующим образом переименован. Если номинал (mathtt {a}) встречается свободно в (mathtt { phi}) в рамках (mathtt { forall c}) или (mathtt {{ downarrow} c}), тогда связанный номинал (mathtt {c}) в (mathtt { phi}) будет соответствующим образом переименован.

Теперь мы определим модели и рамки. Модель для гибридной логики - это тройка ((W, R, V)), где (W) - непустое множество, (R) - бинарное отношение на (W), и (V) - это функция, которой каждой паре, состоящей из элемента (W) и обычного пропозиционального символа, присваивается элемент множества ({0,1 }). Пара ((W, R)) называется фреймом. Таким образом, модели и кадры такие же, как в обычной модальной логике. Элементы (W) называются мирами, а отношение (R) называется отношением доступности. Говорят, что модель ((W, R, V)) основана на системе координат ((W, R)).

Присвоение модели (M = (W, R, V)) - это функция (g), которой каждому именному присваивается элемент из (W). Присвоение (g ') является (mathtt {a}) -вариантом (g), если (g') совпадает с (g) по всем номиналам, кроме, возможно, (mathtt {а}). Отношение (M, g, w / vDash / phi) определяется по индукции, где (g) является присваиванием, (w) является элементом (W) и (mathtt { phi}) это формула.

(M, g, w / vDash / mathtt {p}), если (V (w, / mathtt {p}) = 1)

(M, g, w / vDash / mathtt {a}), если (w = g (mathtt {a}))

(M, g, w / vDash / mathtt { phi / wedge / psi}) iff (M, g, w / vDash / mathtt { phi }) и (M, g, w / vDash / mathtt { psi})

(M, g, w / vDash / mathtt { neg / phi}), если не (M, g, w / vDash / mathtt { phi})

(M, g, w / vDash / mathtt { Box} phi), если для любого элемента (v) из (W) такого, что (wRv), это тот случай, когда (M, g, v / vDash / mathtt { phi})

(M, g, w / vDash / mathtt {@_ a / phi}) iff (M, g, g (mathtt {a}) vDash / mathtt { phi})

(M, g, w / vDash / mathtt { forall a / phi}), если для любого (mathtt {a}) - вариант (g ') из (g), это тот случай, когда (M, g', w / vDash / mathtt { phi})

(M, g, w / vDash / mathtt {{ downarrow} a / phi}) iff (M, g ', w / vDash / mathtt { phi}) где (g') - это (mathtt {a}) - вариант (g) такой, что (g '(mathtt {a}) = w).

Формула (mathtt { phi}) называется истинной в (w), если (M, g, w / vDash / mathtt { phi}); в противном случае он называется ложным в (w). По соглашению (M, g / vDash / mathtt { phi}) означает (M, g, w / vDash / mathtt { phi}) для каждого элемента (w) из (W) и (M / vDash / mathtt { phi}) означает (M, g / vDash / mathtt { phi}) для каждого назначения (g). Формула (mathtt { phi}) действительна в кадре тогда и только тогда, когда (M / vDash / mathtt { phi}) для любой модели (M), основанной на рассматриваемом кадре, Формула (mathtt { phi}) действительна в классе фреймов (F) тогда и только тогда, когда (mathtt { phi}) действительна в любом фрейме (F). Формула (mathtt { phi}) действительна тогда и только тогда, когда (mathtt { phi}) действительна в классе всех фреймов. Определение выполнимости оставлено читателю.

Обратите внимание, что связующее (mathtt { downarrow}) определяется в терминах (mathtt { forall}) как формула (mathtt {{ downarrow} a / phi / leftrightarrow / forall a (rightarrow / phi)}) действует в любом кадре.

Тот факт, что гибридная обычная модальная логика действительно дает больше выразительной силы, можно, например, увидеть, рассмотрев формулу (mathtt {{ downarrow} c / Box / neg c}). Нетрудно проверить, что эта формула действительна в кадре тогда и только тогда, когда она нерефлексивна. Таким образом, нерефлексивность может быть выражена гибридно-логической формулой, но хорошо известно, что она не может быть выражена какой-либо формулой обычной модальной логики. На самом деле нерефлексивность можно выразить, просто добавив номиналы в обычную модальную логику, а именно по формуле (mathtt {c / rightarrow / Box / neg c}). Другими примерами свойств, выражаемых в гибридной логике, но не в обычной модальной логике, являются асимметрия (выражаемая (mathtt {c / rightarrow / Box / neg / Diamond c})), антисимметрия (выражаемая (mathtt { c / rightarrow / Box (Diamond c / rightarrow c)})),и универсальность (выражаемая (mathtt { Diamond c})).

См. Главу справочника Areces and ten Cate (2006) для подробного описания синтаксиса и семантики гибридной логики, а также многих других основных определений. Приведенный выше синтаксис и семантика могут быть расширены несколькими способами, в частности, может быть добавлен механизм первого порядка (конечно, эквивалентный способ получения гибридной логики первого порядка заключается в добавлении гибридно-логического механизма к модальному порядку первого порядка). логика). См. Braüner (2014) для обзора гибридной логики первого порядка, см. Главу 6 Braüner (2011a) для более подробного описания и см. Главу 7 Braüner (2011a) для описания интенсиональной гибридной логики первого порядка.

3. Переводы

Гибридная логика может быть преобразована в логику первого порядка с равенством, и (фрагмент) логики первого порядка с равенством может быть переведена обратно в (фрагмент) гибридной логики. Рассматриваемый язык первого порядка имеет 1-местный символ предиката (mathtt {p ^ *}), соответствующий каждому обычному пропозициональному символу (mathtt {p}) модальной логики, 2-местный символ предиката (mathtt {R}) и двухзначный предикатный символ (mathtt {=}). Конечно, символ предиката (mathtt {p ^ *}) будет интерпретироваться таким образом, чтобы он относил интерпретацию соответствующего модального пропозиционального символа (mathtt {p}) к мирам, символу предиката (mathtt {R}) будет интерпретироваться с использованием отношения доступности, а предикатный символ (mathtt {=}) будет интерпретироваться с использованием отношения идентичности в мирах. Мы позволяем (mathtt {a}, / mathtt {b},\ mathtt {c}, / ldots) располагаются над переменными первого порядка. Язык не имеет постоянных или функциональных символов. Мы будем отождествлять переменные первого порядка с номиналами гибридной логики.

Сначала мы переводим гибридную логику в логику первого порядка с равенством. Учитывая две новые переменные первого порядка (mathtt {a}) и (mathtt {b}), переводы (mathrm {ST} _ / mathtt {a}) и (mathrm { ST} _ / mathtt {b}) определяются взаимной рекурсией. Мы просто даем перевод (mathrm {ST} _ / mathtt {a}).

(begin {align *} mathrm {ST} _ / mathtt {a} (mathtt {p}) & = / mathtt {p ^ * (a)} / \ mathrm {ST} _ / mathtt {a } (mathtt {c}) & = / mathtt {a = c} / \ mathrm {ST} _ / mathtt {a} (mathtt { phi / wedge / psi}) & = / mathrm {ST} _ / mathtt {a} (mathtt { phi}) mathtt { wedge} mathrm {ST} _ / mathtt {a} (mathtt { psi}) / \ mathrm {ST} _ / mathtt {a } (mathtt { neg / phi}) & = / mathtt { neg} mathrm {ST} _a (phi) / \ mathrm {ST} _ / mathtt {a} (mathtt { Box / phi }) & = / mathtt { forall b (R (a, b) rightarrow} mathrm {ST} _ / mathtt {b} (mathtt { phi}) mathtt {)} / \ mathrm {ST } _ / mathtt {a} (mathtt {@_ c / phi}) & = / mathrm {ST} _ / mathtt {a} (mathtt { phi}) (mathtt {c} / / mathtt {a}] / \ mathrm {ST} _ / mathtt {a} (mathtt {{ downarrow} c / phi}) & = / mathrm {ST} _ / mathtt {a} (mathtt { phi}) (mathtt {a} / / mathtt {c}] / \ mathrm {ST} _ / mathtt {a} (mathtt { forall c / phi}) &= / mathtt { forall c} mathrm {ST} _ / mathtt {a} (mathtt { phi}) end {align *})

Определение (mathrm {ST} _ / mathtt {b}) получается путем обмена (mathtt {a}) и (mathtt {b}). Перевод является расширением известного стандартного перевода модальной логики в логику первого порядка. В качестве примера мы покажем шаг за шагом, как гибридно-логическая формула (mathtt {{ downarrow} c / Box / neg c}) переводится в формулу первого порядка:

(begin {align *} mathrm {ST} _ / mathtt {a} (mathtt {{ downarrow} c / Box / neg c}) & = / mathrm {ST} _ / mathtt {a} (mathtt { Box / neg c}) (mathtt {a} / / mathtt {c}] & = / mathtt { forall b (R (a, b) rightarrow} mathrm {ST} _ / mathtt {b} (mathtt { neg c}) mathtt {)} (mathtt {a} / / mathtt {c}] & = / mathtt { forall b (R (a, b) rightarrow / neg} mathrm {ST} _ / mathtt {b} (mathtt {c}) mathtt {)} (mathtt {a} / / mathtt {c}] & = / mathtt { forall b (R) (a, b) rightarrow / neg b = c)} (mathtt {a} / / mathtt {c}] & = / mathtt { forall b (R (a, b) rightarrow / neg b = а)}. / Конец {выравнивание *})

Полученная формула первого порядка эквивалентна (mathtt { neg R (a, a)}), которая показывает, что (mathtt {{ downarrow} c / Box / neg c}) действительно соответствует отношение доступности является нерефлексивным, ср. выше.

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

(begin {align *} mathrm {HT} (mathtt {p ^ * (a)}) & = / mathtt {@_ a p} / \ mathrm {HT} (mathtt {R (a, c)}) & = / mathtt {@_ a / Diamond c} / \ mathrm {HT} (mathtt {a = c}) & = / mathtt {@_ a c} / \ mathrm {HT} (mathtt { phi / wedge / psi}) & = / mathrm {HT} (mathtt { phi}) mathtt { wedge} mathrm {HT} (mathtt { psi}) / \ mathrm {HT} (mathtt { neg / phi}) & = / mathtt { neg} mathrm {HT} (mathtt { phi}) / \ mathrm {HT} (mathtt { forall a / phi})) & = / mathtt { forall a} mathrm {HT} (mathtt { phi}) end {align *})

Обратите внимание, что гибридно-логическое связующее (mathtt { forall}) необходимо. История вышеупомянутых наблюдений восходит к работе Артура Н. Приора, мы вернемся к этому позже.

Точно так же то, что называется ограниченным фрагментом логики первого порядка, может быть переведено в гибридную логику, но здесь необходим только связующий элемент (mathtt { downarrow}), как указано в статье Ареса, Блэкберна и Маркса. (2001). Ограниченный фрагмент - это фрагмент логики первого порядка, свойство квантификаторов которого встречается только в формуле (mathtt { forall c (R (a, c) rightarrow / phi)}), где это требуется что переменные (mathtt {a}) и (mathtt {c}) разные. Перевод из ограниченного фрагмента в гибридную логику без связывателя (mathtt { forall}) можно получить, заменив последнее предложение в переводе HT выше на

(mathrm {HT} (mathtt { forall c (R (a, c) rightarrow / phi)}) = / mathtt {@_ a / Box { downarrow} c} mathrm {HT} (mathtt { Phi}).)

В Areces, Blackburn, и Marx (2001) приведен ряд независимых семантических характеристик ограниченного фрагмента.

Приведенные выше переводы сохраняют правду. Чтобы сформулировать это формально, мы используем хорошо известное наблюдение, что модели и назначения для гибридной логики могут рассматриваться как модели и назначения для логики первого порядка и наоборот. Эти результаты по сохранению правды просты для формулировки, и мы оставляем детали читателю. Таким образом, гибридная логика со связующим (mathtt { forall}) обладает той же выразительной силой, что и логика первого порядка с равенством, а гибридная логика без связующего (mathtt { forall}) (но с переплетчик (mathtt { downarrow})) обладает той же выразительной силой, что и ограниченный фрагмент логики первого порядка (обратите внимание, что перевод (mathrm {ST} _ / mathtt {a} (mathtt {) phi})) любой формулы (mathtt { phi}) без связующего (mathtt { forall}) находится в ограниченном фрагменте).

Приведенные выше переводы могут быть расширены на гибридную логику первого порядка, и в этом случае релевантной целевой логикой является логика первого порядка с равенством, один вид для миров и один для индивидуумов, см. Главу 6 Braüner (2011a). В случае интенсиональной гибридной логики первого порядка используются три вида, третий тип предназначен для интенций, см. Главу 7 Braüner (2011a).

4. Артур Н. Приор и гибридная логика

История гибридной логики восходит к гибридной временной логике Артура Н. Приора, которая представляет собой гибридную версию обычной временной логики. С целью дальнейшего изучения этого вопроса мы дадим формальное определение гибридной временной логики: язык гибридной временной логики - это просто язык гибридной логики, определенный выше, за исключением того, что есть два модальных оператора, а именно (mathtt {G}) и (mathtt {H}) вместо одного модального оператора (mathtt { Box}). Два новых модальных оператора называются напряженными операторами. Семантика гибридной временной логики - это семантика гибридной логики, ср. ранее, с предложением (mathtt { Box}), замененным предложениями для операторов времени (mathtt {G}) и (mathtt {H}).

(M, g, w / vDash / mathtt {G / phi}), если для любого элемента (v) из (W) такого, что (wRv), случай (M, g, v / vDash / mathtt { phi})

(M, g, w / vDash / mathtt {H / phi}), если для любого элемента (v) из (W) такого, что (vRw), это тот случай, когда (M, g, v / vDash / mathtt { phi})

Таким образом, теперь есть два модальных оператора, а именно, один «смотрит вперед» по отношению доступности, а другой «смотрит назад». В напряженной логике элементы множества (W) называются моментами или моментами, а отношение (R) называется отношением ранее-позже.

Конечно, легко изменить приведенные выше переводы (mathrm {ST} _a) и (mathrm {HT}) так, чтобы получались переводы между гибридной временной логикой (включая (mathtt { forall) }) связующее) и логика первого порядка с равенством. Рассматриваемая логика первого порядка - это то, что Приор назвал логикой первого порядка раньше-позже. Учитывая переводы, отсюда следует, что логика первого порядка Приора более раннего и более позднего обладает той же выразительной силой, что и логика гибридного времени.

Теперь Приор ввел гибридную напряженную логику в связи с тем, что он назвал четырьмя ступенями напряженно-логической вовлеченности. Мотивация его четырех ступеней напряженно-логического участия была философской. Четыре класса были представлены в книге «Приор» (1968), глава XI (также глава XI в новом издании «Приор» (2003)). Более того, см. Prior (1967), главу V.6 и приложение B.3-4. Для более общего обсуждения см. Посмертно изданную книгу Prior and Fine (1977). Этапы переходят от того, что можно рассматривать как чистую логику первого порядка раньше-позже, к тому, что можно рассматривать как чистую напряженную логику; цель состоит в том, чтобы иметь возможность рассматривать напряженную логику четвертой стадии как охватывающую логику первой и более поздней стадии. Другими словами, цель состояла в том, чтобы иметь возможность перевести логику первого порядка отношения «раннее-позднее» в напряженную логику. Именно с этой целью Приор представил так называемые мгновенные предложения:

То, что я назову третьим классом напряженно-логического вовлечения, состоит в том, чтобы рассматривать мгновенные переменные (a, b, c) и т. Д. Как представляющие предложения. (До 2003 г., стр. 124)

В контексте модальной логики Приор назвал такие предложения возможными мировыми предложениями. Конечно, это то, что мы здесь называем номиналами. Приор также ввел связующее (mathtt { forall}) и то, что мы здесь называем операторами удовлетворения (он использовал обозначение (mathtt {T (a, / phi)}) вместо (mathtt {@ _a / phi}) для операторов удовлетворенности). Фактически, логика времени третьего класса Приора идентична гибридной логике времени, определенной выше. Связыватель (mathtt { downarrow}) был введен намного позже. Таким образом, Приор получил выразительную силу своей логики раннего-первого порядка первого порядка, добавив к обычной напряженной логике дополнительную выразительную силу в форме номиналов, операторов удовлетворения и связующего (mathtt { forall}). Так что с технической точки зрения он явно достиг своей цели.

Однако с философской точки зрения обсуждается вопрос о том, является ли онтологический смысл его временной логики третьего класса таким же, как онтологический смысл логики первого порядка более раннего или более позднего. Например, связыватель (mathtt { forall}) некоторыми авторами рассматривается как прямая аналогия с квантификатором первого порядка (mathtt { forall}) и поэтому подозрительный; см., например, статью Sylvan (1996) в коллекции Copeland (1996). Также ряд других работ в этом сборнике актуальны. См. Браунер (2002) для обсуждения напряженной логики Приора в четвертом классе. См. Также Øhrstrøm and Hasle (1993), Øhrstrøm and Hasle (2006), Müller (2007) и Blackburn (2007). Наконец, см. Обсуждение четырех классов Приора в главе 1 Браунера (2011a).

Вышеупомянутая работа Øhrstrøm and Hasle (2006) дает подробный отчет о логической работе Приора. Полное описание жизни и работы Приор см. В книге «Øhrstrøm and Hasle» (1995). В статье Hasle and Øhrstrøm (2016) описывается методологический подход Приора, в частности, его взгляд на формализацию и роль символической логики в концептуальных исследованиях.

5. Развитие гибридной логики со времен Приора

Первое полностью строгое определение гибридной логики было дано в Bull (1970), которое появилось в специальном выпуске журнала Theoria в память о Приоре. Булл вводит третий тип пропозициональных символов, где предполагается, что пропозициональный символ является истинным точно в одной ветви («ходе событий») в модели времени ветвления. Эта идея сортировки пропозициональных символов в соответствии с ограничениями их интерпретаций позже получила дальнейшее развитие у ряда авторов, для обсуждения см. Раздел 5 статьи «Блэкберн и Цакова» (1999).

Гибридный логический механизм, первоначально изобретенный Приором в конце 1960-х годов, был заново изобретен в 1980-х годах Соломоном Пасси и Тинко Тинчевым из Болгарии, см. Пасси и Тинчев (1985), а также Пасси и Тинчев (1991). В отличие от обычной модальной логики, эта работа проводилась в связи с гораздо более выразительной пропозициональной динамической логикой.

Основным вкладом в 90-е годы стало введение связующего (mathtt { downarrow}). Ранняя версия связующего вещества вниз была представлена Валентином Горанко в работах Горанко (1994) и Горанко (1996). Версия настоящего документа была представлена в Blackburn and Seligman (1995). С тех пор гибридная логика со связующим (mathtt { downarrow}) широко изучалась, см., Например, статью Ареса, Блэкберна и Маркса (2001) о теоретико-модельных аспектах этой логики. Комплексное исследование модели теории гибридной логики является докторская диссертация Тен Кейт (2004).

Также более слабая гибридная логика, полученная путем исключения обоих связующих (mathtt { downarrow}) и (mathtt { forall}), была предметом обширного исследования. Оказывается, что эта логика без связующего и ряд ее вариантов разрешимы. В работе Areces, Blackburn и Marx (1999) приведен ряд результатов сложности для гибридных модальных и временных логик в различных классах фреймов, например, произвольных, транзитивных, линейных и ветвящихся. Примечательно, что проблема выполнимости гибридной логики без связующего по произвольным кадрам разрешима в PSPACE, что аналогично сложности определения выполнимости в обычной модальной логике. Таким образом, гибридизация обычной модальной логики дает больше выразительной силы, но сложность остается той же. Была проведена некоторая работа по моделированию номиналов внутри модальной логики,см. Kracht and Wolter (1997).

Любая обычная модальная формула выражает монадическое свойство второго порядка на фреймах, и хорошо известно, что для некоторых модальных формул, включая так называемые формулы Сальквиста, свойство второго порядка эквивалентно свойству первого порядка. В работе Goranko and Vakarelov (2006) показано, что это справедливо и для класса гибридно-логических формул, включая номиналы. Существует несколько алгоритмов для вычисления эквивалентов первого порядка обычной модальной формулы. Один из таких алгоритмов, SQEMA, содержится в работе Conradie, Goranko и Vakarelov (2006), расширенной для охвата гибридно-логических формул, рассмотренных в Goranko и Vakarelov (2006).

Примечательно, что гибридная логика первого порядка предлагает именно те функции, которые необходимы для доказательства теорем интерполяции: хотя интерполяция не выполняется в ряде известных модальных логик первого порядка, их гибридные аналоги обладают этим свойством, см. Areces, Blackburn и Marx (2003), а также Блэкберн и Маркс (2003). Первая статья дает теоретико-модельное доказательство интерполяции, тогда как вторая статья дает алгоритм вычисления интерполантов на основе системы таблиц.

Следует также упомянуть, что логики, подобные гибридным логикам, играют центральную роль в области логики описания, которая является семейством логик, используемых для представления знаний в искусственном интеллекте, см. Статью Blackburn and Tzakova (1998) и докторскую диссертацию Карлоса Ареса. Диссертация (2000).

Как описано в предыдущем разделе, Приор ввел гибридную временную логику для решения конкретной проблемы в философии времени, но в Приоре (1968), главе XIV (также в главе XIV в новом издании Приора (2003)), он также показал эта гибридная временная логика может заменить двумерную временную логику, введенную Гансом Кампом в Kamp (1971). Измерение - это просто число моментов, относительно которых вычисляется формула, поэтому добавление гибридно-логического механизма позволяет заменить два измерения одним. Эта работа недавно была продолжена в ряде работ Блэкберном и Йоргенсеном, см. Блэкберн и Йоргенсен (2016a) для обзора. Теперь мы дадим краткий набросок этого направления работы, адаптированный к терминологии настоящей статьи. Рассматриваемая версия гибридной логики имеет обозначенный номинал (mathtt {now}), и каждая модель поставляется вместе с обозначенным временем (t_0), так что i) любая автономная формула оценивается относительно (t_0) и ii) номинал (mathtt {now}) относится к (t_0). Более формально, мы принимаем соглашение, что ((M, t_0), g / vDash / mathtt { phi}) означает (M, g, t_0 / vDash / mathtt { phi}), и мы рассматриваем только назначения (g) где (g (mathtt {now}) = t_0). Обратите внимание, что номинал (mathtt {now}), рассматриваемый как автономная формула, действителен в этой семантике, но это не относится к любым другим номиналам. Это новое понятие валидности Блэкберн и Йоргенсен называют контекстуальной валидностью. В статье Blackburn and Jørgensen (2013) приведена система аксиом, которая является полной по отношению к. это понятие контекстуальной действительности. В статье Blackburn and Jørgensen (2012) дается полная система таблиц, но семантика этой статьи соответствует первоначальной двумерной семантике Кампа. Обе статьи также рассматривают другие индексы, такие как (mathtt {вчера}), (mathtt {сегодня}) и (mathtt {завтра}).

В статье Блэкберн и Йоргенсен (2016b) используется гибридная временная логика для объединения идей Приора с идеями Ханса Райхенбаха о том, как представлять времена естественного языка. Приор предпочитал известные операторы времени, описанные выше, тогда как Райхенбах предпочитал временные ссылки, то есть ссылки на конкретные времена, Райхенбах (1947). Оказывается, что эти два подхода могут быть объединены, что не было маршрутом, выбранным самим Приором, - см. Отчет, приведенный в «Блэкберн и Йоргенсен» (2016b),

6. Аксиомы для гибридной логики

Ряд работ посвящен аксиомам гибридной логики, например, Гаргов и Горанко (1993), Блэкберн (1993) и Блэкберн и Цакова (1999). В статье Гаргов и Горанко (1993) дается система аксиом для гибридной логики, и показано, что если система расширяется набором дополнительных аксиом, которые являются чистыми формулами (то есть формулами, в которых все пропозициональные символы являются номиналами), тогда расширенная система аксиом полна относительно класса фреймов, проверяющих рассматриваемые аксиомы. Чистые формулы соответствуют условиям первого порядка в отношении доступности (см. Перевод (mathrm {ST} _ / mathtt {a}) выше), поэтому системы аксиом для новых гибридных логик с условиями первого порядка относительно доступности отношение может быть получено единообразным способом, просто добавляя аксиомы в зависимости от ситуации. Так,если, например, формула (mathtt {c / rightarrow / Box / neg c}) добавлена в качестве аксиомы, то полученная система является полной относительно нерефлексивных фреймов, ср. ранее. См. Обсуждение таких правил в разделе 4 статьи «Блэкберн» (2000).

Система доказательств в Gargov and Goranko (1993) использует комплексное правило (называемое COV), где схема формулы, содержащая активную часть правила, может быть сколь угодно большой; фактически активная часть вложена в сколь угодно глубокие вложения модальных операторов. Блэкберн и Цакова (1999) показывают, что операторы удовлетворенности можно использовать для формулирования системы аксиом в более стандартном формате, используя более простое правило, называемое PASTE, так что система по-прежнему завершена при расширении чистыми аксионами.

В статье Blackburn и ten Cate (2006) исследуются ортодоксальные правила доказательства (которые являются правилами доказательства без побочных условий) в аксиомных системах, и показано, что если требуется расширенная полнота с использованием чистых формул, то неортодоксальные правила доказательства необходимы в системах аксиом для гибридной логики без связующего, но система аксиом может быть дана только с использованием ортодоксальных правил доказательства для более сильной гибридной логики, включая связующее (mathtt { downarrow}). См. Также книгу Braüner (2011a) для другой системы аксиом для гибридной логики, а также систем аксиом для интуиционистской гибридной логики и гибридизации паранепротиворечивой логики Нельсона N4 (сравните с Костой и Мартинсом (2016), где рассматривается другая параконсистентная гибридная логика). Обзор интуиционистской гибридной логики можно найти в Браунере (2011b).

В работе Areces, Blackburn, Huertas и Manzano (2014) рассматривается гибридно-логическая версия модальной логики высшего порядка (то есть модальная логика, построенная на простой теории типов Черча). Приводятся системы аксиом и полнота доказывается относительно. Семантика хенкинского типа. В статье Blackburn, Huertas, Manzano и Jørgensen (2014) эти результаты расширяются, чтобы охватить связующий элемент вниз и дает переводы в ограниченный фрагмент логики первого порядка и из него (см. Выше).

7. Аналитические методы доказательства для гибридной логики

Tableau, Gentzen и теория доказательств в стиле естественного вывода для гибридной логики работают очень хорошо по сравнению с обычной модальной логикой. Обычно, когда дается модальная таблица, система Генцена или система естественных дедукций, речь идет об одной конкретной модальной логике, и оказалось проблематичным сформулировать такие системы для модальной логики единообразным образом без использования металингвистического механизма. Это может быть исправлено путем гибридизации, то есть гибридизация модальных логик позволяет формулировать однородные таблицы, системы Генцена и естественных дедукций для широких классов логики. В статье Blackburn (2000) вводится система таблиц для гибридной логики, которая имеет такую желательную особенность: аналогично системе аксиом Блэкберна и Цакова (1999), полнота сохраняется, если система таблиц расширяется набором чистых аксиом, то есть,набор чистых формул, которые можно добавлять в таблицу во время ее построения. Система таблиц Блэкберна (2000) является основой для процедуры принятия решения для фрагмента гибридной логики без связующего вещества, приведенного в работе Боландера и Браунера (2006). Эта линия работы была продолжена в работах Bolander и Blackburn (2007) и Bolander and Blackburn (2009). В работе Cerrito and Cialdea (2010) представлена еще одна процедура принятия решений на основе таблиц для гибридной логики. Другие процедуры принятия решений для гибридной логики, которые также основаны на теории доказательств, приведены в статье Kaminski and Smolka (2009). Процедуры последней статьи основаны на формулировке гибридной логики высшего порядка, включающей простейшее лямбда-исчисление. Система таблиц Блэкберна (2000) является основой для процедуры принятия решения для фрагмента гибридной логики без связующего вещества, приведенного в работе Боландера и Браунера (2006). Эта линия работы была продолжена в работах Bolander и Blackburn (2007) и Bolander and Blackburn (2009). В работе Cerrito and Cialdea (2010) представлена еще одна процедура принятия решений на основе таблиц для гибридной логики. Другие процедуры принятия решений для гибридной логики, которые также основаны на теории доказательств, приведены в статье Kaminski and Smolka (2009). Процедуры последней статьи основаны на формулировке гибридной логики высшего порядка, включающей простейшее лямбда-исчисление. Система таблиц Блэкберна (2000) является основой для процедуры принятия решения для фрагмента гибридной логики без связующего вещества, приведенного в работе Боландера и Браунера (2006). Эта линия работы была продолжена в работах Bolander и Blackburn (2007) и Bolander and Blackburn (2009). В работе Cerrito and Cialdea (2010) представлена еще одна процедура принятия решений на основе таблиц для гибридной логики. Другие процедуры принятия решений для гибридной логики, которые также основаны на теории доказательств, приведены в статье Kaminski and Smolka (2009). Процедуры последней статьи основаны на формулировке гибридной логики высшего порядка, включающей простейшее лямбда-исчисление. Эта линия работы была продолжена в работах Bolander и Blackburn (2007) и Bolander and Blackburn (2009). В работе Cerrito and Cialdea (2010) представлена еще одна процедура принятия решений на основе таблиц для гибридной логики. Другие процедуры принятия решений для гибридной логики, которые также основаны на теории доказательств, приведены в статье Kaminski and Smolka (2009). Процедуры последней статьи основаны на формулировке гибридной логики высшего порядка, включающей простейшее лямбда-исчисление. Эта линия работы была продолжена в работах Bolander и Blackburn (2007) и Bolander and Blackburn (2009). В работе Cerrito and Cialdea (2010) представлена еще одна процедура принятия решений на основе таблиц для гибридной логики. Другие процедуры принятия решений для гибридной логики, которые также основаны на теории доказательств, приведены в статье Kaminski and Smolka (2009). Процедуры последней статьи основаны на формулировке гибридной логики высшего порядка, включающей простейшее лямбда-исчисление. Процедуры последней статьи основаны на формулировке гибридной логики высшего порядка, включающей простейшее лямбда-исчисление. Процедуры последней статьи основаны на формулировке гибридной логики высшего порядка, включающей простейшее лямбда-исчисление.

В статье Хансен, Боландер и Браунер (2017) дается основанная на таблицах процедура принятия решения для многозначной гибридной логики, то есть гибридной логики, в которой двухзначный классический логический базис был обобщен на многозначный логический базис, включающий пространство истинности, имеющее структуру конечной гейтинговой алгебры. Хансен (2010) дает основанную на таблицах процедуру принятия решения для гибридизированной версии динамической эпистемической логики, называемой логикой публичных объявлений. Это также главная проблема докторской диссертации Хансена (2011).

Теория доказательств гибридной логики в стиле естественных дедукций была исследована в книге Браунера (2011a). Эта книга также дает систему Генцена для гибридной логики. Эти естественные системы дедукции и Генцена могут быть расширены с помощью дополнительных правил доказательства, соответствующих условиям первого порядка для отношений доступности, выраженных так называемыми геометрическими теориями (это, конечно, аналогично расширению систем таблиц и аксиом с чистыми аксиомами). См. Также Браунер и де Пайва (2006), где для интуиционистской гибридной логики дана естественная система дедукции (глава 8 Браунера (2011a)).

Табличные системы для гибридной логики первого порядка можно найти в статье Blackburn and Marx (2002). Естественные дедукционные и аксиомные системы для гибридной логики первого порядка можно найти в главе 6 книги Браунер (2011a) и в главе 7 книги, посвященной естественному выводу для интенсиональной гибридной логики первого порядка. В статье Barbosa, Martins и Carreteiro (2014) дается аксиоматизация фрагмента гибридной логики первого порядка, называемой эквациональной гибридной логикой первого порядка.

Дженри Селигман (Jerry Seligman) исследовал системы Генцена и естественного вывода для логики, аналогичной гибридной логике, еще в 1990-х годах, см. Обзор в Seligman (2001). В частности, Селигман разработал системы доказательств, которые работают с произвольными формулами, а не только с заявлениями об удовлетворенности, причем последний случай применим к большинству систем доказательств для гибридной логики, где операторы удовлетворенности используются для доступа к информации, скрытой за модальностями. Система естественного удержания в этом стиле была введена в Seligman (1997), и эта система получила дальнейшее развитие в главе 4 книги Braüner (2011a). Табличные системы в стиле доказательства Селигмана были рассмотрены в Blackburn, Bolander, Braüner и Jørgensen (2017), где приводится синтаксическое доказательство полноты. Семантическое полное доказательство системы таблиц дано в Йоргенсене, Блэкберне, Боландере,Браунер (2016). Рассуждения в этих системах не зависят напрямую от глобальных кодировок, которые делают возможным операторы удовлетворения, следовательно, эти системы можно рассматривать в большей степени в соответствии с локальным характером стандартной семантики Крипке для модальной логики. Фактически, этот более локальный стиль мышления делает эти системы подходящими для формализации перспективного мышления, имеющего место в определенных задачах психологического мышления, см. Браунер (2014b), а также Браунер, Блэкберн и Полянская (2016).этот более локальный стиль мышления делает эти системы подходящими для формализации перспективного мышления, имеющего место в определенных задачах психологического мышления, см. Браунер (2014b), а также Браунер, Блэкберн и Полянская (2016).этот более локальный стиль мышления делает эти системы подходящими для формализации перспективного мышления, имеющего место в определенных задачах психологического мышления, см. Браунер (2014b), а также Браунер, Блэкберн и Полянская (2016).

Была проведена некоторая работа по исчислению разрешений и проверке моделей, см. Арес, де Рийке и де Нивель (2001), а также Арес и Горин (2011) по исчислениям разрешения и см. Франческет и де Рийке (2006), а также Lange (2009) за результаты проверки моделей.

С середины 1990-х годов работа над гибридной логикой процветала. Мы отсылаем читателя к публикациям в библиографии для дальнейших ссылок. Более того, см. Интернет-ресурсы ниже.

Библиография

  • Аресес, C., 2000. Логическая инженерия. Случай описания и гибридной логики, кандидатская диссертация, Институт логики, языка и вычислений, Университет Амстердама.
  • Аресес, С., Блэкберн, П. и Маркс, М., 1999. «Вычислительная сложность гибридной темпоральной логики», The Logic Journal of IGPL, 8: 653–679.
  • –––, 2001. «Гибридная логика: характеристика, интерполяция и сложность», Журнал символической логики, 66: 977–1010.
  • –––, 2003. «Восстановление теоремы об интерполяции в количественной модальной логике», Анналы чистой и прикладной логики, 124: 287–299.
  • Аресес С., Блэкберн П., Уэртас А. и Мансано М., 2014. «Полнота в теории гибридного типа», журнал «Философская логика», 43: 209–238.
  • Areces, C., de Rijke, M., и de Nivelle, H., 2001. «Резолюция в модальной, описательной и гибридной логике», Journal of Logic and Computation, 11: 717–736.
  • Аресес, С. и Горин, Д., 2011. «Резолюция с порядком и отбором для гибридной логики», Журнал автоматического рассуждения, 46: 1–42.
  • Areces, C. и ten Cate, B., 2006. «Гибридная логика», в Блэкберне, Ван Бентеме и Уолтере (ред.) (2006).
  • Барбоса Л. С., Мартинс М. А. и Карретейро М., 2014. «Аксиоматизация по Гильберту для эквациональной гибридной логики», журнал «Логика, язык и информация», 23: 31–52.
  • Блэкберн, П., 1993. «Номинальная напряженная логика», журнал формальной логики Нотр-Дама, 14: 56–83.
  • –––, 2000. «Интернализация помеченного удержания», журнал «Логика и вычисления», 10: 137–168.
  • –––, 2007. «Артур Приор и Гибридная логика», Synthese, 150: 329–372.
  • Блэкберн П., Боландер Т., Браунер Т. и Йоргенсен К. Ф., 2017. «Полнота и завершение для системы таблиц в стиле Селигмана», Журнал логики и вычислений, 27: 81–107.
  • Блэкберн П., Уэртас А., Мансано М. и Йоргенсен К. Ф., 2014. «Хенкин и гибридная логика», в жизни и творчестве Леона Хенкина: очерки о его вкладе (исследования по универсальной логике), стр. 279–306. Birkhäuser.
  • Блэкберн П., Йоргенсен, К. Ф., 2012. «Индексная гибридная временная логика», «Достижения в модальной логике» (том 9), с. 144–160. Публикации колледжа.
  • –––, 2013. «Контекстуальная валидность в гибридной логике», в Моделировании с использованием контекста (Конспект лекций в области компьютерных наук: Том 8177), с. 185–198. Гейдельберг: Спрингер.
  • –––, 2016a. «Артур Приор и« сейчас », Synthese, 193: 3665–3676.
  • –––, 2016b. «Райхенбах, логика априорной и гибридной времени», Synthese, 193: 3677–3689
  • Блэкберн, П. и Маркс, М., 2002. «Таблицы для количественной гибридной логики», в Автоматизированных рассуждениях с аналитическими таблицами и смежными методами, TABLEAUX (Конспект лекций по искусственному интеллекту: том 2381), стр. 38–52. Гейдельберг: Спрингер.
  • –––, 2003. «Конструктивная интерполяция в гибридной логике», Журнал символической логики, 68: 463–480.
  • Блэкберн, П. и Селигман, J., 1995. «Гибридные языки», журнал «Логика, язык и информация», 4: 251–271.
  • Блэкберн, П. и Тен Кейт, Б., 2006. «Чистые расширения, правила доказательства и гибридная аксиоматика», Studia Logica, 84: 277–322.
  • Блэкберн П., Цакова М., 1998. «Гибридизация концептуальных языков», Анналы математики и искусственного интеллекта, 24: 23–49.
  • –––, 1999. «Гибридные языки и временная логика», Logic Journal of IGPL, 7: 27–54.
  • Блэкберн П., Ван Бентем Дж. И Вольтер Ф. (ред.), 2006. Справочник по модальной логике, Амстердам: Elsevier.
  • Боландер Т. и Блэкберн П., 2007. «Завершение гибридных таблиц», журнал «Логика и вычисления», 17: 517–554.
  • –––, 2009. «Концевые исчисления таблиц для гибридной логики, расширяющей K», в Сборнике методов для модальностей 5 (Электронные заметки в теоретической информатике: том 231), стр. 21–39.
  • Боландер Т. и Браунер Т., 2006. «Процедуры принятия решений на основе таблиц для гибридной логики», Журнал логики и вычислений, 16: 737–763.
  • Браунер Т., 2002. «Модальная логика, Истина и Модальность Мастера», журнал «Философская логика», 31: 359–386.
  • –––, 2011a. Гибридная логика и ее теория доказательств (Серия прикладной логики: том 37), Дордрехт-Гейдельберг-Берлин-Нью-Йорк: Springer.
  • –––, 2011b. «Интуиционистская гибридная логика: введение и обзор», Информация и вычисления, 209: 1437–1446.
  • –––, 2014a. «Гибридная логика первого порядка: введение и обзор», журнал «Логика» IGPL, 22: 155–165.
  • –––, 2014b. «Гибридно-логическое мышление в умах и задачах Салли-Энн», журнал «Логика, язык и информация», 23: 415–439.
  • Браунер Т., Блэкберн П. и Полянская И., 2016. «Задачи ложного убеждения второго порядка: анализ и формализация», по логике, языку, информации и вычислениям: 23-й международный семинар, WoLLIC (Конспект лекций) в области компьютерных наук: том 9803), с. 125–144. Гейдельберг: Спрингер.
  • Браунер Т. и де Пайва В., 2006. «Интуиционистская гибридная логика», Журнал прикладной логики, 4: 231–255.
  • Bull, R., 1970. «Подход к напряженной логике», Theoria, 36: 282–300.
  • Cerrito, S. and Cialdea, M., 2010. «Номинальное замещение при работе с глобальными и обратными модальностями», в разделе «Достижения в модальной логике» (том 8), стр. 57–74. Публикации колледжа.
  • Конради В., Горанко В. и Вакарелов Д., 2006. «Алгоритмическое соответствие и полнота в модальной логике II. Полиадические и гибридные расширения алгоритма SQEMA », Журнал логики и вычислений, 16: 579–612.
  • Copeland, J. (ed.), 1996. Логика и реальность: очерки наследия Артура Приора, Оксфорд: Clarendon Press.
  • Коста, Д. и Мартинс, Массачусетс, 2016. «Параконсистенция в гибридной логике», журнал «Логика и вычисления». DOI:
  • Franceschet, M. and de Rijke, M., 2006. «Проверка модели гибридной логики (с применением к полуструктурированным данным)», журнал прикладной логики, 4: 279–304.
  • Gabbay, D. and Woods, J. (eds.), 2006. Логика и модальности в двадцатом веке. Справочник по истории логики (том 7). Амстердам: Elsevier.
  • Гаргов Г., Горанко В., 1993. «Модальная логика с именами», журнал «Философская логика», 22: 607–636.
  • Горанко В., 1994. «Временная логика со ссылочными указателями», в материалах 1-й Международной конференции по временной логике (Конспект лекций по искусственному интеллекту: том 827), с. 133–148. Берлин: Спрингер.
  • –––, 1996. «Иерархии модальной и временной логики с ссылочными указателями», Журнал логики, языка и информации, 5: 1–24.
  • Горанко В., Вакарелов Д., 2001. «Формулы Сахквиста в гибридной полиадической модальной логике», Журнал логики и вычислений, 11: 737–754.
  • Хансен, JU, 2010. «Завершение таблиц для динамической эпистемической логики», в материалах шестого семинара по методам модальностей (M4M-6 2009) (Электронные заметки в теоретической информатике: том 262), стр. 141–156.
  • –––, 2011. Набор логических инструментов для моделирования знаний и информации в многоагентных системах и социальной эпистемологии, кандидатская диссертация, Университет Роскилле.
  • Хансен, JU, Боландер, T. и Браунер, T., 2015. «Многозначная гибридная логика», журнал «Логика и вычисления». DOI:
  • Hasle, P. and Øhrstrøm, P., 2016. «Парадигма Приора для изучения времени и его методологической мотивации», Synthese, 193: 3401–3416.
  • Йоргенсен К. Ф., Блэкберн П., Боландер Б. и Браунер Т., 2016. «Доказательства синтетической полноты для систем таблиц Селигмана», «Достижения в модальной логике» (том 11), с. 302–321. Публикации колледжа.
  • Камински, М. и Смолка, Г., 2009. «Конечные системы таблиц для гибридной логики с различием и обратностью», журнал «Логика, язык и информация», 18: 437–464.
  • Kamp, H., 1971. «Формальные свойства« сейчас »», Theoria, 37: 237–273.
  • Крахт, М. и Вольтер, Ф., 1997. «Результаты моделирования и переноса в модальной логике - обзор», Студия Логика, 59: 149–177.
  • Ланге, М., 2009. «Проверка модели гибридной логики», журнал «Логика, язык и информация», 18: 465–491.
  • Мюллер, Т., 2007. «Интенсивный логический универсализм Приора», Logique et Analyze, 50: 223–252.
  • Эрстрем, П. и Хасле, П., 1993. «Повторное открытие напряженной логики А. Н. Приора», Эркеннтнис, 39: 23–50.
  • –––, 1995. Темпоральная логика. От древних идей к искусственному интеллекту, Дордрехт: Kluwer.
  • –––, 2006. «Логика А. Н. Приора», в Gabbay and Woods (2006), с. 399–446.
  • Пасси С. и Тинчев Т., 1985. «Квантификаторы в комбинаторных PDL: полнота, определимость, неполнота», Основы теории вычислений FCT 85 (Конспект лекций в области компьютерных наук: том 199), стр. 512–519. Берлин: Спрингер.
  • Пасси С. и Тинчев Т., 1991. «Очерк комбинаторной динамической логики», Информация и вычисления, 93: 263–332.
  • До, AN, 1967. Прошлое, настоящее и будущее, Оксфорд: Кларендон Пресс.
  • –––, 1968. Статьи о времени и времени, Оксфорд: Кларендон Пресс.
  • –––, 2003. Статьи о времени и времени, Оксфорд: издательство Оксфордского университета. Второе пересмотренное и расширенное издание Prior (1968). Под редакцией П. Хасле, П. Орстрёма, Т. Браунера и Дж. Коупленда.
  • Приор, А. Н. и Файн, К., 1977. Worlds, Times and Selves, London: Duckworth. На основе рукописей Приора с предисловием и постскриптумом К. Файна.
  • Райхенбах, Х., 1947. Элементы символической логики, Нью-Йорк: Свободная пресса.
  • Селигман, Дж., 1997. «Логика правильного описания», в книге «Достижения в интенсивной логике» (Серия прикладной логики: Том 7), с. 107–135. Kluwer.
  • Селигман, J., 2001. «Интернализация: случай гибридной логики», журнал «Логика и вычисления», 11: 671–689.
  • Сильван, Р., 1996. «Другие увядшие пни времени», в Copeland (1996), с. 111–130.
  • ten Cate, B., 2004. Теория моделей для расширенных модальных языков, кандидатская диссертация, Институт логики, языка и вычислений, Амстердамский университет.

Академические инструменты

значок сеп человек
значок сеп человек
Как процитировать эту запись.
значок сеп человек
значок сеп человек
Предварительный просмотр PDF-версию этой записи в обществе друзей SEP.
значок Inpho
значок Inpho
Посмотрите эту тему в Проекте интернет-философии онтологии (InPhO).
Фил документы
Фил документы
Расширенная библиография для этой записи в PhilPapers со ссылками на ее базу данных.

Другие интернет-ресурсы

Рекомендуем: