Representation and duality of the untyped lambda-calculus in nominal lattice and topological semantics, with a proof of topological completeness
我们给出了一个语义的λ演算的基础上的拓扑对偶定理的名义集。一个新的解释lambda给出的伴随，和lambda-条款绝对解释为集（没有估值是必要的）。
2016-10-06 cs.LO math.LO
On affine usages in signal-based communication
我们描述了一个类型系统的同步π演算正式的概念，仿射使用基于信号的通信。特别是，我们确定了数量有限的用法，保持亲和力，可以组成。作为一个主要的应用程序的系统，我们表明，类型化的程序是确定性的。
2008-09-03 cs.LO
Proof-relevant pi-calculus
形式化π演算是对逻辑框架和机械化元理论系统的表达能力的启发性测试，因为存在名称绑定、带有名称挤出的标记转换、互模拟和结构一致性。形式化已经在各种系统中进行，主要集中在充分研究（和具有挑战性）的属性，如过程互模拟理论。我们提出了一个形式化的Agda，而不是探讨理论的并发转换，残留，因果等价的痕迹，这是以前没有正式的π演算。我们的形式化采用德Bruijn指数和依赖类型的语法，并对齐的“证明转换”提出的Boudol和Castellani在CCS的上下文中与自然存在的Agda的表示标记的过渡关系的证明条款。我们的主要贡献是证明了“钻石引理”的剩余的并发过渡和一个正式的定义等价的轨迹置换的过渡。
2015-07-29 cs.LO
Nominal Henkin Semantics: simply-typed lambda-calculus models in nominal sets
我们研究了一类简单类型的λ演算的名义代数Henkin式模型，其中变量映射到表示中的名称，而λ演算抽象映射到（非功能性的）名称抽象操作。由此产生的表示更小，更好的行为，在我们精确的方式，比基于函数值的模型。使用这些新的模型，我们然后开发了一个概括的λ-长期语法丰富他们的存在元变量，从而产生一个理论的不完整的功能。这种不完备性与函数抽象和应用给出的不完备性的通常概念是正交的，并且对应于洞和不完备对象。
2011-11-01 cs.LO cs.PL
Consequence-based Reasoning for Description Logics with Disjunction, Inverse Roles, Number Restrictions, and Nominals
University of Oxford（牛津大学）
我们提出了一个基于结果的演算的概念包容和分类的描述逻辑ALCHOIQ，它扩展了ALC的角色层次结构，逆角色，数量限制，和名词。通过使用标准的转换，我们的演算扩展到SROIQ，它涵盖了所有的OWL 2 DL除了数据库。我们的演算的一个关键特征是它的现收现付行为：与现有的算法不同，我们的演算对于所有已知的ALCHOIQ适当片段都是最坏情况下的最优，尽管不是对于完整的逻辑。
2018-05-03 cs.AI cs.LO
A Linear-Time Nominal $μ$-Calculus with Name Allocation
无限字母表语言的逻辑和自动机模型，如Freeze LTL和寄存器自动机，用于验证过程或带有数据的文档。它们与名义集上的形式主义密切相关，例如非确定性轨道有限自动机（NOFA），其中名称扮演数据的角色。在这种形式主义中的推理问题在计算上往往是困难的。名字绑定的名义自动机模型，如规则的非确定性名义自动机（RNAs）已被证明是计算上更容易处理。在本文中，我们介绍了一个线性时间不动点逻辑Bar-muTL有限字在一个无限的字母表，它的特点是完全否定和冻结量化通过名称绑定。我们通过对扩展的正则非确定性名义自动机的非平凡约简表明，尽管Bar-muTL允许无限制的非确定性和无限多的寄存器，但RNAs上的模型检验Bar-muTL和可满足性检验都具有基本的复杂性.例如，模型检验在2 ExpSpace中，更准确地说是在参数化的ExpSpace中，有效地将寄存器的数量作为参数。
2021-08-20 cs.FL cs.LO
De Morgan Dual Nominal Quantifiers Modelling Private Names in Non-Commutative Logic
本文探讨了必要的证明理论推荐一个富有表现力的，但可判定的一阶系统，名为MAV 1，具有德摩根对偶对名义量词。这些名量词被称为“新”和“文”，不同于自对偶的Gabbay-Pitts和Miller-Tiu名量词。这些名词性量词的新颖之处在于它们是两极分化的，在这个意义上，“新”分布在积极的运营商，而“文”分布在消极的运营商。这种对簿记的更大控制使私有名称能够在MAV 1中嵌入公式的过程中建模。技术上的挑战是建立一个割消结果，从其中的基本性质，包括传递性的蕴涵遵循。由于该系统是使用微积分的结构，一个概括的微积分，新的技术被采用。证明依赖于一个复杂设计的基于多集的证明大小的度量，它被用来指导一种称为分裂的规范化技术。在分裂证明中，交换连续量词的等方差的存在导致了名义量词、加法合取算子和乘法算子之间复杂的相互依赖。每一条规则都通过一个例子来证明，为什么这条规则对于合理地嵌入流程和确保削减消除是必要的。
2020-01-15 cs.LO
A Mechanised Proof of Gödel's Incompleteness Theorems using Nominal Isabelle
一个伊莎贝尔/HOL形式化哥德尔的两个不完全定理。这项工作遵循Zeriwierczkowski的详细证明定理使用遗传有限（HF）集理论。避免通常的算术编码的语法消除了形式化的必要性，在嵌入式逻辑演算的初等数论。伊莎贝尔形式化使用两个单独的治疗变量绑定：标称包的规模，以发展这种复杂性，而德Bruijn指数原来是理想的编码语法。伊莎贝尔证明的关键细节进行了描述，特别是在文献中发现的差距和错误。
2021-04-28 cs.LO
Reconciling positional and nominal binding
我们定义了一个简单类型的λ演算的扩展，其中两种不同的绑定机制，通过位置和名称，很好地共存。在前者中，和标准λ演算一样，参数和自变量之间的匹配是在位置基础上完成的，因此α等价成立，而在后者中，它是在名义基础上完成的。这两种机制也分别对应于静态绑定和动态绑定，静态绑定在编译时检查参数的存在性和类型兼容性，动态绑定在运行时检查参数的存在性和类型兼容性。
2013-07-31 cs.LO cs.PL cs.SE
Permissive-Nominal Logic (journal version)
本文介绍宽容名义逻辑（PNL），一种扩展一阶谓词逻辑以支持绑定器的逻辑，能有限公理化算术及带绑定的名义数据类型，兼具高阶逻辑的表达力与一阶逻辑的简洁性。
2023-12-27 cs.LO
Proofs as Execution Trees for the π-Calculus
本研究基于演绎即计算范式，为π演算构建新型逻辑框架，通过扩展一阶乘法加法线性逻辑的无切割矢列式演算，将进程对应为公式、证明对应为计算，并设计证明网给出推导的典范表示。
2025-01-16 cs.LO
Proof-Relevant Logical Relations for Name Generation
本文提出用证明相关逻辑关系为带递归的名称生成语言构建直接风格模型，解决动态分配单子构造失效问题，并提供一个易于理解的介绍性场景。
2018-03-29 cs.LO
Nominal Unification from a Higher-Order Perspective
名义逻辑是一阶逻辑的一个版本，具有相等性，名称绑定，通过名称交换重命名和名称的新鲜性。类似于高阶逻辑，可绑定的名称，称为原子，和可实例化的变量被认为是不同的实体。此外，原子可以通过实例化来捕获，这打破了原子演算的基本原则。尽管有这些差异，名义统一可以从更高层次的角度来看。从这个角度来看，我们表明，名义统一可以减少到一个特定的片段高阶统一问题：高阶模式统一。这种减少证明，名义统一可以决定在二次确定性时间，使用高阶模式统一的线性算法。我们还证明了翻译保持最一般的统一。
2010-05-20 cs.LO cs.SC
Proof-Theory and Semantics for a Theory of Definite Descriptions
本文提出了一种定摹状词理论，在这种理论中，这些表达式在完整的句子的上下文中由一个二元量词$I$形式化，并给出了一个对偶域语义。$I$由两个公式组成一个公式。$Ix[F, G]$表示“$F$是$G$”。这种方法的优点是将范围区分直接合并到符号中。本文证明了一个经典正自由逻辑系统用$I$的割消去，并证明了它在语义上是可靠的和完备的。该系统具有一些新的功能，并简要地比较了通常的方法正式的“的$F$”由一个长期形成运营商。它并不符合欣蒂卡和兰伯特的首选理论，但分歧是动机良好和有吸引力的。
2021-08-09 cs.LO math.LO
A Formalized Extension of the Substitution Lemma in Coq
本文在 Coq 中形式化验证了扩展显式替换算子后的 lambda 演算语法下替换引理仍然成立，采用 nominal 方法处理 alpha 等价，为不同显式替换演算提供了通用框架。
2023-09-25 cs.LO
Nominal Matching Logic
我们引入名义匹配逻辑（NML）作为匹配逻辑的扩展与名称和绑定以下的Gabbay-Pitts名义的方法。匹配逻辑是$\mathbb{K}$框架的基础，用于指定程序设计语言并自动派生相关工具（编译器、调试器、模型检查器、程序验证器）。匹配逻辑不包括名称绑定的原始概念，尽管绑定运算符可以通过编码来表示，该编码将函数的图从绑定名称内部化为包含绑定名称的表达式。这种方法足以表示涉及绑定运算符的计算，但是还没有与对具有绑定的语法的归纳推理的支持相协调（例如，对$λ$项的推理）。名词逻辑是一个关于名称和绑定的形式化推理系统，它为基于绑定的语法的归纳推理提供了良好的和强大的原则，NML继承了这些原则。我们讨论了NML的语法和语义的设计方案，证明元理论的属性，并给出例子来说明其表达能力。特别是，我们展示了如何归纳原则$λ$ -条款（$α$ -结构归纳）可以定义和用于证明标准属性的$λ$ -演算。
2022-07-28 cs.LO cs.PL
Hypertableau Reasoning for Description Logics
University of Oxford（牛津大学）
我们提出了一种新的推理演算的描述逻辑SHOIQ^+-一个知识表示形式主义与应用领域，如语义Web。不必要的非确定性和大型模型的建设是两个主要来源的低效率的基于表的推理演算中使用的国家的最先进的推理机。为了减少不确定性，我们基于超表和超分辨率演算，我们扩展了阻塞条件，以确保终止。为了减少所构造模型的大小，我们引入了任意位置成对分块。我们还提出了一个改进的名义介绍规则，确保终止在存在的名义，逆角色，和数量限制-DL结构的组合，已被证明是出了名的难以处理。我们的实现显示出显着的性能改进，在国家的最先进的推理几个著名的本体。
2014-01-15 cs.AI cs.LO
Complete and Terminating Tableau Calculus for Undirected Graph
本文针对无向图构造混合逻辑的表列方法，证明其完备性与终止性，并由此得出该逻辑的可判定性。
2024-11-25 cs.LO math.LO
Concurrency Models with Causality and Events as Psi-calculi
PSI演算是名义演算的参数框架，其中标准演算作为实例，如pi演算，或密码学spi演算和应用pi。PSI演算具有交错的操作语义，其理论基础是名义集和进程代数。PSI演算的大部分表达能力来自其逻辑部分，即，断言、条件和蕴涵，它们是开放的，因此可以容纳广泛的逻辑。我们感兴趣的是这种表现力如何处理基于事件的并发模型。因此，我们采取流行的素数事件结构模型，并给出一个编码到一个PSI演算的实例。我们还采取了最近的动态条件响应图（其中严格包括事件结构）和表现力的模型，并给出了一个编码到另一个相应的PSI演算的实例。我们实现的编码看起来相当自然和直观。关于这些编码的其他结果使我们对它们的正确性更有信心。
2014-10-28 cs.DC cs.LO
Proofs Without Nominals: Gödel's Ontological Argument, its Shallow Embedding, and the Open Questions of the Monatshefte Notes
Otto-Friedrich-Universität Bamberg（班贝格奥托-弗里德里希大学）；Freie Universität Berlin（柏林自由大学）
本文通过机械分析浅嵌入证明，证实哥德尔本体论论证的294个定理均可在无名义词的对象语言内证明，并修正合取公理后解决了《数学月刊》笔记遗留的三个开放问题。
2026-11-03 cs.AI cs.LO math.LO
A Normalizing Computation Rule for Propositional Extensionality in Higher-Order Minimal Logic
单值公理表达了依赖类型论的外延性原则。然而，如果我们只是简单地将单价公理添加到类型论中，那么我们就失去了规范性的性质--每个闭项都计算为一个规范形式。当一个计算达到它需要评估一个证明项的点时，它就被“卡住”了，这个证明项是单价公理的一个应用。所以我们希望找到一种方法来计算与univalence公理。虽然这个问题已经解决了制定的立方类型论，其中的计算表示使用名义上的扩展的微积分，它可能是有趣的探索替代解决方案，不需要这样的扩展。作为第一步，我们在这里提出了一个系统的命题高阶极小逻辑（PHOML）。PHOML中有三种类型判断。有一些术语存在于类型中，它们是$Ω$上的简单类型。存在着存在于命题中的证明，这些命题是$Ω$类型的项。规范命题是由$\bot$通过蕴涵$\supset$构造的命题。第三，存在于方程$M =_A N$中的路径，其中$M$和$N$是$A$类型的项。有两种方法可以证明一个等式：自反性和命题外延性-逻辑等价的命题是相等的。这个系统允许一些定义等式，而这些等式在立方类型论中是不存在的，即沿着平凡路径的传输是恒等式。我们给出了这个系统的一个按名调用约简关系，并证明了这个系统满足规范性：每一个闭类型项首约简为一个规范型。这项工作已在阿格达正式确定。
2017-03-13 cs.LO
