Proof-Theoretic Functional Completeness for the Connexive Logic C
本文通过纯证明论方法，在双边主义框架下结合相干推理理解，证明了逻辑C联结词的功能完备性。
2025-07-09 cs.LO math.LO
First-order answer set programming as constructive proof search
我们提出了一个解释的一阶答案集编程（FOASP）的直觉证明理论。它是通过FOASP和一阶直觉逻辑中Mints层次的Sigma_1层的有界元片段之间的两个多项式变换而得到的。因此，使用固定元谓词（特别是一元谓词）的Sigma_1公式与FOASP具有相同的强度。我们的构造揭示了构造性可证明性和稳定蕴涵之间的密切相似性，或者等价地，答案集的构造和直觉反驳之间的相似性。这篇论文正在考虑发表在《逻辑程序设计理论与实践》上
2018-04-30 cs.LO
Virtual Evidence: A Constructive Semantics for Classical Logics
本文提出了一个计算语义的经典逻辑使用建设性类型论。这样的语义似乎是不可能的，因为经典逻辑允许排中律（LEM），而在构造性逻辑中不被接受，因为它没有计算意义。然而，在逻辑推理模型中所表达的明显的神谕力量，即对于任何命题P，要么它是真的，要么它的否定是真的，而不是P，也可以用不涉及“真理的神谕”的构造性证据来解释。具有虚拟证据和否定证据的构造性不可能性的类型为经典真理提供了足够的语义基础，并且具有简单的计算意义。这个想法是使用精化类型形式化的，精化类型是自1984年以来使用的构造性类型论的概念，在这里解释。一个新的公理创建虚拟证据，充分保留了经典语境中的逻辑算子的建设性意义。关键词：经典逻辑，构造性逻辑，直觉主义逻辑，命题类型，构造性类型论，精化类型，双重否定翻译，计算内容，虚拟证据
2014-08-31 cs.LO
A Non-Binary Method for Finding Interpolants: Theory and Practice
Institute of Philosophy（哲学研究所）；Jagiellonian University（雅盖隆大学）；The University of Zielona Góra（热舒夫绿山大学）
本文提出一种基于非二进制推理系统的插值函数寻找方法，展示了其在形式系统分析中的应用与优势。
2026-03-16 cs.LO
Splitting Proofs for Interpolation
研究了局部一阶反驳的插值抽取问题。在将公式的逻辑强度条件与公共签名要求明确分离的基础上，提出了一种新的插值理论观点。这使我们能够突出所有插值的空间，可以从一个反驳作为一个简单的选择空间，如何分裂的反驳成两个部分提取。我们使用这种新的见解，开发一种算法，用于提取插值是线性的输入反驳的大小，可以进一步优化使用的度量，如非逻辑符号或量词的数量。我们在一阶定理证明器VAMPIRE中实现了新算法，并在来自一阶证明社区的大量示例上对其进行了评估。我们的实验给出了实际的证据，我们的工作提高了国家的最先进的一阶插值。
2017-11-07 cs.LO
Intuitionistic PUC-Logic for Constructive Counterfactuals
我们提出了直观版本的PUC-Logic。在此之后，我们提出了一个建设性的方法来刘易斯的反事实抽象，以表明它不需要经典的荒谬规则。
2014-05-21 cs.LO
On Nested Sequents for Constructive Modal Logics
我们提出了各种模态逻辑的演绎系统，这些模态逻辑可以通过添加公理d，t，b，4和5的组合从正常模态逻辑CK的构造性变体中获得。这包括标准模态逻辑K4、S4和S5的构造变体。我们使用我们的演示形式主义的嵌套序列，并给出一个句法证明削减消除。
2015-09-02 cs.LO
A constructive proof of Skolem theorem for constructive logic
本文针对构造逻辑，证明了一阶构造性自然演绎中矢列可证时引入新函数符号可构成保守扩展，从而给出 Skolem 定理的构造性证明。
2023-05-17 cs.LO
Minimal modal logics, constructive modal logics and their relations
提出一族对应经典模态逻辑的极小模态逻辑，通过两种独立但等价的方法定义，并揭示其与构造性模态逻辑CK的紧密关系，进而衍生出一族构造性模态逻辑。
2023-09-05 cs.LO
Meaning and identity of proofs in a bilateralist setting: A two-sorted typed lambda-calculus for proofs and refutations
本文为Wansing双直觉主义逻辑2Int构建双类类型化λ演算λ-2Int，建立带项标注的证明系统并证明对偶化定理，从而从双边主义视角探讨证明的意义、指称与同一性问题。
2024-02-23 cs.LO math.LO
A Constructive Epistemic Logic with Public Announcement (Non-Predetermined Possibilities)
我们认为，建构主义（直觉主义）中的认知\emph{possible worlds}的概念是不一样的，它是在经典的观点，并有可能性，所谓的非预定世界，这是被忽视的（经典）认知逻辑。对于非预定的可能性，我们提出了一个构造性的认知逻辑，证明了它的可靠性和完备性定理，并通过增加一个公共宣告算子对所提出的逻辑进行了扩展。为了说明我们工作的重要性，我们通过所提出的建构性认知逻辑，构造了著名的惊奇考试悖论$\mathbf{SEP}$，并提出了解决该悖论的方法。我们澄清，在$\mathbf{SEP}$的困惑是因为学生的（错误）假设，考试的日子一定是预先确定的。
2013-02-05 cs.LO
Bilateral base-extension semantics
本文提出基扩展语义的双边版本，通过在原子基中同时引入原子证明规则与原子反驳规则，证明了其相对于双边对偶直觉主义逻辑2Int的可靠性与完备性，并借此定义对偶性概念以证明双边语义和谐结果。
2025-05-02 cs.LO math.LO
Canonicity of Proofs in Constructive Modal Logic
本文针对构造性模态逻辑中lambda演算与获胜策略间的证明等价性差距，通过扩充归约规则定义了新lambda演算，证明其规范化与合流性，并利用聚焦证明系统风格的类型系统建立了范式项与获胜策略间的一一对应关系。
2023-07-30 cs.LO
On Natural Deduction for Herbrand Constructive Logics I: Curry-Howard Correspondence for Dummett's Logic LC
达米特逻辑LC是用达米特公理扩展的直觉主义逻辑：对于每两个陈述，第一个蕴涵第二个或第二个蕴涵第一个。本文给出了一阶和二阶Dummett逻辑的一个自然演绎和Curry-Howard对应。我们添加到λ演算的运营商表示，从编程的角度来看，一种机制，用于表示并行计算和它们之间的通信，并从逻辑的角度来看，达米特的公理。我们证明了我们的类型演算是正常化，并表明存在量化公式的证明条款减少到一个单独的条款形成一个Herbrand析取的列表。
2016-09-27 cs.LO
Paraconsistent Constructive Modal Logic
该研究提出构造模态逻辑CK的次协调对应逻辑族，基于带双赋值的直觉主义框架定义语义，提供希尔伯特式公理化与模块化无切割矢列演算，用于形式化矛盾但非平凡命题态度的推理并证明可判定性。
2025-08-25 cs.LO
A Graph Calculus for Predicate Logic
我们介绍了一个反驳图演算经典的一阶谓词逻辑，这是以前的二元关系的扩展。一个简化的逻辑后果，建立一个构造的图有空的扩展，即。e.它代表底部。我们的演算通过将图转换为范式来确定图具有空扩展，该范式被扩展到其他图，直到我们可以识别冲突的情况（等价于公式及其否定）。
2013-03-29 cs.LO
Optimal Tableaux Method for Constructive Satisfiability Testing and Model Synthesis in the Alternating-time Temporal Logic ATL+
我们开发了一个健全的，完整的，实际上可实现的基于表格的决策方法建设性的可满足性测试和模型合成的片段ATL+的完整交替时间时序逻辑ATL*。该方法扩展了一个基本的方式以前开发的基于表格的ATL的决策方法和工程在2EXPTIME，这是最佳的最坏情况下的可满足性问题的ATL+的复杂性。我们还讨论了如何适当的参数化和语法限制输入ATL+公式类可以降低可满足性问题的复杂性。
2015-05-27 cs.LO
LogicProof: An Interactive Web-Based Educational Theorem Prover for Natural Deduction and Sequent Calculus across Classical and Constructive Logics
Technical University of Košice（科希策理工大学）
介绍LogicProof这一用于教育的交互式网络定理证明器，支持经典和构造性逻辑的自然演绎与相继式演算，经学生测试能提升对形式证明构建的理解，补充现有教学方法。
2026-07-07 cs.LO
Constructive Hybrid Games
混合游戏是结合离散、连续和对抗动态的模型。博弈逻辑能够证明（经典的）获胜策略的存在性。我们引入建设性微分博弈逻辑（CdGL）的混合游戏，证明一个球员可以赢得比赛对应的可计算的获胜策略。这是正确的控制和监控代码的安全关键的网络物理系统的合成的逻辑基础。我们的贡献包括新的静态和动态语义以及健全性和一致性。
2020-02-06 cs.LO
Classical Mathematics for a Constructive World
基于依赖类型论的交互式定理证明器具有支持构造性推理和经典推理的灵活性。构造性推理由依赖类型论原生地支持，而经典推理通常通过添加额外的非构造性公理来支持。然而，还有另一种观点认为，构造性逻辑是经典逻辑的延伸。本文将说明如何经典的推理可以支持在一个实用的方式内依赖类型论没有额外的公理。我们将看到几个经典结果如何应用于构造性数学的例子。最后，我们将看到如何通过使用弱值单子来表示经典函数空间，将这种观点从逻辑扩展到数学。
2010-12-12 cs.LO
Some constructive variants of S4 with the finite model property
逻辑CS4和IS 4是模态逻辑S4的直觉变体。有限模型属性是否适用于这些逻辑中的每一个一直是一个长期存在的开放问题。在本文中，我们介绍了两个逻辑密切相关的IS 4：GS 4，通过增加哥德尔-达米特公理到IS 4，和S4 I，通过颠倒的角色模态和直觉关系。然后证明了CS4、GS4和S4 I都具有有限模型性质。
2021-04-30 cs.LO
A Constructive Equivalence between Computation Tree Logic and Failure Trace Testing
形式化验证的两个主要系统是模型检验和基于代数模型的测试。模型检验基于某种形式的时态逻辑，例如线性时态逻辑（LTL）或计算树逻辑（CTL）。CTL是一种强大而现实的逻辑，它能够表达进程的最有趣的属性，如活性和安全性。基于模型的测试基于进程的某些操作语义（例如跟踪、故障或两者）及其关联的前序。除了互模拟之外，最细粒度的前序（主要是理论上的重要性）是基于故障跟踪的。我们表明，这两个最强大的变种是等价的，也就是说，我们表明，对于任何故障跟踪测试存在一个CTL公式相当于它，反之亦然。我们所有的证明都是构造性的和算法性的。我们的结果允许一个大系统的部分被指定为逻辑，而其他部分被指定为代数，从而结合了最好的两个（逻辑和代数）的世界。
2019-01-30 cs.LO
Constructive Provability Logic
我们提出了建设性的可证明性逻辑，一个直观的模态逻辑，通过允许逻辑反射可证明性来验证哥德尔和Löb的可证明性逻辑的Löb规则。这种逻辑的两个不同的变体，CPL和CPL*，在自然演绎和微积分的形式，然后被证明是等价的。此外，我们讨论了使用建设性的可证明性逻辑来证明分层否定逻辑编程中的直觉和结构证明理论。
2012-05-29 cs.LO cs.PL
Interpolation in Classical Propositional Logic
Vrije Universiteit Amsterdam（阿姆斯特丹自由大学）；University of Potsdam（波茨坦大学）；University of Liverpool（利物浦大学）
研究经典命题逻辑中的插值法等相关概念，提出通过量词消去等四种方法计算插值，最后探讨了插值规模与电路复杂性的关系。
2026-07-08 cs.LO
Collapsing Constructive and Intuitionistic Modal Logics
本文证明模态逻辑KB的构造性与直觉主义变体等价，与Das和Marin关于K的变体不等价的结果形成对比。
2024-10-01 cs.LO math.LO
Wijesekera-style constructive modal logics
我们定义了一个命题构造性模态逻辑族，每个模态逻辑对应于一个不同的经典模态系统。逻辑定义在风格的Wijesekera的建设性模态逻辑，并证明理论和语义动机。一方面，它们对应于经典模态逻辑的标准演算的单一后继限制。另一方面，它们是通过将直觉Kripke模型的遗传性纳入模态公式的经典满足子句而获得的。我们表明，对于所考虑的经典逻辑，证明理论和语义方法返回相同的建设性系统。
2022-10-18 cs.LO math.LO
On Natural Deduction for Herbrand Constructive Logics III: The Strange Case of the Intuitionistic Logic of Constant Domains
常域逻辑是直觉主义逻辑，它用所谓的全移位公理（forall-shift axiom）进行了扩展，这是一个经典有效的命题，蕴涵了可判定公式上的排中律。令人惊讶的是，这种逻辑是建设性的，到目前为止，这已经证明了削减消除特设的结石。在这里，我们使用自然演绎和Curry-Howard对应的方法来提供一个简单的计算解释的逻辑。
2018-10-18 cs.LO math.LO
Lewis meets Brouwer: constructive strict implication
C. I.刘易斯发明了现代模态逻辑作为“严格蕴涵”的理论。在经典的命题演算中，人们也可以使用一元盒连接词。然而，从直觉上看，严格含义比盒子具有更强的表达能力，并且允许在普通语法中看不到区别。特别地，由直觉K的最流行的语义所确定的逻辑成为二元连接词的最小正规逻辑的适当扩展。即使是这种最小逻辑的扩展与“强度”公理，经典的近平凡，保持二进制和一元设置之间的区别。事实上，函数式编程社区在研究“arrows”与“idioms”的对比时，也发现了这种区别和强构造性严格含义本身。我们特别关注的是算术解释的直觉严格蕴涵在扩展的Heyting的算术。
2017-10-29 cs.LO
Duality for Constructive Modal Logics: from Sahqlvist to Goldblatt-Thomason
Mathematical Institute, University of Bern（伯尔尼大学数学研究所）；School of Computer Science, University of Birimingham（伯明翰大学计算机学院）；School of Computing, The Australian National University（澳大利亚国立大学计算学院）
本文研究了构造模态逻辑CK的语义学，建立代数与双关系语义的对偶性，并由此证明了萨尔奎维斯特类型的对应性和完备性结果，以及戈德布拉特-托马森类型的框架类可定义性定理。
2026-04-13 cs.LO math.LO
Refining Constructive Hybrid Games
我们扩展了建设性的微分博弈逻辑（CdGL）的混合游戏与细化连接，涉及两个混合游戏。我们使用这个连接证明一个民间定理有关的混合游戏混合系统。
2020-02-13 cs.LO
On the definition of the classical connectives and quantifiers
经典逻辑是嵌入到构造性逻辑，通过定义的经典连接词和量词的建设性的。
2016-01-08 cs.LO
On Natural Deduction for Herbrand Constructive Logics II: Curry-Howard Correspondence for Markov's Principle in First-Order Logic and Arithmetic
直觉主义一阶逻辑用马尔可夫原理的一个限制形式扩展是构造性的，并承认Curry-Howard对应，如Herbelin所示。我们提供了一个更简单的证明结果，然后我们研究直觉一阶逻辑扩展的无限制马尔可夫原理。从经典自然演绎出发，对排中律进行了限制，得到了一个自然演绎系统和一个平行的Curry-Howard同构。我们证明存在量化公式的证明项减少到代表所有可能证人的单个项的列表。作为推论，我们得出该逻辑是Herbrand构造性的：每当它证明任何存在公式时，它也证明该公式的Herbrand析取。最后，使用刚刚介绍的技术，我们还提供了一个新的计算解释的算术与马尔可夫的原则。
2017-10-17 cs.LO math.LO
Constructive Game Logic
游戏逻辑是一个很好的环境，通过将这些证明解释为程序来研究关于程序的证明，因为游戏的建设性证明对应于有效的获胜策略，以响应对手的行动。因此，我们开发的建设性的游戏逻辑扩展Parikh的游戏逻辑（GL）与建设性和一阶程序一个la普拉特的一阶动态逻辑（DL）。我们的主要贡献包括：1）一种新颖的可实现性语义，捕捉游戏的对抗动态，2）自然演绎演算和操作语义，通过证明术语描述策略的计算意义，以及3）理论结果，包括证明演算的合理性wrt可实现性语义、证明的操作语义的进展和保持、以及支持从游戏证明中提取计算工件的存在性属性。总之，这些结果提供了迄今为止任何程序逻辑的Curry-Howard解释的最一般的帐户，并且是游戏逻辑的第一个。
2020-07-22 cs.LO cs.PL
Internalising modified realisability in constructive type theory
一个修改后的可实现性解释的无穷逻辑形式化，并证明了健全的建设性类型理论（CTT）。所考虑的逻辑包括一阶逻辑。这种解释使得提取具有简化类型的程序并在CTT中对其进行合并和推理成为可能。
2005-10-05 cs.LO math.LO
A Proof-Theoretic View of Basic Intuitionistic Conditional Logic (Extended Version)
本文从证明论角度研究基本直觉主义条件逻辑，为IntCK引入嵌套演算、为CCKbox引入矢列演算，并在此基础上定义带might算子的保守扩张CCK，给出其模型类、公理化及若干扩张结果。
2025-07-03 cs.LO
A Constructive Proof of Cut Elimination for a System of Full Second Order Logic
本文给出了一个完全二阶逻辑系统的割消的构造性证明，它吸收了结构规则，用集合代替序列。通过使用一个新的诱导参数，cutrank增长的标准问题是避免。这种技术也可以应用于一阶逻辑。
2016-06-21 cs.LO math.LO
Church's thesis and related axioms in Coq's type theory
“Church's thesis”（$\mathsf{CT}$）作为构造性逻辑中的一个公理指出，每个$\mathbb{N} \to \mathbb{N}$类型的全函数都是可计算的，即在计算模型中是可定义的。$\mathsf{CT}$在经典数学和布劳威尔的直觉主义中都是不一致的，因为它分别与弱柯尼希引理和扇形定理相矛盾。最近，$\mathsf{CT}$被证明是一致的（单价）建设性类型论。由于弱柯尼希引理和扇形定理都不是构造性逻辑中假设的逻辑公理或选择类公理的结果，所以$\mathsf{CT}$似乎只与经典逻辑和选择公理的组合不一致。我们研究的后果$\mathsf{CT}$和它的关系，几类公理在Coq的类型论，建设性的类型论与宇宙的命题，既不证明经典的逻辑公理，也不强选择公理。因此，我们对以下问题提供了部分答案：哪些公理可以保留类型论固有的计算直觉，哪些公理肯定不能。该文件也可以阅读作为一个广泛的调查公理在类型论，所有结果机械化的Coq证明助手。
2020-11-03 cs.LO
The Many Worlds of Modal λ-calculi: I. Curry-Howard for Necessity, Possibility and Time
这是一个关于λ演算的综述，通过Curry-Howard同构，对应于构造模态逻辑。我们涵盖了这个主题的史前史，然后集中在20世纪90年代和21世纪初发生的发展。我们讨论逻辑方面，模态λ演算，和它们的范畴语义。所调查的演算背后的逻辑是K、K4、S4和LTL的构造性版本。
2016-05-26 cs.LO
Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic<br> Semantics
丘奇的高阶逻辑是有影响的证明助手-- HOL和PVS的基础。Church的逻辑有一个简单的集合论语义，使其可信和可扩展。我们因素HOL到一个建设性的核心加上公理的排中律和选择。我们同样的因素标准集理论，ZFC，到一个建设性的核心，IZF，公理排除中间和选择。然后，我们提供了标准的集合论语义，这样的方式，建设性的核心HOL映射到IZF。我们使用的析取，数值存在性和长期存在的IZF属性提供了一个程序提取能力，从证明建设性的核心。我们可以用两种不同的方式实现析取和数值存在性：一种是使用Rathjen对IZF的可实现性，另一种是使用Moczydlowski对IZF的一个新的直接弱归一化结果。后者也可以用于术语存在属性。
2008-09-09 cs.LO
Completeness Theorems for First-Order Logic Analysed in Constructive Type Theory (Extended Version)
我们研究各种配方的完整性一阶逻辑措辞建设性类型论和机械化的Coq证明助手。具体而言，我们研究的经典和直觉主义的自然演绎和微积分的变种模型论，代数和博弈论语义的完整性。作为完整性方面的标准模型理论语义的塔斯基和Kripke是不容易建设性的，我们分析连接的完整性定理，马尔可夫原理和弱柯尼希引理，并讨论非标准的语义承认无故障的完整性。我们贡献了一个可重用的Coq库一阶逻辑包含本文所涉及的所有结果。
2021-12-14 cs.LO math.LO
Conditionals and Modalities in Constructive Quantum Logics
TU Wien（维也纳工业大学）；Chapman University（查普曼大学）
研究推广直觉主义逻辑和量子逻辑的逻辑系统，提出iEx-逻辑作为直觉主义逻辑与带有Sasaki钩的orthomodular逻辑的交集，并刻画其扩展格。
2026-07-01 cs.LO math.LO
Constructive Modalities with Provability Smack
我概述了第比利斯学校的直觉模态逻辑的良好的基础/分散的结构和它与当代理论计算机科学的连接的工作。不动点定理及其推论特别有趣。
2017-08-18 cs.LO
Uniform interpolation with constructive diamond
University of Amsterdam（阿姆斯特丹大学）；University of Birmingham（伯明翰大学）；University of Melbourne（墨尔本大学）
本文通过构造性方法证明构造性K（CK）和Wijesekera的K（WK）具有均匀插值性质，填补了直觉主义模态逻辑中独立box和diamond算子均匀插值研究的空白。
2026-05-27 cs.LO math.LO
Logics and Type Theory: essays dedicated to Stefano Berardi on the occasion of his 1000000th birthday
本文集纪念斯蒂芬诺·贝拉迪100万岁生日，汇集了研究者在构造逻辑、依赖类型和循环证明等领域的最新研究成果。
2026-03-03 cs.LO
TryLogic tutorial: an approach to Learning Logic by proving and refuting
为了给证明论教学提供一个混合式学习的框架，本文描述了一个交互式教程，称为\textsc{TryLogic}，教授如何通过证明或反驳来解决逻辑问题。本文还介绍了我们的基础设施与虚拟学习环境\texttt{Moodle}通过IMS学习工具互操作性规范的集成，并评估我们已经开发的工具。
2015-07-14 cs.CY cs.LO
Towards a Denotational Semantics for Proofs in Constructive Modal Logic
本文给出了构造模态逻辑CK和CD中证明的两种新语义。第一个语义是通过扩展命题直觉逻辑的组合证明的语法给出的，其中证明被分解为线性片段（竞技场网）和并行的弱化收缩片段（斜纤维化）。特别是，我们提供了一个编码的模态公式通过有向图（模态竞技场），和一个编码的线性证明作为模态竞技场配备满足拓扑标准的顶点分区。第二个语义是通过赢得无辜的策略，两个球员的游戏模式舞台。这是通过在Hyland-Ong竞技场中扩展直觉组合证明和获胜无辜策略之间的Heijltjes-Hughes-Straßburger对应关系给出的。使用我们的第一个结果，我们提供了一个表征的获胜策略的游戏模式舞台上对应的模态证明。
2021-04-19 cs.LO math.LO
Universal Proof Theory: Feasible Admissibility in Intuitionistic Modal Logics
在本文中，我们介绍了一个一般家庭的序列式演算的模态语言及其片段，以捕捉所有建设性的可接受的系统的本质。称这些演算为\emph{constructive}，我们表明，任何足够强的建设性的微积分，满足一个温和的技术条件，可行地承认所有的Visser规则，即，有一种多项式时间算法，它读取维塞尔规则的前提的证明，并为其结论提供证明。作为一个积极的应用，我们证明了Visser规则在直觉模态逻辑的几个演算中的可行容许性，这些演算包括$\mathsf{CK}$，$\mathsf{IK}$及其由模态公理$T$，$B$，$4$，$5$，有界宽度和深度的模态公理以及命题逻辑的扩展。在消极的一面，我们表明，如果一个足够强大的直觉模态逻辑（满足一个温和的技术条件）不承认至少一个Visser的规则，那么它不能有一个建设性的逻辑演算。因此，除了$\mathsf{IPC}$之外，没有中间逻辑具有构造性的构造演算。
2022-10-16 cs.LO math.LO
Constructive Quantum Logics
本研究联合探究量子逻辑与直觉主义逻辑，提出线性时间翻译方法构造二者交的公理系统，证明超Ex逻辑格同构于两类逻辑格的乘积，且存在无穷多扩展Holliday基础逻辑的次Ex逻辑，解决了相关公开问题。
2025-03-19 cs.LO math.LO
A Note on Semantic Web Services Specification and Composition in Constructive Description Logics
Università degli Studi dell’Insubria（因苏布里亚大学）
语义Web的思想是用计算机可解释的描述来注释Web内容和服务，目的是使目前由人类用户执行的许多任务自动化。在Web服务的上下文中，最有趣的任务之一是它们的组合。在本文中，我们正式这个问题的框架内的建设性描述逻辑。特别是，我们提出了一个声明性的服务规约语言和演算的服务组合。我们通过一个例子表明如何使用这种演算来定义组合Web服务，我们讨论了自动服务合成的问题。
2010-07-14 cs.AI cs.LO
The Complexity of the Constructive Master Modality
本文提出了两种构造性主模态逻辑，并证明其复杂性为 EXPTIME，同时解决了相关逻辑的有效性问题
2026-07-22 cs.LO math.LO
A logical basis for constructive systems
这项工作致力于可计算性逻辑（CoL）-哲学/数学平台和长期项目，用于在其底层语义中用可计算性取代真理之后重新开发经典逻辑（见http：//www.cis.upenn.edu/paggiorgi/cl.html）。本文阐述了CoL框架的一些基本复杂性理论。然后证明了演绎系统CL 12关于CoL语义的可靠性和完备性，包括后者基于多项式时间可计算性而不是原则上可计算性的版本。CL 12是一个微积分系统，其中一个变量的含义直观上可以被描述为“后继变量可以在算法上还原为先行变量”，并且其中公式是由谓词字母、函数字母、变量、常数、恒等式、否定式、平行和选择连接词以及盲量词和选择量词构建的。一个案例是CL 12是一个足够的逻辑基础建设性的应用理论，包括复杂性导向的。
2011-03-14 cs.CC cs.LO math.LO
Constructive S4 modal logics with the finite birelational frame property
IRIT, Toulouse University（图卢兹大学 IRIT）；LERIA, University of Angers（昂热大学 LERIA）；Department of Philosophy, University of Barcelona（巴塞罗那大学哲学系）；Department of Mathematics, Ghent University（根特大学数学系）
本文证明了直觉主义模态逻辑CS4具有有限框架性质，并研究了与IS4相关的GS4、GS4^c和S4I逻辑，为它们建立了有限双关系框架性质，从而证明了可判定性，并给出了NEXPTIME上界。
2026-06-23 cs.LO
Game semantics for the constructive $μ$-calculus
本文为构造性$μ$-演算提出博弈语义，证明其与双关系语义等价，并借此证明$μ$-演算在$\mathsf{IS5}$上坍缩为模态逻辑，同时给出扩展不动点算子的$\mathsf{IS5}$完备性。
2024-10-01 cs.LO math.LO
The Constructive $μ$-calculus: Game Semantics and Non-Wellfounded Proof Systems
Institute of Sciece Tokyo, Japan（东京科学研究所）
本文研究基于构造模态逻辑CK的μ-演算变种，定义了游戏语义并证明其等价于双关系李普克内语义，进而利用游戏语义证明了完全标记的非良基证明系统的正确性与完备性，并探讨如何将其扩展到其他非经典模态逻辑的μ-演算。
2026-04-25 cs.LO math.LO
