Модальная клаузальная форма
Модальная клаузальная форма , также известная как нормальная форма, разделенная модальными уровнями (SNF ml ). [1] и нормальная форма Минта , [2] является нормальной формой формул модальной логики .
Такая нормальная форма обычно используется для автоматического доказательства теорем с использованием методов табличного исчисления и разрешающего исчисления из -за ее преимуществ, заключающихся в улучшении пространственных границ и улучшенных процедурах принятия решений. В нормальной модальной логике любой набор формул можно преобразовать в эквивалентно выполнимый набор формул в этой нормальной форме. [3]
В мультимодальной логике , где a представляет агента, соответствующего функции отношения доступности в семантике Крипке , формула в этой нормальной форме представляет собой соединение предложений, помеченных модальным уровнем (т. е. количеством вложенных модальностей). Каждый модальный уровень состоит из трех следующих форм.
- Буквальное предложение: дизъюнкция пропозициональных литералов. .
- Положительное предложение a : где и являются пропозициональными литералами.
- Отрицательное предложение a : где и являются пропозициональными литералами.
Эти три формы также называются cpl -предложениями, блок -предложениями и диа -предложениями соответственно. [4] Обратите внимание, что любое предложение в конъюнктивной нормальной форме (CNF) также является буквальным предложением в этой нормальной форме.
Ссылки
[ редактировать ]- ^ Налон, Клаудия; Хуштадт, Ульрих; Диксон, Клэр (8 ноября 2015 г.). Модальное исчисление разрешения для K . TABLEAUX 2015: Автоматизированное рассуждение с помощью аналитических таблиц и связанных с ними методов, Вроцлав, Польша. Конспекты лекций по информатике. Том. 9323. Чам: Спрингер. стр. 185–200. дои : 10.1007/978-3-319-24312-2_13 . ISBN 978-3-319-24312-2 .
- ^ Минц, Григорий (1990). Системы генценовского типа и правила разрешения, часть I. Логика высказываний . COLOG 1988: Международная конференция по компьютерной логике. Конспекты лекций по информатике. Том. 417. Берлин, Гейдельберг: Шпрингер. дои : 10.1007/3-540-52335-9_55 . ISBN 978-3-540-46963-6 .
- ^ Горе, Раджив; Нгуен, Линь Ань (12 августа 2009 г.). «Клаузальные таблицы для мультимодальной логики убеждений» . Фундамента информатики . 94 (1). Польское математическое общество, IOS Press: 21–40. дои : 10.3233/FI-2009-115 .
- ^ Горе, Раджив; Киккерт, Кормак (6 сентября 2021 г.). CEGAR-Tableaux: улучшенная модальная выполнимость посредством обучения модальным предложениям и SAT . TABLEAUX 2021: Автоматизированное рассуждение с помощью аналитических таблиц и связанных с ними методов, Бирмингем, Великобритания. Конспекты лекций по информатике. Том. 12842. Чам: Спрингер. стр. 74–91. дои : 10.1007/978-3-030-86059-2_5 . ISBN 978-3-030-86059-2 .
 | Эта формальным методам, статья, посвященная незавершена . Вы можете помочь Википедии, расширив ее . |
