Sahlqvist Correspondence Theory for Instantial Neighbourhood Logic
在本文中，我们研究的Sahlqvist型对应理论的实例邻域逻辑（INL），它可以谈论一个给定的世界的邻域的存在性信息，是一个关系语义和邻域语义之间的混合。我们对对应结果给出了两个证明，第一个证明是直接利用标准平移和最小赋值技术得到的，第二个证明遵循[4]和[6]，其中我们利用双峰平移方法将实例邻域逻辑中的对应问题约化为经典Kripke语义中的正常双峰逻辑。最后，我们给出了一些评论和未来的发展方向。
2020-03-28 cs.LO math.LO
Sahlqvist Correspondence Theory for Sabotage Modal Logic
破坏模态逻辑是一种动态逻辑。它扩展了静态模态逻辑，增加了一个动态模态，该模态被解释为“在框架中删除一个箭头后，公式为真”。本文旨在解决一个公开问题，即给出破坏模态逻辑的Sahlqvist型对应定理。本文定义了破坏Sahlqvist公式，并给出了计算破坏Sahlqvist公式的一阶对应项的算法。最后，我们给出了一些评论和未来的发展方向。
2021-07-02 cs.LO math.LO
A Correspondence between Maximal Abelian Sub-Algebras and Linear Logic Fragments
我们展示了一个分类的最大交换子代数（MASAs）的雅克Dixlane和片段的线性逻辑之间的对应关系。为此，我们暴露了一个修改后的建设吉拉德的超有限几何的相互作用，解释证明运营商在冯诺依曼代数。在这个模型中合理解释的逻辑的表达性取决于MASA的属性，MASA是解释的参数。我们还揭示了MASA在以前的几何互动建设中发挥的重要作用。
2015-09-23 cs.LO math.LO
Unified inverse correspondence for DLE-Logics
通过利用Sahlqvist对应背后的代数和序理论机制，统一对应理论为不同语义和签名的对应性和规范性提供了强大的工具，涵盖了所有其代数语义由正常（分配）格展开（称为（D）LE）给出的逻辑。特别是，算法ALBA，参数在每个（D）LE，有效地计算（D）LE-归纳公式的一阶对应。我们提出了一种算法，利用ALBA的规则和代数语言，以扭转其步骤中的DLE设置，因此有效地计算归纳公式从其一阶对应。
2022-03-17 cs.LO math.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
Distribution-Free Modal Logics: Sahlqvist -- Van Benthem Correspondence
University of Thessaly（色萨利大学）
本文提出无分布模态逻辑中Sahlqvist—Van Benthem对应关系的扩展，通过还原主义策略和格扩展与框架的对偶性实现可扩展的对应关系方法。
2025-03-16 cs.LO math.LO
Correspondence Theory for Many-valued Modal Logic
本文将 Sahlqvist 对应理论推广到以完备 Heyting 代数为真值空间的 Fitting 多值模态语义，定义参数化框架对应并改造 ALBA 算法，证明多值 Sahlqvist 与归纳公式的对应性及经典情形的句法一致性。
2025-06-10 math.LO
On the Correspondence between Nested Calculi and Semantic Systems for Intuitionistic Logics
本文研究了命题直觉主义逻辑、一阶非常数论域直觉主义逻辑和一阶常数论域直觉主义逻辑的标号演算和套演算之间的关系。它示出，拟合的嵌套结石自然产生于其相应的标记结石-为上述每一个逻辑-通过消除标记派生的结构规则。这两种类型的系统之间的平移对应关系被用来表明嵌套演算从其相关的标记演算中继承了证明理论属性，例如规则的完整性，可逆性和切割容许性。由于标记的演算很容易通过逻辑的语义，本文提出的方法可以被看作是一个，从而细化版本的标记演算（包含嵌套的演算片段）具有良好的性能直接从逻辑的语义。
2021-04-19 cs.LO math.LO
Algorithmic correspondence for relevance logics, bunched implication logics, and relation algebras: the algorithm PEARL and its implementation (Technical Report)
非确定性算法过程PEARL（“Propositional variables Elimination Algorithm for Relevance Logic”的首字母缩写）最近已经被开发用于根据标准的Meilley-Meyer关系语义来计算相关逻辑RL的语言的公式的一阶等价物。它成功的一大类公理的相关逻辑，包括所有所谓的归纳公式。在目前的工作中，我们从代数的角度重新解释PEARL，其重写规则被视为操纵在厄克特的相关代数上解释的准不等式，并报告其最近的Python实现。我们还证明了PEARL成功的所有公式都是规范的，即，在相关代数的典型扩张下保持不变。这推广了厄克特1996年论文中的“通过对应的正规性”结果。我们还指出，稍加修改，PEARL可以应用到集束蕴涵代数和关系代数。
2021-08-14 cs.LO math.LO
Unified Correspondence as a Proof-Theoretic Tool
本文旨在建立模态逻辑领域的对应现象与贝尔纳普提出的显示演算理论之间的形式联系。马库斯·克拉赫特（Marcus Kracht）在描述模态公理（他称之为原始公式）的背景下，对这些联系进行了细致的观察和利用，这些模态公理可以有效地转化为显示演算的“分析”结构规则。在这种情况下，一个规则是“分析的”，如果将它添加到一个显示演算保持贝尔纳普的削减消除定理。近年来，对应论的发展已经从经典的模态逻辑统一地扩展到非经典逻辑的不同家族，从（双）直觉（模态）逻辑、线性、相关和其他子结构逻辑，到混合逻辑和μ演算。这种推广产生了一种称为统一对应的理论，其中最重要的技术工具是算法ALBA，以及Sahlqvist型公式和不等式类的语法表征，这些公式和不等式在正常DLE逻辑（逻辑的代数语义是基于有界分配格）的设置中是统一的。我们应用统一对应理论，其工具和见解，扩展Kracht的结果，并证明他的要求在设置DLE逻辑。本文的结果刻画了真可显示DLE-逻辑空间。
2016-03-27 cs.LO math.LO
Coding-Logic Correspondence: Turning Information and Communication Networks into Logical Formulae via Hypergraph Heyting Algebra
The Chinese University of Hong Kong（香港中文大学）
通过超图Heyting代数将信息和通信网络转化为逻辑公式，实现编码设置与逻辑公式的对应关系。
2026-09-18 cs.IT math.IT math.LO
Taming "McKinsey-like" formula: An Extended Correspondence and Completeness Theory for Hybrid Logic H(@)
本文通过改进文[8]中的算法hybrid-ALBA，将文[8]中的混合语言L（@）的归纳公式片段扩充为一个类McKinsey公式，并证明扩充类中的每个公式都有一个一阶对应.我们还确定了这个扩展归纳片段的一个子类，即扩展骨架公式，它扩展了[8]中的骨架公式类，每个公式都公理化了一个完整的混合逻辑。我们这里的证明方法是证明论的，遵循[10，19]和[3，第14章]，与[8]中的代数证明相反。
2022-10-10 cs.LO math.LO
Continuous Algebra: Algebraic Semantics for Continuous Propositional Logic
本文提出连续代数作为连续命题逻辑CPL的代数语义，并通过与2可除$\ell u$-群的对应关系，给出了CPL弱完备性定理的纯代数证明。
2025-12-22 math.LO
A presentation theorem for continuous logic and Metric Abstract Elementary Classes
给出了连续一阶逻辑和度量抽象初等类分别用$L_{ω_1, ω}$和抽象初等类表示的一个表示定理。这个演示是通过分析在函数下闭合的稠密子集来完成的。我们将这种对应关系扩展到类型和饱和度。
2016-09-12 math.LO
Sequent-style tableaux for first-order logic: structural analysis, cut admissibility, and the correspondence with LK
University of Calabria（卡拉布里亚大学）
本文在一阶逻辑语境下，基于Smullyan的块演算，确立其结构性质与切消，证明其与Gentzen LK的对应关系，为sequent式tableaux提供了系统的结构分析。
2026-07-31 math.LO
Correspondence Theory for Modal Fairtlough-Mendler Semantics of Intuitionistic Modal Logic
我们在模态Fairtlough-Mendler语义学（模态FM语义学）\cite{FaMe97}中研究直觉模态逻辑的对应理论，它是可能性语义学\cite{Ho16}的直觉模态版本。我们识别了该语言中的归纳公式片段\cite{GorankoV06}，并在此语义环境下给出了算法$\mathsf{ALBA}$ \cite{CoPa12}.论文有两大特点：一个是在扩展模态语言中，被解释为完美布尔代数中的原子、完美分配格中的完全并素元和完美格中的完全并不可约元的名义变量在本设置中被解释为单例的精化正则开闭包，与经典的正规模态逻辑\cite{Zh21d}的可能性语义相似;另一个特点是我们不使用同形或菱形，这大大限制了归纳公式的碎片。我们证明了健全的$\mathsf{ALBA}$相对于模态FM帧，并表明$\mathsf{ALBA}$成功的归纳公式，类似于现有的设置，如\cite{CoPa12,Zh21d,Zh22a}。
2022-10-05 cs.LO math.LO
Correspondence and Inverse Correspondence for Input/Output Logic and Region-Based Theories of Space
本文发展输入/输出逻辑的代数语义，给出闭开解析不等式的模态刻画、一阶对应与逆对应算法，并将对偶表示推广到预接触和对偶预接触代数。
2024-12-02 cs.LO math.LO
Reconstruction of non-$\aleph_0$-categorical theories
我们把$\aleph 0$ -范畴理论与它们的自同构群之间的对应关系推广到经典逻辑中的任意完备理论和连续逻辑中的某些理论（特别是包括所有$\aleph 0$ -范畴理论）。
2021-02-03 math.LO
Inception Display Calculi
IMDEA Software Institute（IMDEA软件研究所）；Vrije Universiteit Amsterdam（阿姆斯特丹自由大学）；Department of Mathematics and Applied Mathematics, U. of Johannesburg（约翰内斯堡大学数学与应用数学系）
本文提出了一种扩展的显现演算框架，用于涵盖更广泛的逻辑系统，包括非分析归纳公理的公理扩展，并通过统一对应理论和ALBA算法生成分析规则。
2026-05-16 math.LO
The groupoid-based logic for lattice effect algebras
本文的目的是建立一种与格效应代数相对应的逻辑。首先，我们回答了一个自然的问题，即格效应代数是否可以用类广群结构来表示。我们建立了格效应代数与某些具有反调对合的广群之间的一一对应关系。利用这些广群，我们能够引入一个合适的逻辑格效应代数。
2018-10-12 math.LO
The logic induced by effect algebras
效应代数形成量子力学逻辑的代数形式化。对于格效应代数E，我们研究了E的一个自然蕴涵，证明了E的蕴涵约简与E是项等价的。然后，我们提出了一个简单的公理系统在根岑风格公理化的逻辑诱导的格效应代数。对于不需要是格序的效应代数，我们引入了一种处处定义但其结果不需要是单个元素的蕴涵。然后研究了效应蕴涵代数，证明了这些代数与满足升链条件条件的效应代数之间的对应关系。我们给出了一个Gentzen形式的公理系统，它也适用于不一定是格序的效应代数，并证明了它是有限效应代数诱导逻辑的代数语义。
2020-01-18 math.LO
Algebraic logic and logically-geometric types in varieties of algebras
本文的主要目的是说明在逻辑和模型论框架内发展起来的类型概念与代数的几何性质有着深刻的联系。这些联系通过代数逻辑的机制，从泛代数几何到模型论，来回往复。我们发现，类型自然出现在伽罗瓦对应的过滤器之间的Halmos代数的一阶公式的等式和相应的仿射空间的基本集合的逻辑内核。
2011-08-02 math.AG math.LO
Algorithmic correspondence and analytic rules
本文引入算法MASSA，可从经典模态公式生成G3K的分析几何规则与无切割推导，证明其对分析归纳公式的终止性及对应性，还拓展至归纳公式与带量词模态逻辑。
2025-04-15 cs.LO math.LO
A General (Uniform) Relational Semantics for Sentential Logics
University of Thessaly（色萨利大学）
本文提出了一种通用的关系语义学框架，通过公理化和结构的调整，为经典和非经典逻辑提供统一语义，并利用广义Sahlqvist-van Benthem算法进行对应结果计算。
2025-11-23 cs.LO math.LO
A meta-modal logic for bisimulations
Universidad de Málaga（马拉加大学）；Universidad de Sevilla（塞维利亚大学）
本文提出一种元模态逻辑用于研究仿射关系，通过扩展基本模态语言引入新模态，建立仿射关系的定义，并证明其逻辑的可判定性和PSPACE完全性。
2026-10-27 cs.LO math.LO
A model-theoretic characterization of monadic second order logic on infinite words
一元二阶逻辑和线性时态逻辑是两种可用于描述无限词类的逻辑形式，即，基于自然数的一阶模型，具有顺序、后继和多个一元谓词符号。无限字上的一元二阶逻辑（S1 S）可以替代地被描述为在$\mathcal{P}(ω)$中解释的一阶逻辑，$\mathcal{P}(ω)$是自然数的幂集布尔代数，配备有用于“初始”、“下一个”和“未来”状态的模态算子。我们证明了这种结构的一阶理论是对应于线性时态逻辑（LTL）的适当版本的一类代数的模型伴侣没有直到。证明关键使用两个经典的，非平凡的结果，从文献中，即完备性LTL关于自然数，和S1 S-公式和Büchi自动机之间的对应关系。
2016-04-29 cs.FL cs.LO math.LO
A Type Theory for Probabilistic and Bayesian Reasoning
本文提出一种用于概率推理的新型定量类型理论与逻辑，通过谓词与无副作用动作的双射对应推导计算规则，并在图模型示例中计算条件概率，为贝叶斯推理机械化奠定基础。
2015-11-30 cs.LO math.LO math.PR
Quantum Logic in Intuitionistic Perspective
在他们的开创性论文伯克霍夫和冯诺依曼揭示了以下困境：“.对于逻辑学家来说，否定的正交互补性质是最经不起批判性分析的性质，而力学的研究则指出，分配恒等式是逻辑代数中最薄弱的环节。“在本文中，我们消除了这种困境，提供了一种同时保持两者的方法。通过在物理系统的性质格中引入“缺失”的析取，同时将交作为合取继承，我们得到了一个关于物理性质的完备的Heyting命题命题代数代数.特别是有一个双射之间的对应关系的性质格和命题格配备了所谓的操作决议，一个操作，暴露的性质的水平上的命题。如果属性格配备了一个正交补，那么这个双射对应可以被细化为一个配备了运算补的命题格，这样就建立了上面的主张。从形式上讲，通过物理和逻辑上的考虑，我们分别重新发现了Bruns和Lakser（1970）关于交半格的内射壳的纯数学结果的一个规范和一个改进。从我们的表示，我们可以得到一个真正直观的功能性的影响，财产格，因此面对索赔在以前的著作就此事。我们还对析取性与分配性、有限与无限合取性作了详细的分析，简要地回顾了Bruns-Lakser构造并指出了一些有待解决的问题。
2002-04-22 math-ph math.LO math.MP
