A Sketch of a Proof-Theoretic Semantics for Necessity
本文认为，证明理论语义的必要性达米特和Prawitz的框架内。受Pfenning和Davies系统的启发，直觉主义逻辑的语言被一个高阶算子扩展，该算子捕获了有效性的概念。相对必要性的概念是根据它来定义的，它表达了一个推论的假设和结论之间的必要联系。
2021-07-29 cs.LO math.LO
From Proof-theoretic Validity to Base-extension Semantics for Intuitionistic Propositional Logic
本文针对直觉主义命题逻辑，论证其基扩展语义涵盖了一种基于消去规则的证明论有效性版本的陈述内容，既阐释了基扩展语义的运作原理，也证明了该版本证明论有效性的完备性。
2024-09-12 cs.LO math.LO
Game-Theoretic Semantics for Alternating-Time Temporal Logic
我们介绍了交替时间时态逻辑（ATL）的博弈论语义（GTS）的版本。在GTS中，真理被定义为在语义评估博弈中获胜策略的存在，因此博弈论的视角出现在ATL的框架中的两个语义层面上：在策略算子的标准语义中的对象层面上，以及在元层面上，博弈论的逻辑语义被应用于ATL。我们统一这两个角度到专门为ATL设计的语义评估游戏。博弈论的角度，使我们能够确定新的变体的ATL语义的基础上限制的时间资源提供给验证者和证伪者的语义评估游戏。我们介绍和分析一个无界和（序数）有界的GTS，并证明这些是等价的标准（塔斯基风格）的成分语义。我们证明了在这两个版本的GTS中，ATL公式的真值总是可以在有限时间内确定的，即，而不需要构建无限的路径。我们还介绍了一个不等价的有界语义，并认为这是自然的逻辑和博弈论的角度来看。
2019-06-15 cs.GT cs.LO math.LO
Formal Component-Based Semantics
为提高程序设计语言语义的可伸缩性，提出了一种解决方案，即由Peter D.苔藓预计该框架也可以有效地用于模块化Meta理论推理。本文提出了一种形式化的定理证明器Coq的基于一致性的语义。它基于模块化SOS（SOS的一个变体），并且基本上使用了依赖类型，同时受益于类型类。这种形式化构成了对定理证明器中的模块化Meta理论形式化的贡献。作为一个小的例子，一个小型语言的确定性的模块化证明。
2011-08-16 cs.LO
Infinite Traces by Finality: a Sheaf-Theoretic Approach
本研究针对Kleisli范畴中终共代数无法通用刻画无限迹语义的问题，提出结合Kleisli范畴、序数层与受保护（余）递归的层论框架，引入受保护行为函子并证明温和条件下其终共代数可直接刻画无限迹。
2025-07-30 cs.LO
A proof theoretic basis for relational semantics
逻辑已被证明是必不可少的正式建模软件为基础的系统。这种形式化的描述，通常被称为规范，不仅作为需求文档和形式化，而且还为它们的分析和自动推理工具的开发提供了数学基础。逻辑学通常从其内在的两个方面来研究：句法和语义。后者的相关性在于这样一个事实，即对现实世界的现象进行逻辑描述，需要人们就人类如何解释和理解这些描述达成一致，以便系统可以根据其规范自信地构建。在更实际的方面，句法和语义之间的元逻辑关系决定了人们可以从某些分析技术的应用中得出的结论的重要方面，如模型检验。抽象模型理论（Abstract Model Theory）关于逻辑语言语义的数学观点）对于软件工程努力几乎没有实用价值。从我们的观点来看，值（可以分配给常量和变量的值）不应该仅仅是柏拉图式解释域中的点，而是可以通过规范签名上的术语命名的元素。简而言之，我们对那些需要任何语义信息而无法用可用语法表示的属性不感兴趣。在本文中，我们提出了一个框架，支持证明理论的形式化类的关系模型的行为逻辑语言，其域的话语保证只形成命名值。
2021-07-17 cs.LO
Game-Theoretic Semantics for ATL+ with Applications to Model Checking
我们开发了完整的交替时间时态逻辑ATL* 的片段ATL+的博弈论语义（GTS），基本上扩展了最近推出的GTS ATL。我们首先表明，新的博弈论语义是等价的ATL+的标准语义（基于完美的召回策略）。然后，我们提供了一个分析，基于新的语义，模型检查ATL+所需的内存和时间资源。基于此，我们确定仅使用非常有限的内存量的策略就足以满足ATL+的需求。此外，使用GTS，我们提供了一个新的算法模型检查的ATL+和确定一个自然的层次结构的易处理的片段ATL+扩展ATL。
2019-06-14 cs.GT cs.LO math.LO
Proof-Theoretic Semantics, a Problem with Negation and Prospects for Modality
本文讨论了证明论语义学，该项目规定的逻辑常数的意义方面的推理规则，他们。我专注于迈克尔达米特和达格Prawitz的哲学动机，并给出精确的特点的关键概念的和谐与稳定，放置在证明正常化的结果，在系统的自然演绎的背景下。我指出了一个问题，在这个框架中定义否定的意义和前景的解释模态算子的意义的推理规则。
2021-07-29 cs.LO math.LO
Dialetheism, Game Theoretic Semantics, and Paraconsistent Team Semantics
我们介绍了一个变体的依赖逻辑中的真理定义不存在的获胜策略的支持者（Eloise）在语义游戏中，但在缺乏获胜策略的对手（Abelard）。我们证明了这种语言是一阶逻辑的保守但次协调的扩展，它的有效性问题可以归结为一阶逻辑的有效性问题，它能够表达自己的真值和有效性谓词，并且它在表达上等价于通用二阶逻辑。此外，我们证明了一个次协调的非依赖逻辑公式是一致的当且仅当它是等价于一些一阶逻辑句子;另一方面，我们表明，所有的次协调依赖逻辑句子等价于一些一阶句子就真（但不一定就假）。
2014-03-14 cs.LO math.LO
Proof-theoretic Semantics for Intuitionistic Multiplicative Linear Logic (Extended Abstract)
本文首次探索子结构逻辑的证明论语义，提出直觉主义乘法线性逻辑（IMLL）的基础扩展语义，其中逻辑常量定义均采用消去规则形式，并证明了其可靠性与完备性。
2024-11-12 cs.LO math.LO
A Proof-Theoretic Approach to the Semantics of Classical Linear Logic
University College London（伦敦大学学院）
本文提出通过基础扩展语义（BeS）和基础支持的概念，从证明论角度研究经典线性逻辑的乘法-加法片段（MALL）语义学。
2026-02-27 cs.LO math.LO
Towards a Proof-Theoretic Analysis of Incorrect/Incomplete Proofs
Technische Universität Wien（维也纳工业大学）
本文基于希尔伯特epsilon演算，形式化分析不正确或不完整证明的语义修复机制，提出通过语义投影和最弱前置条件修正推导，并证明扩展的第一epsilon定理具有虚假容忍性。
2026-09-17 cs.LO
Proceedings Twentieth International Symposium on Logical and Semantic Frameworks with Applications
本文介绍在巴西利亚举行的LSFA 2025会议论文集，说明其旨在连接逻辑与语义框架领域的理论研究与实践反馈。
2025-09-28 cs.LO
A Game-Semantic Model of Computation, Revisited: an Automata-Theoretic Perspective
在以前的工作中，我们已经给出了一个新颖的，游戏语义计算模型，在一个内在的，非归纳和非公理化的方式，这是类似于图灵机，但超越了自然数的计算，例如，高阶计算作为主要定理的工作，它已被证明，游戏语义模型可以执行所有的计算的程序设计语言PCF。本文从自动机理论的角度重新审视了这一结果：它表明，确定性的非擦除下推自动机的输入磁带配备有简单的有向边缘之间的细胞可以实现所有的游戏语义PCF计算，其中的边缘，而不是限制自动机可以读取磁带的细胞。这是一个数学上非常令人惊讶的现象，因为众所周知，更强大的非确定性擦除下推自动机严格地弱于图灵机（在乔姆斯基层次结构中），更不用说PCF了。
2019-12-14 cs.LO math.LO
A comparison of three kinds of monotonic proof-theoretic semantics and the base-incompleteness of intuitionistic logic
本文比较可归约性语义与基语义（含Sandqvist变体）三种单调证明论语义，建立二者间的转换条件，并据此讨论直觉主义逻辑的基完备性问题。
2025-11-08 cs.LO math.LO
Towards arrow-theoretic semantics of ontologies: conceptories
在知识表示领域范畴论方法和逻辑方法的努力中，我们提出了概念的概念。我们认为交集/工会和其他结构的概念表达替代范畴理论（共）限制，并显示它们具有类似的功能（投影，在）喷射。然后，我们简要地讨论了建立在概念的基础上的形式系统的开发方法，并描述了这种系统的具体本体的可能应用。
2010-08-07 cs.AI cs.LO math.CT
Towards Automated Proof-Theoretic Semantics: Inference-Behaviour Semantics for 3-Dimensional K3 and LP
Institute for Logic, Language and Computation (ILLC) University of Amsterdam（阿姆斯特丹大学逻辑、语言与计算研究所）；Arché Research Centre University of St Andrews（圣安德鲁斯大学Arché研究中心）
本文通过案例研究将推理-行为语义（I-bS）扩展至三维相继式演算，构建K3与LP的I-bS并验证其联结词意义的保守性，为I-bS与MUltlog整合以实现多值逻辑I-bS生成的自动化奠定基础。
2026-08-05 cs.LO math.LO
Proof-theoretic Semantics for Second-order Logic
本文为二阶逻辑发展了基于基础扩展语义的证明论语义，通过改变原子系统类别获得经典与直觉主义版本，证明其可靠性与完备性等价于 Henkin 解释，将二阶量化重构为系统替换，为高阶逻辑提供了哲学轻量且富有表达力的语义基础。
2025-08-11 cs.LO math.LO
Base-extension Semantics for Intuitionistic Modal Logics
本文为Simpson直觉主义模态逻辑建立基扩展语义，并证明其相对自然演绎系统的可靠性与完备性。
2025-07-09 cs.LO math.LO
Proof-theoretic Semantics for First-order Logic
本文为一阶经典逻辑的证明论语义提供了一种初等、构造性且原生的完备性证明，并同时给出一阶直觉主义逻辑的可靠性与完备性证明。
2025-07-17 cs.LO math.LO
Categorical Proof-Theoretic Semantics
本研究将Sandqvist的直觉主义命题逻辑基扩展语义与预层范畴证明论关联，从范畴论重构可靠性与完全性论证，证明其构造的自然性，并指出该语义可视为层范畴中的自然析取。
2024-02-01 cs.LO math.CT math.LO
Game-theoretic Investigation of Intensional Equalities
本文提出了一个新的马丁-洛夫类型论（MLTT）的游戏语义，其中每个游戏都配备了选定的同构策略，表示（计算）证明（内涵）之间的平等的游戏策略。这些同构策略解释了MLTT中的命题等式。作为一个主要的结果，我们已经得到了第一个游戏语义MLTT，反驳了唯一性的身份证明（UIP）的原则，并验证了univalence公理（UA），但它不模拟非平凡的高等平等。分类，我们的模型形成了一个子结构的经典群胚模型的MLTT霍夫曼和Streicher。类似的路径从广群模型的$ω$广群模型，我们正计划推广游戏语义产生一个欧米茄广群结构来解释非平凡的同伦类型论（HoTT）的高等平等。
2017-04-20 cs.LO
Proceedings 16th Logical and Semantic Frameworks with Applications
本卷包含第十六届逻辑和语义框架与应用程序（LSFA 2021）的后续程序。会议于2021年7月23日至24日在网上举行，由阿根廷布宜诺斯艾利斯大学组织。LSFA旨在使研究人员和学生对逻辑和语义框架及其应用的理论和实践方面感兴趣。所涵盖的主题包括证明理论，类型论和重写理论，规范和演绎语言，以及语言和系统的形式语义。
2022-04-07 cs.LO
A Domain-Theoretic Approach to Statistical Programming Languages
我们给一个域理论语义的统计程序设计语言，使用普通的老类dcpos，在对比一些更复杂的最近的建议。值得注意的是，我们的最小估值单子是可交换的，这允许程序转换，置换独立随机抽取的顺序，正如人们所期望的那样。琼斯和普洛特金的连续估值单子中没有类似的性质。我们使用精确的实数运算，而不是使用真实数，为可能的实现提供了一个桥梁。（这里不讨论实现本身。）而值得注意的是，我们表明，限制自己的最小估值并没有限制我们太多：所有措施的真正的线可以模拟域$\mathbf{I}\mathbb{R}_\bot$上的最小估值的真正的算术。我们给我们的语言的三个操作语义，我们表明，他们都是足够的指称语义。我们还探索了相当多的例子，以证明我们的语义计算完全符合预期，并为了揭穿神话，即基于连续映射的语义将不足以表达仅使用紧支持的度量来编码非紧支持的度量，或者通过非连续密度函数编码度量。我们的例子还包括一些有用的，非平凡的情况下，分布在高阶对象。
2021-09-13 cs.LO
A Category-Theoretic Perspective on Approximation Fixpoint Theory
该研究从范畴论视角探讨近似不动点理论（AFT），AFT是研究非单调逻辑语义的抽象代数框架，应用广泛，研究目标是将其提升到更通用的构造性知识框架。
2025-02-13 cs.LO
Bounded game-theoretic semantics for modal mu-calculus
我们引入了一个新的博弈论语义（GTS）的模态μ演算。我们所谓的有界GTS取代奇偶游戏与替代评估游戏，只有有限的路径出现，无限的路径是不需要的，即使当考虑的过渡系统是无限的。新的游戏提供了替代方法的各种建设的框架中的μ演算。例如，它们已经成功地用作一种方法的基础，这种方法导致逻辑的自然公式大小游戏。虽然我们的主要重点是介绍新的GTS，我们也考虑一些应用程序来演示其用途。例如，我们考虑一个自然的模型转换过程，减少模型检查游戏，检查一个单一的，固定的公式在构建的模型，我们还使用GTS识别新的替代变种的μ演算与PTime模型检查。
2020-05-21 cs.LO math.LO
Inferentialist Game Semantics (Extended Abstract)
University College London（伦敦大学学院）；Institute of Philosophy, University of London（伦敦大学哲学研究所）
该研究探讨推理主义博弈语义，利用类似技术建立基扩展语义（B - eS）与海兰德 - 翁博弈语义的完全抽象关联，并通过4x4数独示例说明语义，为逻辑系统提供了基于证明计算的内涵意义理论。
2026-07-23 cs.LO math.LO
Proceedings 17th International Workshop on Logical and Semantic Frameworks with Applications
本卷包含由巴西米纳斯吉拉斯联邦大学组织的第十七届逻辑和语义框架与应用（LSFA 2022）的后续程序。由于COVID-19疫情，会议于2022年9月23日至24日混合举行。LSFA旨在汇集对逻辑和语义框架及其应用的理论和实践方面感兴趣的研究人员和学生。所涵盖的主题包括证明理论，类型论和重写理论，规范和演绎语言，以及语言和系统的形式语义。
2023-03-22 cs.LO
Bounded Game-Theoretic Semantics for Modal Mu-Calculus and Some Variants
我们引入了一个新的博弈论语义（GTS）的模态μ演算。我们所谓的有界GTS取代奇偶游戏与替代评估游戏，只有有限的路径出现，无限的路径是不需要的，即使当考虑的过渡系统是无限的。新的游戏提供了替代方法的各种建设的框架中的μ演算。例如，它们已经成功地用作一种方法的基础，这种方法导致逻辑的自然公式大小游戏。虽然我们的主要重点是介绍新的GTS，我们也考虑一些应用程序来演示其用途。例如，我们考虑一个自然的模型转换过程，减少模型检验游戏，检查一个单一的，固定的公式在构建的模型，我们还使用GTS识别新的替代变种的μ演算与PTime模型检验。
2020-09-23 cs.CC cs.LO
Fixpoint & Proof-theoretic Semantics for CLP with Qualification and Proximity
在过去的几十年里，逻辑程序设计中的不确定性已经被研究，涉及经典LP范式的各种扩展和不同的应用。现有的建议依赖于不同的方法，如基于不确定真值的子句注释，作为不确定真值的概括的资格值，以及基于邻近关系的统一。另一方面，CLP方案已经确立了自己作为一个强大的扩展LP，支持高效的计算在专门的领域，同时保持一个干净的声明语义。在这份报告中，我们提出了一个新的计划SQCLP设计作为CLP的扩展，支持资格值和邻近关系。我们表明，以前的几个建议可以被视为新方案的特殊情况下，通过部分实例化。我们提出了一个声明性的语义SQCLP是基于可观的，提供不动点和证明理论的最小程序模型的特征，以及实现独立的概念的目标解决方案。
2011-01-14 cs.LO cs.PL
Proof-theoretic Semantics for the Logic of Bunched Implications
本文为捆绑蕴含逻辑提出一种基扩展语义，系统组合IPL与IMLL的B-eS，以处理捆绑结构的复杂性，并展示其在安全建模中的应用。
2024-11-11 cs.LO math.LO
An ecumenical view of proof-theoretic semantics
本文将逻辑普世主义与证明论语义学相结合，构建了一个经典逻辑与直觉主义逻辑及其证明概念能够共存的统一框架，为解决两者的哲学争议提供了新视角。
2025-04-03 cs.LO math.LO
Set-Theoretic Completeness for Epistemic and Conditional Logic
在哲学和数学文献中，逻辑的标准方法是定义一种语言，这种方法也被计算机科学所采用（语法），一个适当的模型类以及语言中公式的解释（语义学），公理和推理规则的集合，表征推理（证明理论），然后通过可靠性和完整性结果将证明理论与语义联系起来。在这里，我们考虑一种在经济学文献中更常见的方法，它纯粹在语义，集合论层面上工作。我们提供了一些认知和条件逻辑的集合论完备性结果，并对比了句法和集合论方法的表达能力
2000-05-30 cs.AI cs.LO
Bilateral base-extension semantics
本文提出基扩展语义的双边版本，通过在原子基中同时引入原子证明规则与原子反驳规则，证明了其相对于双边对偶直觉主义逻辑2Int的可靠性与完备性，并借此定义对偶性概念以证明双边语义和谐结果。
2025-05-02 cs.LO math.LO
What are acceptable reductions? Perspectives from proof-theoretic semantics and type theory
本文探讨可接受的归约对证明同一性与证明内容有意义性的决定性作用，指出某些归约会使推导失去意义，并提出归约可接受的最低标准。
2023-10-24 cs.LO math.LO
Proceedings 6th Workshop on Logical and Semantic Frameworks with Applications
本卷包含第六届逻辑和语义框架与应用研讨会（LSFA 2011）的会议记录。研讨会将于2011年8月27日在贝洛奥里藏特举行。逻辑和语义框架是用于表示逻辑、语言和系统的形式语言。这些框架为系统和程序设计语言的正式规范提供了基础，支持工具开发和推理。这个为期一天的研讨会的目的是将理论家和实践者聚集在一起，从理论方面推广新技术和成果，并从实践方面对这些技术和成果的实施和使用进行反馈。
2012-03-24 cs.CC cs.LO cs.PL
Definite Formulae, Negation-as-Failure, and the Base-extension Semantics of Intuitionistic Propositional Logic
证明理论语义学（Proof-theoretical Semantics，P-tS）是一种语义学范式，其中逻辑中的意义基于证明（而不是真理）。直觉命题逻辑（IPL）的P-tS的一个特殊实例是它的基扩展语义（B-eS）。这种语义由一个称为支持的关系给出，解释逻辑常数的含义，它由称为基础的规则系统参数化，提供原子命题的语义。在本文中，我们解释的基础上收集的明确的公式，并使用统一的证明搜索-逻辑编程（LP）的证明理论的基础-提供后者的操作视图-建立完整的IPL的B-eS。这种观点允许否定，P-tS中的一个微妙的问题，被理解为在LP中的否定失败协议。具体地说，虽然对命题的否定在传统上被理解为对命题否定的断言，但在B-eS中，我们可以将对命题的否定理解为未能找到对命题的证明，这样，断言和否定都是P-tS中的基本概念。
2023-03-28 cs.LO math.LO
Proceedings of the 19th International Workshop on Logical and Semantic Frameworks, with Applications
本文介绍第19届LSFA会议论文集，该会议于2024年在巴西戈亚尼亚召开，旨在汇聚理论与实务界，推动逻辑与语义框架在证明论、重写系统、自动推理和并发理论等领域的新技术与应用。
2025-06-05 cs.LO cs.SC
Alternating (In)Dependence-Friendly Logic
针对 IF 逻辑的参与者不对称、非确定及排中律失效问题，本文提出 ADIF，并给出组合、Herbrand-Skolem 与博弈论语义，证明其确定性、排中律及二阶逻辑表达力。
2023-04-23 cs.LO math.LO
