?
Grammar Logics in Nested Sequent Calculus: Proof Theory and Decision Procedures
P. 516–537.
Tiu A., Яновский Е. А., Goré R.
Кудинов А. В., Мясников К. М., Математика и теоретические компьютерные науки 2025 Т. 3 № 2 С. 58–84
В работе доказывается, что для слабо транзитивных логик с универсальной модальностью, проверку выполнимости формулы для которых можно произвести в PSPACE}, добавление аксиомы связности не увеличивает сложность этой проверки, причем строится явный алгоритм, который решает эту задачу. ...
Добавлено: 14 октября 2025 г.
Ma M., Пиетаринен А. Ю., , in: Electronic Proceedings in Theoretical Computer ScienceVol. 243.: [б.и.], 2017. P. 91–103.
Добавлено: 12 ноября 2018 г.
Ma M., Пиетаринен А. Ю., Review of Symbolic Logic 2020 Vol. 13 No. 3 P. 509–540
Добавлено: 3 ноября 2018 г.
College Publications, 2016.
Logic deals with the fundamental notions of truth and falsity. Modal logic arose from the philosophical study of “modes of truth” with the two most common modes being “necessarily true” and “possibly true”. Research in modal logic now spans the spectrum from philosophy, computer science and mathematics using techniques from relational structures, universal algebra, topology, ...
Добавлено: 20 сентября 2018 г.
College Publications, 2018.
Logic deals with the fundamental notions of truth and falsity. Modal logic arose from the philosophical study of “modes of truth” with the two most common modes being “necessarily true” and “possibly true”. Research in modal logic now spans philosophy, computer science, and mathematics, using techniques from relational structures, universal algebra, topology, and proof theory.
These ...
Добавлено: 20 сентября 2018 г.
Шамканов Д. С., Mathematical notes 2014 Vol. 96 No. 4 P. 575–585
В статье рассматривается исчисление секвенций для логики доказуемости GL, доказуемость в котором основана на понятии циклического вывода. В отличие от обычных выводов, циклический вывод можно представлять себе не как дерево, но как граф, содержащий циклы. Используя данное понятие, мы даем синтаксическое доказательство интерполяционного свойства Линдона для логики GL. ...
Добавлено: 13 августа 2014 г.
Blute R., Panangaden P., Slavnov Sergey, Applied Categorical Structures 2012 Vol. 20 No. 3 P. 209–228
Добавлено: 18 февраля 2013 г.
Blute R., Panangaden P., Slavnov S. A., Applied Categorical Structures 2012 Vol. 20 No. 3 P. 209–228
В статье предлагается категорная модель системы глубокого вывода BV, опеределенной Гульеми. В системах глубокого вывода реализована идея дедукций внутри формулы на любой глубине . Стандартные правила исчислений секвенций применимы только к корню дерева подформул, тогда как в этих новых системах можно вносить изменения в любой позиции дерева. В частности, глубокий вывод позволяет синтаксическое описание логик, ...
Добавлено: 28 декабря 2012 г.