Takuma Imamura, Shuya Matsumoto, Shin Quawai
We report on the current status of our on-going project to develop well-behaved hypersequent calculi for intermediate predicate logics, such as the linearity axiom $\mathbf{LIN}\colon\left(φ\toψ\right)\lor\left(ψ\toφ\right)$ and the constant domain axiom $\mathbf{CD}\colon\forall x\left(φ\lorψ\left(x\right)\right)\toφ\lor\forall xψ\left(x\right)$.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
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 …
We investigate a recent proposal for modal hypersequent calculi. The interpretation of relational hypersequents incorporates an accessibility relation along the hypersequent. These systems give the same interpretation of hypersequents as Lellman's linear nested sequents, but were developed independently by Restall for S5 and extended to other normal modal logics by Parisi. The resulting systems obey Dosen's principle: the modal rules are the same across different modal logics. Different modal systems only differ in the presence or absence of external structural rules. With the exception of S5,…
Hypersequent Calculi Have Ackermannian Complexity
研究显示，超序列演算在扩展可交换全拉姆贝克算术时，其证明复杂度可被限制在阿克曼层级，而非超阿克曼层级。
We define a bi-directional embedding between hypersequent calculi and a subclass of systems of rules (2-systems). In addition to showing that the two proof frameworks have the same expressive power, the embedding allows for the recovery of the benefits of locality for 2-systems, analyticity results for a large class of such systems, and a rewriting of hypersequent rules as natural deduction rules.
Grafting Hypersequents onto Nested Sequents
本文提出结合嵌套序列与超序列的嫁接超序列框架，为K5、KD5等模态逻辑提供具备语法切消和最优复杂度证明搜索的新型演算。
Takeuti and Titani have introduced and investigated a logic they called intuitionistic fuzzy logic. This logic is characterized as the first-order Goedel logic based on the truth value set [0,1]. The logic is known to be axiomatizable, but no deduction system amenable to proof-theoretic, and hence, computational treatment, has been known. Such a system is presented here, based on previous work on hypersequent calculi for propositional Goedel logics by Avron. It is shown that the system is sound and complete, and allows cut-elimination. A question by Takano regarding the eliminability of the Ta…
Following G. Mints(Kluwer 2000 and draft 2013), we present terminating and bicomplete proof searches in multi-succedent sequent calculi for intuitionistic propositional logic, fragments of intuitionistic predicate logic and full intuitionistic predicate logic in the spirit of Schuette's schema.
We study propositional and first-order Gödel logics over infinitary languages which are motivated semantically by corresponding interpretations into the unit interval [0,1]. We provide infinitary Hilbert-style calculi for the particular (propositional and first-order) cases with con-/disjunctions of countable length and prove corresponding completeness theorems by extending the usual Lindenbaum-Tarski construction to the infinitary case for a respective algebraic semantics via complete linear Heyting algebras. We provide infinitary hypersequent calculi and prove corresponding cut-elimination t…
Proving Craig and Lyndon Interpolation Using Labelled Sequent Calculi
本文将证明 Craig 与 Lyndon Interpolation 的方法扩展至标号矢列演算，提供了基于 Kripke-frame 表征的充分准则，并证明无量词 Horn 公式可定义的框架类对应具有 IPs 的逻辑，涵盖模态立方体与传递 Geach 逻辑族。
Proof Theory for Bimodal Provability Logics
本文首次为双模可证逻辑设计非标记的序列表演算，涵盖CS、CSM和ER逻辑，并通过非非Wellfounded版本建立切消过程，证明了这些逻辑具有统一的Lyndon插值性质。
We present some new methods for logical deduction, based on ideas from ground theory. Roughly speaking, in our calculi a typical deduction will proceed as follows: we first analyse the premiss down to its ultimate grounds; then we discard information irrelevant to the conclusion; and then we synthesize the conclusion up from its ultimate grounds. We give a series of calculi for: classical propositional logic (Chapter 1); classical predicate logic (Chapter 2); modal propositional logic and modal predicate logic (Chapter 3); and some relevantistic fragments of these various systems (Chapters 4 a…
Optimizing Proof-Search via Linearization for Gödel-Löb Logic with Tree-Hypersequents
针对 GL 逻辑在树-超矢列系统 CSGL 中的可判定性证明和 PSPACE 证明搜索算法问题，提出线性化方法，仅构建单分支推导和树矢列，实现 PSPACE 最优复杂度，并提取有限反模型验证算法正确性。
The problems of logical translation of axiomatizations and the choice of primitive operators have surfaced several times over the years. An early issue was raised by H. Hi{\. z} in the 1950s on the incompleteness of translated calculi. Further pertinent work, some of it touched on here, was done in the 1970s by W. Frank and S. Shapiro, as well as by others in subsequent decades. As we shall see, overlooking such possibilities has led to incorrect claims of completeness being made (e.g. by J. L. Bell and A. B. Slomson as well as J. N. Crossley) for axiomatizations of classical predicate logic o…
The development of compositional distributional models of semantics reconciling the empirical aspects of distributional semantics with the compositional aspects of formal semantics is a popular topic in the contemporary literature. This paper seeks to bring this reconciliation one step further by showing how the mathematical constructs commonly used in compositional distributional models, such as tensors and matrices, can be used to simulate different aspects of predicate logic. This paper discusses how the canonical isomorphism between tensors and multilinear maps can be exploited to simulate…
Modelling of logical systems by means of their fragments
本文通过研究逻辑系统的片段归约，揭示了非经典逻辑的算法复杂性，并提供了新的复杂性界限和克里普克不完全性结果。
Justification Logic for Intuitionistic Modal Logic (Extended Technical Report)
本文为Fischer Servi的直觉主义模态逻辑IK及其扩展提供证明逻辑对应物，通过扩展证明项语法、公理化和无切嵌套序列系统实现语法实现。
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。