Generalisation of proof simulation procedures for Frege systems by M.L.~Bonet and S.R.~Buss
本文将 Bonet 和 Buss 的证明模拟程序推广到演绎定理不成立的有限值 Łukasiewicz 逻辑，通过扩充 Avron 的 Frege 系统并给出加速上界，并推广到所有有限值情形。
2024-03-14 cs.LO math.LO
An algebraic study of the first order version of some implicational fragments of the three-valued Lukasiewicz logic
MV-代数是Lukasiewicz逻辑的代数语义，由有限链生成的MV-代数是Heyting代数，其中Godel蕴涵可以用De Morgan和Moisil的模态算子表示。在我们的工作中，三价Lukasiewicz逻辑的一个片段进行了研究。提出了命题逻辑和一阶逻辑。在这两种情况下，极大相容理论被研究为Lindenbaum-Tarski代数的Monteiro极大演绎系统。从而证明了关于适当代数结构的充分性定理。
2020-10-23 cs.LO
Complexity Results for Modal Dependence Logic
模态依赖逻辑最近由Väänänen引入。它通过操作符=（）增强了基本模态语言。对于命题变量p_1，.，p_n，=（p_1，...，p_（n-1）;p_n）直观地说明p_n的值由p_1，.，p_（n-1）。Sevenster（J. Logic and Computation，2009）表明，对于非确定性指数时间，模态依赖逻辑的可满足性是完全的。在本文中，我们考虑片段的模态依赖逻辑得到的限制允许命题连接词的集合。我们证明了穷人依赖逻辑的可满足性，这种语言由使用合取、必要性和可能性（即，不允许分离），保持NEXPTIME-完全。如果我们只允许单调公式（没有否定，但有析取），复杂性下降到PSPACE完全性。我们还扩展了Väänänen的语言，允许经典的析取除了依赖析取，并表明可满足性问题仍然是NEXPTIME完全的。如果我们不允许否定和依赖析取，那么对于多项式层次的第二层来说，可满足性是完全的。通过这种方式，我们对Väänänen和Sevenster考虑的命题和依赖运算符的所有限制的可满足性问题的计算复杂性进行了完全分类。
2011-04-04 cs.CC 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
On the Succinctness of Atoms of Dependency
本文通过引入公式大小博弈，系统比较了命题团队逻辑中各类非经典原子的简洁性，在存在片段中获得指数下界，在完整片段中获得多项式上界。
2019-08-19 cs.LO
On Three-Valued Dependence-Like Logics
University of Lodz（罗兹大学）
本文探讨依赖逻辑与三值逻辑的关联，提出两种结合经典联结词与传染性联结词的三值依赖类逻辑，并给出相应的可靠完备无切割二叉相继式演算。
2026-10-07 cs.LO math.LO
Strong Equivalence of Logic Programs with Ordered Disjunction: a Logical Perspective
National and Kapodistrian University of Athens（雅典国立卡波迪斯特里安大学）；University of Ioannina（约阿尼纳大学）
有序析取逻辑程序是对经典逻辑程序的扩展，它具有在程序规则头部表示优先析取的能力。LPOD的初始语义虽然简单且非常直观，但并不是纯粹的模型理论。这样做的后果是，程序的某些属性似乎不平凡的形式化在纯粹的逻辑术语。这种情况的一个例子是LPOD强等价概念的特征。虽然Faber等人（2008）的结果是准确的，但它们没有将LPOD的强等价性表征为某些特定逻辑中的逻辑等价。这与经典逻辑程序的强等价性的著名特征形成了鲜明的对比，正如Lifschitz等人（2001）所证明的那样，强等价性与这里和那里的逻辑中的逻辑等价性相一致。在本文中，我们得到了一个纯粹的逻辑刻画的强等价的LPODs的逻辑等价在一个四值逻辑。此外，我们提供了一个新的证明的coNP-完备性的强等价的LPODs，有兴趣在自己的权利，因为它依赖于这种程序的特殊结构。我们的研究结果是基于Charalambidis等人（2021）介绍的LPODs的最新逻辑语义，我们认为这一事实表明，这种新的语义可能会被证明是LPODs进一步研究的有用工具。
2022-05-10 cs.AI cs.LO
Deciding Boolean Separation Logic via Small Models (Technical Report)
本文提出一种基于小模型边界优化和SMT翻译的分离逻辑判定过程，支持复杂布尔结构与常见链表变体，在符号堆片段上具有竞争力并能处理此前无判定过程的公式。
2024-03-27 cs.LO
A Real-Valued Modal Logic
本文提出一种实值多值模态逻辑，结合Kripke语义与实数上的格群运算，通过带标签tableau系统获得coNEXPTIME上界，并建立模态-乘法片段的消割sequent演算及扩展阿贝尔逻辑的完备性。
2018-01-22 cs.LO
Combining fragments of classical logic: When are interaction principles needed?
我们研究了经典逻辑片段的组合，作为通过添加新的连接词来保守扩展给定布尔逻辑的一种方式，并且我们精确地描述了这样的组合在包含来自两个片段的连接词的签名上产生相应的经典逻辑片段的情况。作为输入。如果由此产生的组合片段只是不完全地被作为输入的成分所表征，这意味着来自一个成分的连接词需要与来自另一个成分的连接词相互作用，从而产生相互作用原则。主要的贡献强烈依赖于（众所周知的）描述的2值克隆后，（不那么知名）公理化程序的2值矩阵奠定了劳滕贝格，并对阿夫隆的非确定性矩阵，这已（最近）被用来产生一个显着的进步理解的语义fibring。
2018-10-16 cs.LO
The Complexity of Reasoning for Fragments of Default Logic
缺省逻辑是由Reiter在1980年提出的。1992年Gottlob将命题缺省逻辑的延拓存在问题的复杂性分类为$\SigmaPtwo$ -完全问题，将轻信和怀疑推理问题的复杂性分类为SigmaP 2-完全问题。PiP 2-完成。此外，他还研究了默认规则的限制，即，半正常默认规则。Selman在1992年提出了类似的方法，使用了无析取和一元缺省规则。本文系统地限定了允许命题连接词的集合。我们给出了一个完整的复杂性分类的所有集合的布尔函数的Post格的意义上的所有三个常见的决策问题的命题缺省逻辑。我们表明，复杂性是一个hexachotomy（SigmaP 2-，DeltaP 2-，NP-，P-，NL-完全，平凡）的扩展存在问题，而对于轻信和怀疑推理问题，我们得到类似的分类没有平凡的情况。
2010-08-23 cs.CC cs.LO
A GLR-like Parsing Algorithm for Three-Valued Interpretations of Boolean Grammars with Strong Negation
针对带否定的布尔文法在经典二值逻辑下规则矛盾难处理的问题，本文定义三值解释并借鉴逻辑编程方法处理矛盾文法，提出类GLR算法判定字符串在对应三值语言中的成员资格。
2024-09-11 cs.FL cs.LO
A propositional cirquent calculus for computability logic
本文提出CL18公理化系统，用于可计算性逻辑的基本命题片段，并证明其相对于该逻辑博弈语义的可靠性与完备性。
2024-11-09 cs.LO math.LO
Algebraic semantics for one-variable lattice-valued logics
任何一阶逻辑的单变量片段都可以被认为是模态逻辑，其中全称量词和存在量词分别被盒模态和菱形模态所取代。在一些情况下，这些逻辑的代数语义的公理化已经得到：最值得注意的是，分别为一阶经典逻辑和直觉主义逻辑的单变量片段的模态对应物S5和MIPC。然而，在一阶中间逻辑的设置之外，缺乏一种通用的方法。本文提供了这样一种方法的基础上设置的一阶格值逻辑，其中公式解释的代数结构与格约简。特别是，公理化得到的模态对应的一个广泛的家庭这些逻辑的一个变量片段通过推广的功能表示定理Bezhanishvili和哈丁一元Heyting代数。一个替代的证明理论的证明也提供了一个变量片段的一阶子结构逻辑，有一个切自由的插值演算，并承认一定的有界插值性质。
2022-09-18 cs.LO math.LO
Inquisitive Team Semantics of LTL
本文提出受探究逻辑启发的InqLTL团队语义，证明其带布尔否定时高度不可判定且表达力弱于带布尔否定的TeamLTL，同时找到一个可判定模型检验、可表达超性质的有意义片段。
2026-11-10 cs.FL cs.LO
Toggling operators in computability logic
Shandong University（山东大学）；Villanova University（维拉诺瓦大学）
可计算性逻辑（Computability Logic，CL）（参见http://www.cis.upenn.edu/~giorgi/cl.html）是一个将逻辑重新发展为可计算性的形式理论的研究项目，与传统上的形式真理论相反。CL中的公式代表交互式计算问题，被视为机器与其环境之间的游戏;逻辑运算符代表对这些实体的操作;“真理”被理解为有效解决方案的存在。合作语言的形式是开放的，并可能会经历一系列的扩展，随着研究的进展。到目前为止，已经研究了三种类型的合取和析取：平行的，顺序的和选择的。本文件增加了一个更自然的类型，这个集合，称为切换。切换操作可以被描述为选择操作的宽松版本，其中选择是可伸缩的，允许重新考虑任何有限次数。通过这种方式，他们在交互式计算中模拟试错式决策步骤。本文的主要技术成果是为可计算性逻辑的命题片断构造了一个合理而完整的公理化，它的词汇表和否定一起包括所有四种合取和析取：平行的、切换的、顺序的和选择的。除了切换合取和析取之外，本文还介绍了量词和递归运算的切换版本。
2010-05-01 cs.AI cs.LO math.LO
On the strongest three-valued paraconsistent logic contained in classical logic and its dual
LP $^{\supset,\mathsf{F}}$是一个三值次协调命题逻辑，本质上与J3相同。它的大多数属性都被认为是合理的次协调命题逻辑的理想属性。然而，从已经发表的结果可以很容易地得出，正好有8192个不同的三值次协调命题逻辑具有相关的性质。本文利用逻辑等价关系的性质来区分LP $^{\supset,\mathsf{F}}$与其它逻辑。作为专注于逻辑等价关系的奖金之一，它被发现，只有32的8192逻辑有一个逻辑等价关系，满足的单位，湮灭，幂等，和交换法律的合取和析取。LP $^{\supset,\mathsf{F}}$的大多数性质都被认为是合理的次协调命题逻辑的理想性质，而它的仿完全类似物也具有类似的性质。本文还利用逻辑等价关系的有关性质，将LP $^{\supset,\mathsf{F}}$的仿完全模拟与具有类似性质的其它三值仿完全命题逻辑区分开来。
2020-12-01 cs.LO math.LO
Combinatory Array Logic with Sums
本文研究扩展了组合数组逻辑的整数索引数组理论，加入序关系和元素求和能力，证明其具有NP上界，并与文献中七个片段比较了表达能力和计算复杂度。
2024-05-01 cs.LO
Towards a Proof Theory of Gödel Modal Logics
针对基本模态模糊逻辑的盒形和菱形片段引入了分析证明演算，该演算将模态逻辑K的Kripke语义与哥德尔逻辑的多值语义相结合.演算用于建立这些片段的完整性和复杂性结果。
2011-05-14 cs.LO math.LO
Positive fragments of coalgebraic logics
正模态逻辑是Dunn在1995年的一篇有影响力的论文中作为标准模态逻辑的正片段而引入的。他的完备性结果包括一个公理化，导出所有模态公式，这些公式在所有Kripke框架上都是有效的，并且只从原子命题、合取、析取、盒子和菱形中构建。本文对这一定理进行了余代数分析，不仅给出了基于对偶理论的概念性证明，而且将Dunn的结果从Kripke框架推广到了弱拉回保函子的余代数.为了便于这种分析，我们证明了一些范畴理论的结果函子的范畴$\mathsf{Set}$的集和$\mathsf{Pos}$的偏序集：每个函子$\mathsf{Set} \to \mathsf{Pos}$有一个$\mathsf{Pos}$丰富的左Kan扩展$\mathsf{Pos} \to \mathsf{Pos}$。以这种方式产生的函子被称为在离散态中有表示。在$\mathsf{Set} \to \mathsf{Pos}$实际上是$\mathsf{Set}$ -值的情况下，我们称相应的左Kan扩张$\mathsf{Pos} \to \mathsf{Pos}$为它的置位.一个$\mathsf{Set}$ -函子保持弱回调当且仅当它的定态保持正合平方。表示为离散点的$\mathsf{Pos}$ -函子保持满射.包涵体$\mathsf{Set} \to \mathsf{Pos}$致密。一个函子$\mathsf{Pos} \to \ma…
2015-09-21 cs.LO math.CT
Possibilistic Computation Tree Logic over Finitely-Valued Kripke Structures: Decidability and Complete Axiomatization
Shaanxi Normal University（陕西师范大学）
本研究针对尚未探讨的PoCTL可满足性问题，通过相关技术证明其可在指数时间内判定，并给出该逻辑的完备公理化，完善了PoCTL的理论基础。
2026-09-22 cs.LO
Outlier detection in default logics: the tractability/intractability frontier
University of Calabria（卡拉布里亚大学）；Jerusalem College of Engineering（耶路撒冷工程学院）
在默认理论中，离群值表示具有意外属性的文字集。在以前的论文中，我们定义了缺省逻辑中的离群点，并研究了它们的形式性质。具体来说，我们已经研究了异常值检测问题的计算复杂性，并证明，虽然它们通常是棘手的，有趣的易处理的情况下，可以挑选出来。根据这些结果，我们在这里研究离群点检测问题的易处理性边界，通过分析它（i）考虑离群点检测问题，（ii）参考默认逻辑片段，（iii）采用离群点的概念。对于第（i）点，我们将考虑三个日益复杂的问题，分别称为离群点-证人识别，离群点识别和离群点存在。至于第（ii）点，当我们寻找可以有效地进行离群点检测的条件时，注意力将限于无析取命题缺省理论的子集。至于第（iii）点，我们将参考[ABP 08]的离群值概念和一个新的更具限制性的概念，称为强离群值。在复杂性结果的基础上，我们提出了一个多项式时间算法来计算拟无循环正态一元缺省理论中所有有界强离群点。我们的一些易处理性的结果依赖于增量引理，提供了条件的一个contrult逻辑片段具有单调的行为。最后，为了表明我们处理的DL的简单片段仍然足够丰富，以解决有趣的问题，因此，我们证明的易处理性结果不仅在理论方面是有趣的，这些片段的表达能力的见解，通过显示正常的一元理论表达所有NL查询，从而间接回答了考茨和塞尔曼提出的问题。
2013-10-30 cs.AI cs.CC cs.LO
Modular many-valued semantics for combined logics
本文利用部分非确定性矩阵上的通用运算，为组合逻辑构建可直接复用各成分逻辑多值语义的模块化语义，并分析有限值性、公理化、片段演算组合与可判定性保持条件。
2023-04-27 cs.LO math.LO
Quantitative Graded Semantics and Spectra of Behavioural Metrics
本文提出定量分级语义框架，统一处理行为度量谱，并给出实值模态逻辑刻画行为距离的一般准则，应用于模糊度量转移系统获得新的迹距离特征逻辑。
2025-01-27 cs.LO
Goedel logics: Prenex fragments
本文对一阶 Goedel logics 允许逻辑等价前束范式的性质进行完整分类，证明仅有限真值集逻辑与 $G_\uparrow$ 允许前束形式，并研究了公式有效性与前束范式有效性间的有效等价存在性。
2024-07-24 cs.LO
Cone-Induced Observation Congruences for Vector-Valued Quantitative Languages
Bahcesehir University（巴切塞尔大学）
本文研究有理多面体锥在向量值定量语言上诱导的观测同余，通过极射线定义内余向量，并利用符号细胞分类增量残差未来，构建观测族载体及观测-精化对应关系。
2026-05-26 cs.FL cs.LO
Complexity of Abduction in Łukasiewicz Logic
本文在无穷值Łukasiewicz模糊逻辑中定义并研究带区间文字的溯因问题，分析解识别、解存在性及假设相关性的计算复杂性，证明子句片段中的溯因推理复杂度低于一般情形。
2025-08-13 cs.LO
Rational Pavelka logic: the best among three worlds?
这一比较调查探讨了三种正式的推理方法与部分真实的陈述和程度的真理，在家庭的Rukasiewicz逻辑。这些方法由无限值Rukasiewicz逻辑（RPL）、理性Pavelka逻辑（RPL）和我们称为分级理性Pavelka逻辑（GRPL）的具有分级公式的逻辑表示。在$0$和$1$之间的所有有理数的真值常数被用作校准真度的技术手段。除了$0$和$1$之外，RationalPavelka逻辑表面上没有真值常数; RationalPavelka逻辑在基本语言中包含常数，并有合适的公理; GradedRationalPavelka逻辑使用分级公式和证明，遵循Pavelka的初衷，受到Goguen工作的启发。从历史上看，Pavelka的论文先于GRPL的定义，而GRPL又先于RPL;检索这些步骤，我们讨论了这些形式系统如何自然地相互演变，我们还记得这个过程是如何在Eukasiewicz逻辑领域中引起争议的。这部作品也可以被解读为逻辑学、逻辑碎片以及逻辑碎片之间关系的案例研究。
2021-12-13 cs.LO math.LO
MacNeille completion and Buchholz' Omega rule for parameter-free second order logics
Buchholz'Omega-规则是一种给出二阶算术的各种子系统的割消的句法的、可能无序的证明的方法。我们的目标是从代数的角度来理解它。在高阶逻辑的割消的许多证明中，Maehara和Okada的代数证明特别有趣，因为他们的论点的本质可以用代数描述为（Dedekind-）MacNeille完成与Girard的约化候选人。有趣的是，事实证明，作为逻辑推理规则的$Ω$规则在MacNeille完备化中找到了其代数基础。在本文中，我们考虑无参数片段LIP 0，LIP 1，LIP 2，…二阶直觉主义逻辑，对应于算术理论ID 0，ID 1，ID 2，.迭代归纳的定义直到Ω。在这种情况下，我们观察到欧米茄规则和MacNeille完成之间的正式连接，导致一种解释二阶量词在一阶的方式在Heyting值的语义，称为欧米茄解释。在此基础上，给出了LIPn的割消的代数证明，证明了LIPn的割消在IDn中是局部形式化的.作为一个结果，我们得到了LIPn的切割消除和IDn的1-一致性之间的等价性，在弱算术理论中成立。
2019-04-09 cs.LO
