Using Modes to Ensure Subject Reduction for Typed Logic Programs with Subtyping
我们考虑了逻辑程序的一个具有参数多态性和子类型的一般规定类型系统。主语归约的性质表达了类型系统相对于主系统的一致性。执行模型：如果一个程序是“良好类型的”，那么所有从“良好类型的”目标开始的派生都是“良好类型的”。众所周知，对于逻辑程序，如果没有子类型，这个性质很容易获得。他们的标准（非类型化）执行模型。在这里，我们给出的句法条件，确保主题减少，也在一般的子类型之间的关系类型构造。其思想是考虑具有由模式给出的固定的逻辑流的逻辑程序。
2001-01-18 cs.LO
On a Dependently Typed Encoding of Matching Logic
本文提出匹配μ-逻辑的首个依值类型定义，通过类型索引编码排序上下文确保良排序性，使不良排序语法不可表示且良排序元素语义保证在关联排序域内。
2025-09-16 cs.LO
Circular Proofs as Session-Typed Processes: A Local Validity Condition
本文扩展了直觉主义线性逻辑与会话类型π演算的对应关系到带最小和最大不动点的子结构逻辑片段，提出一个局部且可判定的有效性准则来识别对应有效循环证明的互递归进程，并证明该准则比既有守护条件更严格但更适合作编程语言基础。
2022-05-09 cs.LO cs.PL
Value Coalition Logic: A Typed Assignment-Based Reconstruction of Coalition Logic
School of Computer and Information Engineering (School of Artificial Intelligence), Henan Normal University（河南师范大学计算机与信息工程学院（人工智能学院））
本文提出价值联盟逻辑，通过类型化变量赋值重构经典联盟逻辑，在保持策略语义不变的同时，在原子层面引入值域完备性与互斥性，并证明与命题联盟逻辑在有限类型签名下真值等价，从而揭示值级不变量。
2026-05-25 cs.LO
Well-Typed Logic Programs Are not Wrong
我们考虑逻辑程序的规定类型系统（如Goedel或Mercury）。在这样的系统中，类型是静态的，但它保证了一个操作属性：如果一个程序是“良好类型的”，那么所有在“良好类型的”查询中开始的派生都是“良好类型的”。这个特性被称为主体还原。我们表明，这个属性也可以被措辞为一个属性的证明理论的语义的逻辑程序，从而抽象通常的操作（自上而下）的语义。这种证明论的观点使我们质疑一个条件，这通常被认为是必要的主题还原，即头部条件。它声明每个子句的头部必须有一个类型，该类型是声明类型的变体（而不是正确的实例）。我们提供了一个更一般的条件，从而在头原子和体原子之间重新建立了某种对称性。这个条件确保在一个推导中，两个统一项的类型本身是可统一的。我们讨论了这一结果的可能影响。我们还讨论了头条件和多态递归之间的关系，这是函数式编程中的一个已知概念。
2001-01-18 cs.LO
A Meta-Programming Approach to Realizing Dependently Typed Logic Programming
依赖类型的lambda演算（如逻辑框架（LF））可以编码类型中术语之间的关系，并且可以自然地捕获公式及其证明之间的对应关系。这样的演算也可以给出一个逻辑编程的解释：LLF系统就是基于这样一个LF的解释。我们在这里考虑是否一个传统的逻辑程序设计语言可以提供一个类似的系统编码类型和证明和公式依赖的好处。特别是，我们提出了一个简单的映射从LF规范的一组公式在高阶遗传Harrop（hohh）语言，涉及推导和证明搜索之间的两个框架。然后，我们表明，这种编码可以通过利用知识的原始LF规范的良好形式，以消除大量冗余的类型检查信息。所得到的逻辑程序具有与原始规范非常相似的结构，从而允许将LF规范视为hohh元程序。使用Teyjus实现的PrologaProlog，我们表明，我们的翻译提供了一个有效的手段执行LF规范，补充的能力，PrologaProlog系统提供的推理。
2010-05-24 cs.LO
Strong Progress for Session-Typed Processes in a Linear Metalogic with Circular Proofs
引入了一个具有最小和最大不动点的无穷大一阶线性逻辑。为了确保切割消除，我们施加了一个有效性条件的无限导子。我们的演算的目的是相互定义的归纳和共归纳线性谓词的丰富签名的原因。在一个主要的案例研究中，我们用它来证明强的二进制会话类型的进程下的异步通信语义的进展属性。据我们所知，这是这个性质的第一个证明。
2021-03-07 cs.LO cs.PL
Random generation of closed simply-typed $λ$-terms: a synergy between logic programming and Boltzmann samplers
软件质量保证的一种自然方法是编写单元测试，以保护程序员声明的代码不变量。在整个文献中，大量的工作都致力于使这一劳动密集型过程自动化的工具和技术。一个突出的例子是随机性的成功使用，特别是随机类型的$λ$ -terms，在测试函数式编程编译器，如格拉斯哥Haskell编译器。不幸的是，由于固有的困难的组合结构的类型$λ$ -条款没有有效的均匀抽样方法是已知的，设置它作为一个基本的开放问题，在随机软件测试方法。在本文中，我们结合了玻尔兹曼采样器，一个强大的随机组合结构生成技术的框架，与今天的Prolog系统提供逻辑变量之间的协同作用，统一与发生检查和有效的回溯。这使我们能够开发一种新的采样机制，能够构建均匀随机封闭的简单类型的$λ$ -项的大小为120。我们应用我们的技术来产生均匀随机封闭的简单类型的范式和设计一个并行执行机制，推动可实现的长期规模为140。逻辑程序设计理论与实践（TPLP）
2017-09-13 cs.LO
Translating Specifications in a Dependently Typed Lambda Calculus into a Predicate Logic Form
依赖类型的lambda演算（英语：Lambda calculi），如Edinburgh逻辑框架（英语：Edinburgh Logical Framework）（LF），是一种流行的方式，用于编码关于正式语法对象的基于规则的规范。在这些框架中，通过使用类型的依赖结构，自然地捕获了表示形式对象的术语上的关系。我们在这里考虑在简单类型的λ-项上将以这种风格编写的规范保持意义地翻译成谓词逻辑。这样的翻译可以为高效的实现和推理规范的复杂能力提供基础。我们开始与先前描述的翻译LF规范的公式在逻辑的高阶遗传Harrop（hohh）公式。我们展示了如何通过识别和消除其中包含的冗余类型检查信息来改进这种翻译。这既有利于翻译公式的清晰度，又减少了执行过程中必须花费在类型检查上的精力。为了允许这种翻译被用来执行LF规范，我们描述了一个逆变换从hohh项LF表达式，因此可以使用翻译的形式进行计算，然后可以将结果导出回LF。基于LF规范的执行还可能涉及某些形式的类型重构。我们讨论的可能性，支持这样的能力，使用翻译的结构规范的一些合理的限制。
2013-10-31 cs.LO
A Transformational Approach to Resource Analysis with Typed-norms Inference
为了自动推断程序的资源消耗，分析器跟踪数据大小如何随着程序的执行而变化。通常，分析器通过应用范数来测量数据的大小，范数是从数据到表示相应数据大小的自然数的映射。当规范是通过考虑类型信息来定义的，它们被称为类型规范。本文提出了一种转换的方法，资源分析与类型化规范，推断出的数据流分析。该分析是基于一个转换的程序到一个中间的抽象程序，其中每个变量被抽象的所有考虑的规范是有效的，其类型。我们还提出了数据流分析，自动推断所需的，有用的，类型规范的程序。我们的分析是在一个简单的基于规则的表示上形式化的，以不同的编程范式编写的程序（例如，功能性、逻辑性、命令性）可以自动翻译。在其他基于类型的分析器使用的标准基准测试上的实验结果表明，我们的方法在实践中是有效和准确的。逻辑程序设计理论与实践（TPLP）
2019-08-06 cs.LO cs.PL
Dependently Typed Model Composition for Matching Logic
ELTE E\" o tv\" o s Lor\' a nd University Budapest, Hungary
本文针对匹配逻辑框架中的模型组合问题，基于多元多类别匹配逻辑变体提出依赖类型化的组合定义，确保组合保持可满足性证明，可为后续Rocq证明助手的机械化实现提供直接蓝本。
2026-09-28 cs.LO
Light Logics and Optimal Reduction: Completeness and Complexity
初等和轻仿射逻辑中的非线性项的分类（分别为EAL，LAL）已经研究了两个不同的原因：一方面，使用LAL（EAL，resp.）证明网承认一个有保证的多项式（分别是初等的）另一方面，这些术语也可以通过使用Lamping算法的抽象版本的最优约简来评估。第一个约简是全局的，而第二个约简是局部的和异步的。我们证明，对于LAL（EAL，resp.）类型的条款，兰坪的抽象算法也承认一个多项式（小学，分别）。绑定我们还显示了它的健全性和完整性（EAL和LAL类型不动点），通过使用一个简单的几何交互模型（上下文语义）。
2007-04-19 cs.LO cs.PL
Categories with Families: Unityped, Simply Typed, and Dependently Typed
我们展示了无类型的，简单类型的和依赖类型的λ演算的范畴逻辑如何可以围绕具有家族的范畴（cwf）的概念来构造。为此，我们引入简单类型的cwfs（scwfs）的子类别，其中类型不依赖于变量，和unityped cwfs（ucwfs），其中只有一个类型。我们证明了几个等价和双等价定理之间的cwf为基础的概念和基本概念的范畴逻辑，如carniveroperads，Lawvere理论，范畴有限的产品和限制，carniver-closed范畴，局部carniver-closed范畴。这些定理中的一些依赖于上下文（在Cartmell的意义上）或民主（由Clairambault和Dybjer用于他们的双等价定理）的限制。有些定理是严格保持所选结构的概念之间的等价。另一些是概念之间的双等价，其中属性只保留到同构。除此之外，我们还讨论了初始ucwfs，scwfs和具有额外结构的cwfs的各种构造。
2020-07-07 cs.LO
Positive Instantial Neighbourhood logic: Typed Completeness and Admissible-Open Representation
Mahishadal Raj College（马希沙达尔皇家学院）；Jadavpur University（贾达普大学）
本文提出正实例邻域逻辑（PINL），一种无否定的模态逻辑，通过两种实例模态处理邻域中的世界，并基于持久双边邻域模型证明了其完备性，同时引入代数语义和典范位拓扑表示。
2026-07-17 cs.LO
Theorem Proving in Dependently-Typed Higher-Order Logic -- Extended Preprint
FU Berlin（柏林自由大学）；University Erlangen-Nürnberg（埃尔朗根-纽伦堡大学）；University Bamberg（班贝格大学）
本文引入了HOL的依存类型扩展DHOL，保留了HOL的风格与概念框架，并构建从DHOL到HOL的翻译作为HOL定理证明器的前置预处理器，从而实现DHOL的定理证明。
2023-05-24 cs.AI cs.FL cs.LO
Verification of Ptime reducibility for system F terms via Dual Light Affine Logic
在以前的工作中，我们介绍了双轻仿射逻辑（DLAL）（[BaillotTerui04]）作为轻线性逻辑的一个变体，适用于保证复杂性的性质上的微积分条款：所有类型的条款可以评估在多项式时间和所有Ptime函数可以表示。在目前的工作中，我们解决的问题，在二阶DLAL的类型的DLDA项。为此，我们给出了一个过程，从系统F中的一个项开始，找到所有可能的方法将其装饰成DLAL类型的项。我们表明，我们的程序可以运行在时间多项式的大小，原来的教会类型的系统F项。
2006-03-27 cs.LO
Simply-typed constant-domain modal lambda calculus I: distanced beta reduction and combinatory logic
UCLA Department of Philosophy（加州大学洛杉矶分校哲学系）
本文提出结合模态逻辑与简单类型λ演算的参数化系统λ_θ，通过组合逻辑给出其模型刻画，并证明λ_θ与最大系统λ_ω之间的语义守恒与可表达性结果。
2026-07-14 cs.LO math.LO
Analysis of Polymorphically Typed Logic Programs Using ACI-Unification
（部分）根据性分析是抽象解释的一个重要应用。有几个建议通过利用类型信息来提高这种分析的精度，包括我们自己与Hill和King的工作，我们已经展示了如何使用程序类型声明中的信息来以精确但固有有限的方式来确定术语的实例化程度。这种方法适用于像Goedel或HAL那样的多态类型程序。在这里，我们重铸这个方法以下的Codish，泻湖和斯塔基的作品。为了形式化我们想要识别的项的哪些属性，我们使用标签函数，这些函数是沿着某些路径从项中提取子项的函数。一个抽象项收集一个项的所有标签函数的结果。对于分析，程序执行的抽象条款，而不是具体的，通常的统一是取代统一模的平等理论，其中包括著名的ACI理论。因此，我们概括了Codish，Lagoon和Stuckey w.r.t.所考虑的类型系统，并相互关联的作品。
2001-05-04 cs.LO
Experiments with Choice in Dependently-Typed Higher-Order Logic
University of Innsbruck（因斯布鲁克大学）；Czech Technical University in Prague（布拉格捷克理工大学）
本文提出两种将选择机制引入依赖类型高阶逻辑（DHOL）的方法，通过Hilbert选择算子扩展项结构并定义到HOL的翻译，证明了其完备性与可靠性，并在依赖HOL问题上完成评估。
2024-10-11 cs.AI cs.LO
Tableaux for Automated Reasoning in Dependently-Typed Higher-Order Logic (Extended Version)
本文针对依赖类型高阶逻辑DHOL提出原生表推演自动推理规则，并在Lash中实现，借助DHOL到HOL的可靠完备翻译保证完备性，实验表明其性能优于在翻译结果上运行的主流HOL证明器。
2024-10-18 cs.LO
MaudeTypedLog: A Typed Interpreter for Prolog in Maude
Universitat Politècnica de València（瓦伦西亚理工大学）；Faculdade de Ciências da Universidade do Porto（波尔图大学理学院）
研究针对 Prolog 传统无类型的问题，用 Maude 实现类型化合一算法并构建 MaudeTypedLog 解释器，其遵循特定操作语义，能动态检测程序和查询中的类型错误。
2026-07-23 cs.LO
From Linear Logic to Cyclic Sharing
我们提出了一个翻译从乘法指数线性逻辑到一个简单类型的λ演算与循环共享。这个翻译是从对追踪monoidal范畴的int-结构的简单观察中得出的。事实证明，翻译是一个混合的按名称呼叫CPS翻译和几何互动为基础的解释。
2019-04-15 cs.LO cs.PL
Typed realizability for first-order classical analysis
我们描述了经典一阶逻辑的可实现性框架，其中实现者生活在类型λμ演算（模型）中。这允许对经典证明的直接解释，避免了通常对直觉主义逻辑的否定翻译。我们证明了哥德尔系统T的通常项实现了Peano算术公理，并且在计算模型的某些假设下，棒递归算子实现了依赖选择公理.我们还进行了适当的分析，相对化，这使得较少的技术证明的充分性。从2002年公式的证明中提取算法依赖于弗里德曼技巧的一种新的实现，利用语言的控制可能性。这允许具有比在负翻译之后是直观可实现性的情况下更简单的类型的提取程序。
2015-12-30 cs.LO
Lax Modal Lambda Calculi
University of Edinburgh（爱丁堡大学）
本文提出了一种基于Lax逻辑的类型lambda计算，为强functor提供了模态逻辑基础，并通过形式化验证证明了归约和等价完备性等结果。
2025-12-11 cs.LO cs.PL
Uniform Algebras: Models and constructive Completeness for Full, Simply Typed λProlog
本文为λProlog语言基础逻辑HOHH建立模型论，证明消解的可靠性与完备性，并利用最小不动点及Lindenbaum代数变体给出构造性证明，同时提出新的切割消去方法。
2024-05-23 cs.LO cs.PL math.LO
Schematic Polymorphism in the Abella Proof Assistant
Abella交互式定理证明器已被证明是推理关系规范的有效工具。然而，该系统有一个局限性，这是由于它是基于简单类型化逻辑的事实：除了应用于不同类型的形式化之外，其他形式化都是相同的，必须在每个类型上重复。我们开发了一种方法，克服了这一限制，同时保留系统的逻辑基础。在这种方法中，对象构造函数、公式和其他相关的逻辑概念被允许通过类型参数化，解释为它们代表通过实例化类型参数获得的相应构造的（无限）集合。我们考虑的公式的证明结构，以这种方式被模式化的限制，其类型实例是有效的证明在简单类型逻辑。我们开发的示意性证明规则，确保这一属性，一个任务，是复杂的事实，类型信息影响的概念，在逻辑中起着关键作用的统一。我们的想法，这已经实现了系统的更新版本，容纳示意图多态性的核心逻辑Abella和可执行的规范逻辑，它嵌入。
2018-06-20 cs.LO cs.PL
Logic Programming with Extensible Types
Universidad Politecnica de Madrid（马德里理工大学）
本文提出了一种在类型化函数式编程语言中通过可扩展类型、合一算法和领域特定语言实现逻辑编程的方法，展示了其可行性和实用性。
2026-01-07 cs.LO cs.PL
Comparing Deadlock-Free Session Typed Processes
除了遵守规定的协议，以通信为中心的系统永远不应该“卡住”。这个需求已经通过诸如进度或（死）锁自由度之类的活动属性来表达。已经提出了几个类型的纪律，确保这些属性的移动进程。不幸的是，人们对这些规程之间的精确关系以及它们所引发的类型化过程的类知之甚少。本文对两类无死锁的会话型并发进程L和K进行了比较。类L因其规范性而突出：它自然地产生于将线性逻辑命题解释为会话类型。类K，通过将会话类型编码到Kobayashi的使用类型中获得，包括在其他类型系统中不可类型化的进程。我们证明了L严格包含在K中。我们还确定了L和K重合的精确条件。一个关键的观察是，并行进程之间的共享程度决定了类型化进程的新表达层次结构。我们还提供了一个保持类型的重写过程中的进程在K到L。这个过程表明，虽然共享程度是有效的，但它是区分类型化进程的一个相当微妙的标准。
2015-08-27 cs.LO cs.PL
Semi-Automation of Meta-Theoretic Proofs in Beluga
本文提出一种用于Beluga核心逻辑的可靠完备聚焦演算，并实现为Harpoon中的策略，自动完成简单子情形，简化了简单类型λ演算的弱头规范化证明。
2023-11-17 cs.LO cs.PL
Redundancies in Dependently Typed Lambda Calculi and Their Relevance to Proof Search
依赖类型的lambda演算，如逻辑框架（LF），能够通过类型表示术语之间的关系。通过利用“公式作为类型”的概念，这种演算也可以在类型判断中编码公式及其证明之间的对应关系。因此，这些演算提供了一个自然而强大的手段来指定各种形式系统。这样的规范可以被转换成更直接的形式，该形式在简单键入的非线性项上使用谓词公式，从而使用传统的逻辑编程技术为它们的动画提供基础。然而，这种想法的天真使用充满了效率低下的事实，依赖类型的表达式通常包含大量冗余的类型信息。我们研究的句法标准识别，因此，消除这种冗余。特别是，我们确定了LF类型中的绑定变量的属性，称为“刚性”，并正式表明，检查这些变量的实例化遵守类型限制是不必要的，以确保整体表达是良好的。我们将展示如何利用这一属性在一个基于翻译的方法来执行规范的BMPF语言。识别冗余也与设计依赖类型表达式的紧凑表示有关。我们强调我们工作的这一方面，并讨论它与在这方面提出的其他方法的联系。
2010-07-05 cs.LO
Session Types in Abelian Logic
有一个博士生说：“我找到了一双木鞋。我在左边放了一枚硬币，在右边放了一把钥匙。第二天早上，我在另一只鞋里发现了这些东西。“我们并不声称存在这样的鞋子，但在类型化lambda演算的上下文中提出了类似的编程抽象。我们称之为Amida演算的结果推广了Abramsky的线性λ演算LF并刻画了Abel逻辑.
2013-12-10 cs.LO cs.PL
A Bunch of Sessions: A Propositions-as-Sessions Interpretation of Bunched Implications in Channel-Based Concurrency
作为会话的命题（Propositions-as-Sessions）的出现，为消息传递并发奠定了逻辑基础，它是线性逻辑命题与并发进程会话类型之间的Curry-Howard对应。这种方法的核心是由线性逻辑预示的资源消耗范式。在本文中，我们研究了一个新的点，在设计空间的会话类型系统的消息传递并发程序。我们确定O 'Hearn和Pym的逻辑束的影响（BI）作为一个富有成效的基础解释的逻辑作为一个并发程序设计语言。这导致了对非线性资源的处理，这与基于线性逻辑的现有方法完全不同。我们介绍了一个新的$π$ -演算会话，称为$π$ BI，其最显着的特点是一个构造称为产卵，它表达了新的形式的共享，诱导BI的结构原则。我们说明了$π$ BI的表现力，并奠定了其基本理论：类型保存，死锁自由和弱规范化的结果良好的类型化进程;一个操作上健全和完整的仿射$λ$ -演算的类型化编码;和一个非干扰的结果访问资源。
2022-09-12 cs.LO cs.PL
A program logic for fresh name generation
我们给出了Pitts和Stark的ν-演算的程序逻辑，它是按值调用的简单类型λ-演算的扩展，具有生成新名称的机制。可以比较名字是否相等，从而产生具有细微可观察属性的程序。由生成和抽象之间的交互产生的隐藏名称通过类型上下文上的二阶量词逻辑地捕获。我们说明使用的逻辑推理著名的困难的情况下，从文献。
2021-03-12 cs.LO cs.PL
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
On Generalized Metric Spaces for the Simply Typed Lambda-Calculus (Extended Version)
广义度量，从Lawvere的度量空间丰富的范畴的观点，已被广泛应用于指称语义作为一种方式来衡量在何种程度上两个程序的行为相似，但不等价的方式。然而，到目前为止，将广义度量应用于高阶语言（如简单类型的λ演算）并不令人满意。本文研究了广义度量空间的Carnival闭范畴的一种新的构造方法。我们的出发点是一个定量语义学的基础上，一般的逻辑关系。在这种情况下，我们表明，几个家庭的广义度量提供的方法来扩展欧几里德度量的所有高阶类型。
2021-04-27 cs.LO cs.PL math.LO
Clones, closed categories, and combinatory logic
本文用多元结构阐释简单类型λ演算的语义，引入外延SK-克隆并证明其可靠完备，进而证明不含产品的简单类型λ演算是SK-范畴的内部语言。
2024-05-02 cs.LO math.CT
Justification Logic of the Lambda Calculus
Faculty of Technical Sciences, University of Novi Sad（诺维萨德大学技术科学学院）；Mathematical Institute of the Serbian Academy of Sciences and Arts（塞尔维亚科学院数学研究所）；School of Computer Science, University of Birmingham（伯明翰大学计算机学院）
研究λ演算的证明逻辑，通过引入一种逻辑，其模态证明项为类型化λ项，能同时推理计算与证明。给出公理系统、自然演绎系统及Curry-Howard解释，还构建相继式演算并证明切割消去，得到归一化结果。
2026-07-28 cs.LO math.LO
Ticket Entailment is decidable
我们证明了票蕴涵的可判定性。Anderson和Belnap在关联逻辑的框架内提出的这个问题等价于具有部分基BB'IW的简单类型组合逻辑中的类型栖居的可判定性问题。本文解决了单纯型微积分对遗传右极大项的限制的类型栖居等价问题。
2012-07-05 cs.LO
Full Abstraction for a Recursively Typed Lambda Calculus with Parallel Conditional
我们定义了一个递归类型的λ演算的语法和约简关系，并给出了一个并行的条件函数。减少显示为融合性。我们将递归类型解释为受限形式的信息系统，我们称之为素系统。一个指称语义定义与此解释。定义了项的语法范式逼近，证明了逼近定理：项的语义等于其逼近的语义的极限。证明使用包含谓词（逻辑关系）。对于布尔值的观察，语义是足够的。在平行格功能的存在下，它也是完全抽象的。
2008-06-11 cs.LO
Using Inhabitation in Bounded Combinatory Logic with Intersection Types for Composition Synthesis
我们描述了正在进行的工作，从软件组件库的自动组合合成的框架。这项工作是基于组合逻辑与交叉类型。这个想法是，组件被建模为类型的组合子，和居住的算法{ \textemdash }是否有一个组合项e与类型tau相对于环境伽玛？{ \textemdash }可用于合成组合物。在这里，Gamma以类型化组合子的形式表示存储库，tau指定合成目标，e是合成程序。我们说明我们的方法的例子，包括应用程序的GUI组件合成。
2013-07-31 cs.LO cs.SE
A generalization of falsity in finitely-many valued logics
本文提出了多值逻辑中的一种新的否定类型，为回答以下问题提供了一种不同的方法：某个对象语言公式不具有给定的真值意味着什么？在此过程中，本文给出了任意多值逻辑中真与假的一般定义。
2022-03-31 cs.LO
A Logic of Interactive Proofs (Formal Theory of Knowledge Transfer)
我们提出了一个交互式证明的逻辑作为交互式计算的直观基础的框架，我们通过一个交互式的类似的Goedel-McKinsey-Tarski-Artemov定义的直观逻辑嵌入到一个经典的模态逻辑的证明，和Curry-Howard同构之间的直观证明和类型化的程序。我们的交互式证明实现了持久的认知影响，在他们的预期社区的同行评审，包括在诱导的（命题）知识，他们的证明目标的（个人）知识的证明与解释审查。也就是说，交互式证明通过在多代理分布式系统中传输某些个人知识（可知证明）来实现命题知识（可知事实）的转移。换句话说，我们作为一个社区可以拥有正式的共同知识，即如果我们的一个对等成员知道证明，那么该成员就会知道它的证明目标。最后但并非最不重要的是，我们证明了非平凡的交互式计算定义在我们的简单类型的交互式组合逻辑，但等价于非交互式计算定义的简单类型的组合逻辑。
2017-08-08 cs.CR cs.DC cs.LO
Comparing several calculi for first-order infinite-valued Łukasiewicz logic
从可证明性的观点出发，比较了一阶无穷值Pukasiewicz逻辑和一阶有理Pavelka逻辑的Gentzen型超代数演算，并与Hájek的Hilbert型演算进行了比较.我们的比较的关键方面是密度消除证明的hypereclipse结石之一。
2018-12-13 cs.LO
Binary Sequent Calculi for Truth-invariance Entailment of Finite Many-valued Logics
在本文中，我们考虑具有有限真值集的真值函数多值逻辑类。本文的主要结果是发展了一个新的\emph{binary}演算（每个演算是一对公式）的多值逻辑与一个有限集的真值，和Kripke的似语义，它是既健全和完整的。我们没有使用基于矩阵的逻辑蕴涵与指定的真值的一个严格的子集，但不同的一种新的语义的基础上推广的经典的2值真值不变蕴涵。为了定义这种基于非矩阵的多模态演算，我们利用经典的合取、析取和模态连接词的有限集合，将多值逻辑转化为正2值多模态逻辑。在这个代数框架中，我们定义了一个唯一确定的公理系统，通过扩展经典的2-值分配格逻辑（DLL）的一组新的公理多值逻辑连接。对偶地，在自指Kripke式框架中，我们得到一个唯一确定的框架，其中每个可能世界也是多值逻辑的Lindenbaum代数的等价类，由真值表示。
2011-03-07 cs.LO
Cofree coalgebras and differential linear logic
证明了向量空间中直觉线性逻辑的语义也是微分线性逻辑的一个模型，并且证明了上自由余代数的笛卡尔闭范畴是简单型微分λ演算的一个模型.
2019-01-07 cs.LO
Verification of Ptime Reducibility for system F Terms: Type Inference in<br> Dual Light Affine Logic
在以前的工作中，Baillot和Terui介绍了双轻仿射逻辑（DLAL）作为轻线性逻辑的一种变体，适用于保证λ演算项的复杂性：所有可类型化的项都可以在多项式时间内通过beta约简进行评估，并且可以表示所有Ptime函数。在目前的工作中，我们解决的问题，在二阶DLAL的类型的DLDA项。为此，我们给出了一个过程，从系统F中的一个项开始，确定它在DLAL中是否可类型化，并输出一个具体的类型化，如果存在的话。我们表明，我们的程序可以运行在时间多项式的大小，原来的教会类型的系统F项。
2007-11-15 cs.CC cs.LO
A New Representation Theorem for Many-valued Modal Logics
本文提出了一种新的多值逻辑表示定理的定义，并引入了模态算子，定义了给定逻辑的代数模型与用于定义其Kripke可能世界语义的关系结构之间的更强关系，这种新的框架为基于真值不变性蕴涵的多值逻辑提供了一种新的语义.因此，它与基于具有指定逻辑值子集的矩阵的当前定义有很大不同，用于满足关系，通常难以确定。当多值模态逻辑是基于真值集的完备分配格时，我们得到了一个紧凑的自指Kripke式正则表示。模态逻辑的这个子类的克里普克式语义将多值代数的载体集的联合不可约子集作为可能世界的集合。这个子类的一个重要成员是由新的逻辑值扩展的次协调模糊逻辑，以便也处理不完整和不一致的信息。这个新的理论适用于自认知直觉主义多值逻辑的情况下，基于贝尔纳普的4值双格，作为一个最小的扩展经典逻辑用于管理不完整和不一致的信息以及。
2011-03-01 cs.LO
Typed Hilbert Epsilon Operators and the Semantics of Determiner Phrases (Invited Lecture)
Université de Bordeaux（波尔多大学）；CNRS（法国国家科学研究中心）
限定词短语的语义，无论是定指、不定摹状词还是量化名词短语，通常被认为是一个完全解决的问题：普通名词是属性，限定词是适用于两个谓词的广义量词：对应于普通名词的属性和对应于动词短语的属性。我们首先提出了一个批评这种标准的观点。首先，限定词的语义不遵循句子的句法结构。第二，不定冠词的标准解释不能适用于名词性句子。第三，标准观点忽略了广义量词的两个属性之间的语言不对称性。在续集中，我们提出了一个丰富的类型系统，我们最初开发的词汇语义，使用许多排序的逻辑语义表示的希尔伯特术语的决定词和量词的治疗。我们提出了这个语义框架称为蒙塔古生成词典，并显示这些条款如何更好地匹配的句法结构，避免了上述问题的标准方法。希尔伯特项与选择函数的不同之处在于，每个公式都有一个多态算子而不是一个算子。它们还在意义组装逻辑、处理组合性的类型化λ演算和语义表示的多排序逻辑之间建立了有趣的联系。此外，语义项自然地引入了类型判断，并证实了类型判断是一种预设形式的主张。
2014-06-18 cs.AI cs.CL cs.LO
Many-Valued Coalgebraic Modal Logic: One-step Completeness and Finite Model Property
本文利用谓词提升方法研究了多值形式的余代数模态逻辑。余代数，被理解为一般的转移系统，可以作为各种模态逻辑的语义结构。在余代数模态逻辑中，一个著名的结果是它的完备性可以在一步水平上确定。利用正则模型的构造方法，我们将结果推广到多值情形。我们证明了基于三种不同多值代数结构的余代数模态逻辑的结果，这三种多值代数结构包括：有限值Rukasiewicz代数，用正则常数和Baaz Delta展开的交换积分Full-Lambek代数（FL $_{ew}$ -代数），以及用赋值运算展开的FL $_{ew}$ -代数.此外，我们还利用过滤技巧证明了多值余代数模态逻辑的有限模型性质。
2022-06-15 cs.LO
Moded Types for Grassroots Logic Programs, by AI, for AI (Full Version)
London School of Economics（伦敦政治经济学院）；Weizmann Institute of Science（魏茨曼科学研究所）
本文提出基于模式原子语义的类型定义，通过模式路径扩展Herbrand语义，为AI开发逻辑程序类型提供方法，证明类型正确性。
2026-07-28 cs.DC cs.FL cs.LO
Duality for Fitting's Multi-valued Modal logic via bitopology and biVietoris coalgebra
本文通过扩展双拓扑对偶性并调整双Vietoris构造至成对布尔空间范畴，为Fitting多值模态逻辑建立了双拓扑与余代数对偶性，证明了其可靠性与完备性，并确立了Hennessy-Milner性质。
2025-11-01 cs.LO
On Three-Valued Modal Logics: from a Four-Valued Perspective
本文旨在以生动的直观形象、令人信服的哲学论证和广泛的实际应用，全面解决三值模态逻辑的语义定义这一古老的开放性问题。本文在已有的从创新的角度研究三值逻辑的基础上，采用迂回的方法从四值的角度解释三值逻辑，从而为三值模态逻辑的开发、解释和应用提供了一个通用的、系统的方法论。我们通过两个具体的例子来说明我们的方法，一个是道义的，另一个是认识的，对于这两个声音和强完整的自然演绎证明系统也详细介绍。我们认为，我们的三值模态逻辑作为一个轻量级的候选人合并道义或认知的概念到时态逻辑，没有更重的负担，多模态。
2022-09-27 cs.LO math.LO
Reduction of Many-valued into Two-valued Modal Logics
本文将多值逻辑的二值约简推广到二值多模态逻辑。这种方法是基于多值逻辑的上下文化，引入高阶Herbrand解释类型，其中我们明确地引入了一组代数真值的原始多值逻辑，转换为参数（或可能的世界），和一组经典的两个逻辑值的共存。这种方法接近于注释逻辑中使用的方法，但提供了使用基于Herbrand解释的标准语义的可能性。此外，它使用高阶Herbrand类型的性质，因为它们的基本性质是基于自指Kripke语义，其中可能世界是原始多值逻辑的代数真值。这种自指Kripke语义可以将高阶Herbrand解释扁平化为普通的2-值Herbrand解释，使我们更清楚地了解多值和2-值多模态逻辑之间的关系。该方法被应用于多值逻辑程序类，其中的约简是基于原始多值逻辑的逻辑结构（逻辑连接词）以结构化的方式完成的。在此之后，我们推广的减少一般结构多值逻辑，在一个抽象的方式，基于Suszko的非正式的非建设性的想法。在所有情况下，利用扩展的2值约简，我们得到一类非真值模态元逻辑，其中二值公式是通过对原多值公式应用特定的模态算子而得到的模态语句.
2011-03-04 cs.IT cs.LO math.IT
Neutrality and Many-Valued Logics
在这本书中，我们考虑各种多值逻辑：标准，线性，双曲，抛物，非阿基米德，p-adic，区间，代数等，我们还调查的结果，显示树不同的证明理论框架的多值逻辑，例如框架的下列演绎演算：希尔伯特的风格，代数，和hyperados。我们提出了一个一般的方法，允许系统地构建一个大家庭的非阿基米德多值逻辑分析演算：超有理值，超实值，和p-adic值逻辑的特点是一个特殊的格式的语义与适当的拒绝阿基米德公理。这些逻辑是作为标准多值逻辑（即Lukasiewicz逻辑、Goedel逻辑、Product逻辑和Post逻辑）的不同扩展而构建的。阿基米德公理的非正式意义是任何东西都可以用尺子测量。没有阿基米德公理的逻辑多重有效性也在于真值的集合是无限的，它不是良基的和良序的。在非阿基米德值逻辑的基础上，我们构造了非阿基米德值区间代数逻辑INL，用它来描述中性现象。
2007-07-21 cs.AI cs.LO
