首页/论文/2002.04855

arXiv 2002.048552020-02-12math.LOcs.LO

Labelled calculi for quantified modal logics with definite descriptions

Eugenio Orlandelli

英文摘要：

We introduce labelled sequent calculi for quantified modal logics with definite descriptions. We prove that these calculi have the good structural properties of G3-style calculi. In particular, all rules are height-preserving invertible, weakening and contraction are height-preserving admissible and cut is admissible. Finally, we show that each calculus gives a proof-theoretic characterization of validity in the corresponding class of models.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

On the Correspondence between Nested Calculi and Semantic Systems for Intuitionistic Logics

This paper studies the relationship between labelled and nested calculi for propositional intuitionistic logic, first-order intuitionistic logic with non-constant domains and first-order intuitionistic logic with constant domains. It is shown that Fitting's nested calculi naturally arise from their corresponding labelled calculi--for each of the aforementioned logics--via the elimination of structural rules in labelled derivations. The translational correspondence between the two types of systems is leveraged to show that the nested calculi inherit proof-theoretic properties from their associa…

2021-04-19cs.LOmath.LO

On Deriving Nested Calculi for Intuitionistic Logics from Semantic Systems

This paper shows how to derive nested calculi from labelled calculi for propositional intuitionistic logic and first-order intuitionistic logic with constant domains, thus connecting the general results for labelled calculi with the more refined formalism of nested sequents. The extraction of nested calculi from labelled calculi obtains via considerations pertaining to the elimination of structural rules in labelled derivations. Each aspect of the extraction process is motivated and detailed, showing that each nested calculus inherits favorable proof-theoretic properties from its associated la…

2020-02-03cs.LOmath.LO

使用标号矢列演算证明 Craig 与 Lyndon 插值

Proving Craig and Lyndon Interpolation Using Labelled Sequent Calculi

本文将证明 Craig 与 Lyndon Interpolation 的方法扩展至标号矢列演算，提供了基于 Kripke-frame 表征的充分准则，并证明无量词 Horn 公式可定义的框架类对应具有 IPs 的逻辑，涵盖模态立方体与传递 Geach 逻辑族。

2016-01-21cs.LOmath.LO

基于格的模态逻辑的带标签演算

Labelled calculi for lattice-based modal logics

本文为基本正规非分配模态逻辑L及其31个公理化扩张提出了带标签矢列演算，并证明了其可靠性、完备性、保守性、切割消去与子公式性质，展示了为LE-逻辑类系统引入带标签演算的统一方法。

2024-01-18math.LO

粗糙概念逻辑的加标演算

Labelled calculi for the logics of rough concepts

本文针对非分配正规模态逻辑 L 及其扩张，利用丰富化形式背景的一阶原子公式作标签，构建可靠完备的加标矢列演算，并扩展得到粗糙形式背景逻辑的证明系统。

2024-01-18math.LO

Cut-free Calculi and Relational Semantics for Temporal STIT Logics

Technische Universität Wien（维也纳工业大学）

We present cut-free labelled sequent calculi for a central formalism in logics of agency: STIT logics with temporal operators. These include sequent systems for Ldm, Tstit and Xstit. All calculi presented possess essential structural properties such as contraction- and cut-admissibility. The labelled calculi G3Ldm and G3TSTIT are shown sound and complete relative to irreflexive temporal frames. Additionally, we extend current results by showing that also XSTIT can be characterized through relational frames, omitting the use of BT+AC frames.

2019-04-22cs.AIcs.LOmath.LO

更多相关论文收起更多论文

Refining Labelled Systems for Modal and Constructive Logics with Applications

Australian National University（澳大利亚国立大学）；Laboratoire d’informatique de l’École polytechnique（巴黎综合理工学院计算机实验室）

This thesis introduces the "method of structural refinement", which serves as a means of transforming the relational semantics of a modal and/or constructive logic into an 'economical' proof system by connecting two proof-theoretic paradigms: labelled and nested sequent calculi. The formalism of labelled sequents has been successful in that cut-free calculi in possession of desirable proof-theoretic properties can be automatically generated for large classes of logics. Despite these qualities, labelled systems make use of a complicated syntax that explicitly incorporates the semantics of the a…

2021-07-30cs.AIcs.DMcs.FL

量化命题演算与窄隐式证明

Quantified propositional calculi and narrow implicit proofs

Institute of Mathematics, Czech Academy of Sciences（捷克科学院数学研究所）

研究隐式命题证明系统中窄证明的概念，通过切割消去构造证明G_{i+1}等价于窄隐式G_i，并建立G_1与隐式归结的等价性。

2026-09-02cs.CCcs.LOmath.LO

Hypersequent calculi for non-normal modal and deontic logics: Countermodels and optimal complexity

We present some hypersequent calculi for all systems of the classical cube and their extensions with axioms $T$, $P$, $D$, and, for every $n\geq 1$, rule $RD^+_n$. The calculi are internal as they only employ the language of the logic, plus additional structural connectives. We show that the calculi are complete with respect to the corresponding axiomatisation by a syntactic proof of cut elimination. Then we define a terminating root-first proof search strategy based on the hypersequent calculi and show that it is optimal for coNP-complete logics. Moreover, we obtain that from every saturated …

2020-06-09cs.LOmath.LO

双模可证逻辑的证明论

Proof Theory for Bimodal Provability Logics

University of Bern（伯尔尼大学）

本文首次为双模可证逻辑设计非标记的序列表演算，涵盖CS、CSM和ER逻辑，并通过非非Wellfounded版本建立切消过程，证明了这些逻辑具有统一的Lyndon插值性质。

2026-05-14math.LO

Automating Agential Reasoning: Proof-Calculi and Syntactic Decidability for STIT Logics

Technische Universität Wien（维也纳技术大学）

This work provides proof-search algorithms and automated counter-model extraction for a class of STIT logics. With this, we answer an open problem concerning syntactic decision procedures and cut-free calculi for STIT logics. A new class of cut-free complete labelled sequent calculi G3LdmL^m_n, for multi-agent STIT with at most n-many choices, is introduced. We refine the calculi G3LdmL^m_n through the use of propagation rules and demonstrate the admissibility of their structural rules, resulting in auxiliary calculi Ldm^m_nL. In the single-agent case, we show that the refined calculi Ldm^m_nL…

2020-02-15cs.AIcs.LOcs.MA

量化模态逻辑的嵌套序列

Nested Sequents for Quantified Modal Logics

本文针对带不同论域的量化模态逻辑构建嵌套序列演算，证明其具备良好结构性质、与公理系统等价且可靠完备，并说明存在谓词可表达时演算具有内部性。

2023-11-08cs.LOmath.LO

Logics of Formal Inconsistency enriched with replacement: an algebraic and modal account

It is customary to expect from a logical system that it can be algebraizable, in the sense that an algebraic companion of the deductive machinery can always be found. Since the inception of da Costa's paraconsistent calculi $C_n$, algebraic equivalents for such systems have been sought. It is known, however, that these systems are not self-extensional (i.e., they do not satisfy the replacement property). More than this, they are not algebraizable in the sense of Blok-Pigozzi. The same negative results hold for several systems of the hierarchy of paraconsistent logics known as Logics of Formal …

2021-05-20math.LO