arXivDaily arXiv每日学术速递 周一至周五更新
arXiv周末暂无论文更新,休息一下吧,周末愉快~~

面向自动证明论语义:三维K3与LP的推理-行为语义

Towards Automated Proof-Theoretic Semantics: Inference-Behaviour Semantics for 3-Dimensional K3 and LP

Sophie Nagler

arXiv 2608.02654首次发表:更新:

AI 中文总结

本文通过案例研究将推理-行为语义(I-bS)扩展至三维相继式演算,构建K3与LP的I-bS并验证其联结词意义的保守性,为I-bS与MUltlog整合以实现多值逻辑I-bS生成的自动化奠定基础。

AI 中文摘要

推理-行为语义(I-bS)是一种基于相继式演算的子结构证明论语义(P-tS)方法,专注于建模不同逻辑间联结词意义的关系。本文开展案例研究,探究I-bS如何扩展至任意有限多维相继式演算,为此给出三维相继式演算K3(强克莱尼逻辑)与LP(悖论逻辑)的I-bS。研究发现K3与LP的联结词具有相同意义,且该意义保守扩展了对应经典LK联结词的意义。本文将此结果置于I-bS与MUltlog整合的更大项目框架下,目标是采用MUltlog风格系统自动生成任意多值逻辑的I-bS,为P-tS方法的计算自动化作出贡献。

英文摘要

Inference-behaviour Semantics (I-bS) is a sequent calculus-based substructural approach to proof-theoretic semantics (P-tS), focussed on modelling the relationships of connective meanings across different logics. This paper provides a case study of how I-bS can be extended to any finitely multi-dimensional sequent calculus. To this end, we give I-bS for the 3-dimensional sequent calculi K3 (Strong Kleene) and LP (Logic of Paradox). We find that the K3 and LP connectives have the same meaning and that their meaning conservatively extends the meaning of the corresponding classical LK connectives. We situate this result within the wider project of integrating I-bS with MUltlog. The goal is to automate the generation of I-bS for arbitrary multi-valued logics using a MUltlog-style system, thus contributing towards the computational automation of P-tS approaches.

Comments48 pages, 2 figures, 5 tables

论文原文

arXiv 摘要页 · PDF 原文 · HTML 原文

↑