Counting proofs in propositional logic
本文给出了一个计算各种命题逻辑中公式的不同证明的方法。这个数字要么是整数（如果公式不可证明，则可能是0），要么是无限大。
2009-05-18 cs.LO math.LO
There are (other) ways to negate in propositional team semantics
本文研究命题团队语义中的否定机制，证明完全直觉主义否定不增加向下封闭逻辑的公理化复杂度，并证明同时含依赖原子与包含原子的命题逻辑具有表达完备性。
2024-10-10 cs.LO math.LO
Logics for Propositional Determinacy and Independence
本文研究了确定性和独立性推理的形式逻辑。命题依赖逻辑D和命题独立逻辑I是最近开发的逻辑系统，基于团队语义，为这样的推理任务提供了一个框架。本文基于Kripke语义，引入了两个新的逻辑L_D和L_I，并分别作为D和I的替代。我们分析了这四种逻辑的相对表达能力，并讨论了这些系统与自然语言的关系。我们认为L_D和L_I自然地解决了D和I中出现的一系列解释问题。我们还得到了L_D和L_I的可靠的和完全的公理化。
2017-12-03 cs.LO math.LO
Remarks on Propositional Logics and the categorial relationship between Institutions and Π-Institutions
在这项工作中，我们探讨了机构和机构-机构概念在命题逻辑中的一些应用，并建立了这些概念之间的精确范畴关系，即，我们提供了一对函子，它们在类别Inst和Inst-Inst之间建立了一个连接。
2016-11-05 cs.LO math.LO
A modal logic amalgam of classical and intuitionistic propositional logic
由哥德尔在1932年提出并由麦肯锡和塔斯基在1948年证明的一个著名的结果是：$φ$是直觉命题逻辑IPC的一个定理当且仅当它的哥德尔翻译$φ'$是模态逻辑S4的一个定理。在本文中，我们扩展了在我们的前一篇文章（S. Lewitzka，Algebraic Semantics for a Modal Logic Close to S1，J. Logic and Comp.，doi：10.1093/logcom/exu 067），并证明了：命题公式$φ$是IPC的一个定理当且仅当$\squareφ$是L的一个定理（实际上，我们证明了：$Φ\vdash_{IPC}φ$当且仅当$\squareΦ\vdash_L\squareφ$，对于命题$Φ,φ$）.因此，映射$φ\mapsto\squareφ$是IPC到L中的嵌入，即L包含IPC的副本。此外，L是经典命题逻辑CPC的保守扩展。在这个意义上，L是CPC和IPC的混合物。证明了L是完备的。一类具有（非正规）模态算子的特殊Heyting代数。
2015-06-03 cs.LO math.LO
Complexity and expressivity of propositional dynamic logics with finitely many variables
研究了命题动态逻辑有限变量片段可满足性的复杂性。我们认为三种形式主义属于三个代表性的复杂性类，广泛理解，-经常PDL，这是EXPTIME-完整的，PDL的交集，这是2 EXPTIME-完整的，PDL与并行组合，这是不可判定的。我们表明，对于这些逻辑中的每一个，即使我们只允许仅由命题常量（即没有命题变量）构建的公式作为输入，可满足性的复杂性也保持不变。此外，我们表明，这是一个后果的丰富的表达能力的变量免费片段：对于所有的逻辑，我们认为，这样的片段是整个逻辑的语义表达。我们推测，这是PDL风格的代表，以及密切相关的逻辑。
2019-01-18 cs.LO math.LO
Validity and Entailment in Modal and Propositional Dependence Logics
本文全面分类了模态与命题依赖逻辑中有效性与蕴涵的复杂性，证明模态依赖逻辑的有效性问题是NEXPTIME完全的，反驳了先前更高的复杂性猜想。
2019-04-25 cs.LO math.LO
A study of cut-elimination for a non-labelled cyclic proof system for propositional dynamic logics
Graduate School of Information Sciences, Tohoku University（东北大学信息科学研究院）
本文研究了命题动态逻辑中非标记循环证明系统的消去问题，提出了序数演算和循环证明系统，并证明了其正确性和完备性，同时展示了消去失败及限制后的消去性质。
2026-03-02 cs.LO math.LO
Cognitive Binary Logic - The Natural Unified Formal Theory of Propositional Binary Logic
本文提出了一种形式化理论，它将命题二元逻辑描述为一种语义封闭的形式语言，并允许在相同的（计算）形式语言中，使用相同的数据结构来表达和测试语法和语义上良好的公式、形式证明（在希尔伯特接受中的可论证性）、演绎（根岑的可论证性观点）、CNF化和解构。本文还指出，认知二元逻辑是一种自我描述的理论，它解构了说谎者悖论。
2011-06-12 cs.LO math.LO
A propositional cirquent calculus for computability logic
本文提出CL18公理化系统，用于可计算性逻辑的基本命题片段，并证明其相对于该逻辑博弈语义的可靠性与完备性。
2024-11-09 cs.LO math.LO
Tableau methodology for propositional logics
Monash University, Melbourne, Australia（莫纳什大学）
本文提出了一种通用的表格法方法，用于生成命题逻辑的表格系统，并推广了Smullyan和Fitting的抽象一致性属性。
2025-11-20 cs.LO math.LO
On decidable extensions of Propositional Dynamic Logic with Converse
本文利用可定义过滤技术，证明若若干模态逻辑容许可定义过滤，则由它们融合扩张的带逆命题动态逻辑具有有限模型性质，从而得到一类可判定的命题动态逻辑。
2023-05-26 cs.LO math.LO
Complexity of the Model Checking problem for inquisitive propositional and modal logic
本文研究了探究命题逻辑 InqB 和探究模态逻辑 InqM 的模型检测问题复杂性，基于 Yang 的思想证明了这两个问题均为 AP-完全。
2024-03-28 cs.LO math.LO
Complexity of finite-variable fragments of propositional modal logics of symmetric frames
虽然命题模态逻辑S5的有限变量片段--相对于自反、对称和传递框架是完备的--是多项式时间可判定的，但对自反和传递框架逻辑的有限变量公式的限制产生了仍然“难以处理”的片段。“对称条件在这方面的作用还没有被研究过。我们表明，对称性本身或结合自反性产生的逻辑，就像逻辑的自反和传递框架，即他们的有限变量片段仍然难以处理，即PSPACE硬。这就提出了这样一个问题：有限变量片段易于处理的模态逻辑和其他模态逻辑之间的边界究竟在哪里。
2019-10-05 cs.LO math.LO
Decision Problems for Propositional Non-associative Linear Logic and Extensions
在我们以前的工作中，我们提出了从完全非结合Lambek演算通过添加一种线性逻辑模态获得的逻辑。我们称这种逻辑为非关联非交换直觉线性逻辑（简称$\mathbf{NACILL}$）。在本文中，我们建立了可判定性和不可判定性结果的各种扩展的$\mathbf{NACILL}$。关于可判定性的结果，我们证明了$\mathbf{NACILL}$的几个推广的演绎问题与左弱化规则是可判定的。关于不可判定性结果，我们证明了非结合非交换经典线性逻辑的所有扩张的压缩和交换规则的可证明性问题是不可判定的。
2020-03-03 cs.LO math.LO
From Proof-theoretic Validity to Base-extension Semantics for Intuitionistic Propositional Logic
本文针对直觉主义命题逻辑，论证其基扩展语义涵盖了一种基于消去规则的证明论有效性版本的陈述内容，既阐释了基扩展语义的运作原理，也证明了该版本证明论有效性的完备性。
2024-09-12 cs.LO math.LO
Weakly complete axiomatization of exogenous quantum propositional logic
给出了外生量子命题逻辑EQPL的一个弱完备有穷公理化。证明进行了使用非平凡的扩展的Fagin-Halpern-Megiddo技术与三个Henkin风格的完成。
2005-03-22 cs.LO math.LO quant-ph
Complexity of Propositional Logics in Team Semantics
我们分类的可满足性，有效性和模型检测问题的命题独立性，包含性和团队逻辑的计算复杂性。我们的主要结果表明，命题组逻辑的可满足性和有效性问题是完全的交替指数时间与多项式多交替。
2017-01-05 cs.CC 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
Duality between unprovability and provability in forward proof-search for Intuitionistic Propositional Logic
逆方法是一种基于饱和度的定理证明技术;它依赖于前向证明搜索策略，可以应用于享有子公式属性的无切演算。在这里，我们应用这种方法来推导直觉命题逻辑中的目标公式G的不可证明性。为了这个目的，我们设计了一个前向演算FRJ（G）的直觉不可证明性，这是倾向于建设性地确定公式G的不可证明性，通过提供一个简洁的反模型，特别是我们证明了生成的反模型具有最小的高度。此外，我们澄清的作用，饱和的数据库获得的结果失败的证明搜索在FRJ（G），通过展示如何从这样的数据库中提取一个派生见证直观的有效性的目标。
2018-04-18 cs.LO math.LO
Definite Formulae, Negation-as-Failure, and the Base-extension Semantics of Intuitionistic Propositional Logic
证明理论语义学（Proof-theoretical Semantics，P-tS）是一种语义学范式，其中逻辑中的意义基于证明（而不是真理）。直觉命题逻辑（IPL）的P-tS的一个特殊实例是它的基扩展语义（B-eS）。这种语义由一个称为支持的关系给出，解释逻辑常数的含义，它由称为基础的规则系统参数化，提供原子命题的语义。在本文中，我们解释的基础上收集的明确的公式，并使用统一的证明搜索-逻辑编程（LP）的证明理论的基础-提供后者的操作视图-建立完整的IPL的B-eS。这种观点允许否定，P-tS中的一个微妙的问题，被理解为在LP中的否定失败协议。具体地说，虽然对命题的否定在传统上被理解为对命题否定的断言，但在B-eS中，我们可以将对命题的否定理解为未能找到对命题的证明，这样，断言和否定都是P-tS中的基本概念。
2023-03-28 cs.LO math.LO
On Quantified Propositional Logics and the Exponential Time Hierarchy
本文从复杂性理论的角度研究了量化命题逻辑。首先，我们引入交替依赖量化布尔公式（ADQBF），它推广了量化和依赖量化布尔公式。我们证明了ADQBF的真值评价是AEXPTIME（poly）-完全的。我们还确定片段的问题是完整的指数层次的水平。第二，我们研究命题的团队为基础的逻辑。我们表明，DQBF公式自然对应于量化命题依赖逻辑，并提出了一个一般的NEXPTIME上界量化命题逻辑与一大类广义依赖原子。此外，我们证明了AEXPTIME（多）-完备性命题队逻辑的扩展与广义依赖原子。
2016-09-14 cs.LO
Dynamic reconfiguration of component-based systems described by propositional configuration logic
本文研究了动态可重构构件系统，其体系结构由命题配置逻辑公式描述。我们提出了几个例子，可重构系统的基础上著名的架构，并状态初步的可判定性结果。
2023-03-06 cs.LO
Model Checking and Validity in Propositional and Modal Inclusion Logics
命题包含逻辑和模态包含逻辑是属于基于团队语义的逻辑家族的形式主义。本文研究了这些逻辑的模型检验和有效性问题。我们确定这两个问题的复杂性界限，包括宽松和严格的团队语义。通过这样做，我们接近完成该计划，其最终目的是分类的中心推理问题的复杂性模态和命题依赖，独立性和包含逻辑。
2017-04-24 cs.LO
A note on undecidability of propositional non-associative linear logics
本文介绍了一种非结合、非交换的命题直觉线性逻辑，称为命题非结合非交换直觉线性逻辑（NACILL）。我们证明了NACILL和它的任何扩展的交换和/或压缩规则是不可判定的。此外，我们介绍了两种类型的经典版本的NACILL，即，NACILL的对合版本和NACILL的循环和对合版本。我们证明这两个逻辑也是不可判定的。
2019-09-30 cs.LO
The Computational Complexity of Propositional Cirquent Calculus
在2006年由Japaridze提出，cirquent演算是一个改进的cirquent演算。由于需要一个具有更明确的资源推理能力的演绎系统，因此出现了cirquent演算。与操纵树状对象（公式、序列等）的更传统的证明理论方法不同，cirquent演算基于称为cirquent的电路风格结构，其中不同的“对等体”（兄弟姐妹，表亲等）子结构可以共享组件。正是这种资源共享机制，使Cirquent演算具有了新颖性（和优点）。从一开始，cirquent演算就与抽象的资源语义配对。这种语义允许对资源提供者和资源用户之间的交互进行推理，其中资源以其最一般和直观的意义被理解。在一个更有限的计算意义上解释资源已经取得了cirquent演算工具公理化的各种基本片段的可计算性逻辑，一个正式的理论（互动）可计算性。在没有特别麻烦的收缩规则的情况下，所谓的“经典”的Cirquent演算规则产生了一个健全而完整的可计算性逻辑系统CL 5。本文研究了CL 5的计算复杂性，证明了它是$Σ_2^p$ -完全的.我们还表明，CL 5没有重复规则的多项式大小的证明，是NP-完全的。
2015-03-24 cs.LO
Propositional dynamic logic for searching games with errors
本文研究了命题动态逻辑的有限值推广及其检验。我们首先介绍了（n+1）-值Kripke模型和相应的语言的基础上的模态扩展的Mukasiewicz多值逻辑。我们说明的定义提供了一个框架，分析的雷尼-乌拉姆搜索游戏的错误。我们的主要结果是（n+1）值Kripke模型理论的公理化。这一结果是通过对最小（n+1）值命题动态逻辑的正则模型的过滤得到的。
2014-01-28 cs.LO
Weighted propositional configuration logics: A specification language for architectures with quantitative features
本文引入并研究了交换半环上的加权命题配置逻辑。我们的逻辑旨在作为一个规约语言的软件体系结构的定量功能。证明了该逻辑中全范式的有效构造和公式等价的可判定性。我们说明了这项工作的动机，通过描述著名的架构配备了定量的特点，在我们的逻辑公式。
2020-01-17 cs.LO
The intuitionistic fragment of computability logic at the propositional level
从可计算性逻辑的语义出发，给出命题直觉演算的可靠性和完备性证明。后者将公式解释为交互式计算问题，形式化为机器与其环境之间的游戏。直觉主义蕴涵被理解为在最弱的可能性-因此最自然-意义上的算法还原，析取和合取作为问题的确定性选择组合（析取=机器的选择，合取=环境的选择），而“荒谬”作为普遍力量的计算问题。请访问http://www.cis.upenn.edu/~giorgi/cl.html以获得关于可计算性逻辑的全面在线资源。
2006-02-11 cs.AI cs.LO math.LO
Propositional dynamic logic with Belnapian truth values
我们介绍BPDL，命题动态逻辑PDL与Odintsov和Wansing研究的基本四值模态逻辑BK的组合（“具有Belnapian真值的模态逻辑”，J. Appl. Non-Class. Log. 20，279- 301（2010））。我们修改的标准参数的基础上的典型模型和过滤，以适应四值的情况下，证明弱完备性和可判定性的BPDL。
2016-08-22 cs.LO
Propositional Computability Logic II
可计算性逻辑是关于计算任务和资源的形式化理论。它的公式代表交互式计算问题，逻辑运算符代表计算问题的运算，公式的有效性被理解为总是有算法解决方案的问题的方案。关于这一主题的全面在线资源可在http://www.cis.upenn.edu/~giorgi/cl.html上查阅。早期的文章“命题可计算性逻辑I”证明了可计算性逻辑的最小非平凡片段CL1的可靠性和完备性。本文将这一结果扩展到更有表现力的命题系统CL2。使CL2比CL1更具表达力的是其语言中存在两种原子：基本原子，表示基本计算问题（即谓词），以及一般原子，表示任意计算问题。CL2保守地扩展了CL1，后者只是前者的一般无原子片段。
2004-06-20 cs.GT cs.LO math.LO
Propositional modal logic with implicit modal quantification
命题项模态逻辑在具有无限多的可达性关系的Kripke结构上解释，因此语法允许变量索引模态和量化。这种逻辑是不可判定的，我们考虑一个变量自由命题的双模态逻辑与隐量化。因此，$[\forall] α$断言所有可及性关系上的必然性，而$[\exists] α$是某些可及性关系上的经典必然性。该逻辑是与一个自然的互模拟模型的关系，我们表明，该逻辑正是一个两个排序的一阶逻辑的互模拟不变片段。该逻辑很容易被看作是可判定的，并且承认有效公式的完全公理化。此外，决策过程自然地延伸到“捆绑片段”的完整术语模态逻辑。
2018-12-29 cs.LO
Proof search for propositional abstract separation logics via labelled sequents
分离逻辑是霍尔逻辑的一个扩展族，用于对改变存储器的程序进行推理。这些逻辑是“抽象的”，因为它们独立于任何特定的具体内存模型。他们的断言语言，称为命题抽象分离逻辑，以各种方式扩展了（布尔）集束蕴涵（BBI）逻辑。我们发展了一个模块化的证明理论，各种命题抽象分离逻辑使用割自由标记的代数演算。我们首先扩展了Hou等人的BBI的割费标记的代数演算，通过添加部分确定性和可取消性的合理规则来处理Calcagno等人的分离代数的原始逻辑，同时保留割消除。我们通过一个合理的中间演算来证明我们演算的完备性，这个中间演算使我们能够从找不到证明的失败中构建反模型。然后，我们捕获其他命题抽象分离逻辑通过添加健全的规则不可分割的单位和不相交，同时保持完整性。我们提出了一个定理证明的基础上，我们的标记演算这些命题抽象分离逻辑。
2013-11-26 cs.LO
Complexity of validity for propositional dependence logics
研究了命题依赖逻辑、模态依赖逻辑和扩展模态依赖逻辑的有效性问题。我们证明了命题依赖逻辑的有效性问题是NEXPTIME-完全的。此外，我们建立了相应的问题的模态依赖逻辑和扩展的模态依赖逻辑是NEXPTIME困难的，在NEXPTIME^NP。
2014-08-26 cs.CC cs.LO
Fuzzy propositional configuration logics
在De Morgan代数上引入并研究了一种加权命题配置逻辑。这种逻辑能够用定量特征来描述软件架构，例如架构中发生的交互的不确定性。我们通过证明每一个公式都可以写成一种特定的形式来处理我们逻辑中公式的等价问题。令人惊讶的是，有公式是等价的，只有在特定的德摩根代数。我们提供了我们的逻辑公式的例子，它描述了著名的软件架构配备了定量功能。
2021-11-28 cs.LO
Combining intermediate propositional logics with classical logic
在[17]中，我们介绍了一种模态逻辑，称为$L$，它结合了直觉命题逻辑$IPC$和经典命题逻辑$CPC$，并且是完全的w.r.t.代数语义学然而，对于Kripke风格的语义来说，$L$似乎太弱了。在本文中，我们增加了积极和消极的内省，并表明，由此产生的逻辑$L5$有一个Kripke语义。对于中间逻辑$I$，我们考虑$L5$的参数化版本$L5(I)$，其中$IPC$被$I$取代。$L5(I)$可以看作是$I$中关于真值推理的经典模态逻辑。从我们的研究结果，我们得出一个简单的方法来确定代数和Kripke语义的一些特定的中间逻辑。我们讨论了一些计算机科学感兴趣的例子，即这里和那里的逻辑，哥德尔-达米特逻辑和扬科夫逻辑。我们的方法提供了新的证明的完整性定理，由于Hoclane，Dummett/Horn和Jankov，分别。
2015-10-19 cs.LO
The parallel versus branching recurrences in computability logic
本文证明了可计算性逻辑的并行递归导出的基本逻辑是分支递归导出的基本逻辑的真超集。后者被称为精确捕获的cirquent演算系统CL 15，由Japaridze保持健全--但不完整--与平行递归，而不是分支递归。目前的结果是通过积极验证该猜想。第二个结果的文件表明，平行递归是严格弱于分支递归的意义上说，而后者在逻辑上意味着前者，反之亦然不成立。
2011-07-12 cs.LO
Intuitionistic Propositional Logic in Lean
该研究在Lean证明助手中形式化直觉主义命题逻辑，验证其两份完备性证明，探究Kripke与代数两种语义范式的关系，还证明了大量定理及演绎规则。
2024-10-31 cs.LO
On sufficient conditions for expressibility of constants in the 4-valued extension of the propositional provability logic $GL$
本文考虑著名的命题可证性逻辑$GL$的最简单的非经典扩展$GL4$以及A.库兹涅佐夫发现了$GL$的四值扩张$L\mathfrak{B}_2$中常数可表示的条件，这是作者在1996年的论文中首次提出的。
2013-12-03 cs.LO
Teaching Intuitionistic and Classical Propositional Logic Using Isabelle
我们描述了一个自然演绎形式化的直觉和经典命题逻辑的伊莎贝尔/纯框架。与早期的工作相比，我们探索了使用深度嵌入方法进行逻辑建模的教学优势，在这里我们采用了逻辑框架建模。这产生了简单而自然的教学例子，我们报告了它在2020年和2021年教授我们的自动推理课程中所发挥的作用。
2022-02-08 cs.LO
Some Remarks on Counting Propositional Logic
计数命题逻辑最近被引入到随机计算中，并被证明能够在逻辑上描述完整的计数层次。在本文中，我们的目的是澄清其单变量片段的直观意义和表达能力。一方面，我们提供了一个有效的程序来衡量计数公式的概率。另一方面，我们明确了这种逻辑和随机实验之间的联系，证明了计数语言可以模拟与二元分布相关的任何（且唯一）事件。
2022-11-16 cs.LO
Resource separation in dynamic logic of propositional assignments
我们扩展了动态逻辑的命题分配，通过添加一个操作的并行组合，这是受分离逻辑。我们提供了一个公理化通过减少公理，从而建立决策。我们还证明了模型检验和可满足性问题的复杂性都停留在PSPACE中。
2021-04-30 cs.LO
Algebraic characterizations of least model and uniform equivalence of propositional Krom logic programs
Vienna University of Technology（维也纳工业大学）
该研究针对命题Krom逻辑程序，给出了其最小模型、包含关系与一致等价的代数刻画结果。
2023-12-11 cs.AI cs.LO
A Heuristic Proof Procedure for Propositional Logic
定理证明是最古老的应用之一，它需要算法来修剪搜索空间。可逆证明程序一直是主要的工具。在本文中，我们提出了一种新的和强大的启发式称为$nongshim$，它可以被看作是可逆证明过程的基本原则。利用这种启发式方法，我们从命题逻辑中的逆演算导出了一个可逆的逆演算\cite{Ketonen,Troe}。
2022-02-22 cs.LO
Uniform Interpolation for Propositional and Modal Team Logics
在本文中，我们考虑模态组逻辑，经典模态逻辑的推广，它是可能的数据之间的依赖现象描述。我们证明，最有名的片段全模态团队逻辑允许消除所谓的“存在互模拟量词”，其中存在的某个集合是模互模拟。因此，我们证明了这些片段享有一致插值性质。
2018-10-12 cs.LO
Terminating Calculi for Propositional Dummett Logic with Subformula Property
本文给出了两个满足子公式性质的命题Dummett逻辑的终止表演算。我们演算的思想依赖于Dummett逻辑的线性有序Kripke语义。第一个演算在两个语义层面上工作：现在和下一个可能世界。第二个演算采用通常的对象语言的Tableau系统，并利用一个属性的建设的完整性定理，引入一个检查，这是一种替代循环检查机制。
2012-06-20 cs.LO
Every super-polynomial proof in purely implicational minimal logic has a polynomially sized proof in classical implicational propositional logic
在这篇文章中，我们将展示如何在最小蕴涵逻辑中证明超多项式大小的任何公式A在经典蕴涵命题逻辑中具有多项式大小的证明。这一事实提供了一个支持任何经典命题重言式都有简短证明的论点，即，NP = CoNP。
2015-08-13 cs.CC cs.LO
Representation Theorems for Cumulative Propositional Dependence Logics
Department of Mathematics and Statistics, University of Helsinki（赫尔辛基大学数学与统计学系）；Theoretical Computer Science, Leibniz University Hannover（汉诺威莱比锡大学理论计算机科学系）；Faculty of Mathematics and Computer Science, FernUniversität in Hagen（哈根应用科学大学数学与计算机科学学院）
本文研究了累积命题依赖逻辑和累积命题逻辑（具有团队语义）的表示定理，证明了其与特定模型的等价性，并为其他累积逻辑的表示定理提供了证明方法。
2026-02-24 cs.AI cs.LO
On the Expressive Power of Sub-Propositional Fragments of Modal Logic
模态逻辑是计算机科学中几种有用和适用的形式系统的范式。它通常保留了经典命题逻辑的低复杂性，但在描述、时间和空间逻辑领域存在明显的例外，其中最具表达力的形式主义具有非常高的复杂性，甚至是不可判定的。为了寻找计算上表现良好的片段，时态和描述逻辑的小句形式和其他子命题限制最近被研究。这种对子命题逻辑的新兴趣主要集中在各种片段的复杂性上，这就提出了关于它们的相对表达能力的自然问题，我们试图在这里回答基本的多模态逻辑Kn。我们考虑霍恩和克罗姆限制，以及模态逻辑的组合限制（称为核心片段），以及正交，通过不允许方块或菱形从正文字出现的片段。我们在一个非常一般的环境中研究这个问题，以便于将我们的结果转移到其他有意义的案例中。
2016-09-14 cs.LO
Sequential composition of propositional logic programs
本文研究命题逻辑程序的顺序组合与分解，证明无环程序可分解为单规则程序，并利用组合表示直接后果算子以计算最小模型，从而弥合语法与语义的鸿沟。
2023-10-11 cs.AI cs.DB cs.DM
A Fixed-Parameter Study on Propositional Dynamic Logic
本文围绕命题动态逻辑（PDL）相关问题的复杂性展开固定参数研究，给出 PL 与 PDL 若干特殊情形的结果。
2024-01-22 cs.LO
Tableaux for Dynamic Logic of Propositional Assignments
CRIL, Univ. of Artois and CNRS（阿尔图瓦大学与法国国家科学研究中心CRIL实验室）；IRIT, Univ. of Toulouse and CNRS（图卢兹大学与法国国家科学研究中心IRIT研究所）
动态命题推理逻辑（DL-PA）是近年来研究的命题动态逻辑（PDL）的一种替代方案。在DL-PA中，PDL的抽象原子程序被命题变量到真值的赋值所取代。这使得DL-PA具有PDL所没有的一些有趣的元逻辑性质，如Kleene星的可消除性、紧性和插值性。我们定义和分析tableaux演算DL-PA，并表明它符合已知的复杂性结果。
2014-06-09 cs.AI cs.LO
On the Relational Translation Method for Propositional Modal Logics
模态逻辑中定理证明的一种方法是将它们转换为谓词演算，然后使用传统的归结式定理证明器。这种方法在实践中被认为是不合适的，因为得到的公式太长，而且不可能证明模态公式的非定理性。在本文中，我们证明了（关系）翻译方法的实际可行性。使用最先进的一阶谓词逻辑定理证明器，我们证明了模态逻辑文献中的许多基准定理。我们证明了命题模态和时态逻辑公式的无效性，使用模型生成器或可满足性测试的经典逻辑。许多可满足的公式被发现具有非常小的模型。最后，几种不同的方法进行了比较。
2021-12-29 cs.LO
Propositional Logics Complexity and the Sub-Formula Property
1979年，理查德·斯塔曼（Richard Statman）利用证明论证明了直觉主义逻辑的纯蕴涵部分（M-蕴涵）是PSPACE-完备的。他展示了从完整的直觉主义命题逻辑到其蕴涵片段的多项式有界翻译。通过Ladner证明的S4的PSPACE-完备性，以及从S4到直觉逻辑的Goedel变换，得出了M-隐含的PSPACE-完备性。逻辑L的演绎系统的子公式原理指出，只要F1，...，Fk证明了A，有一个证明，其中每个公式的出现要么是A的子公式，要么是Fi的某个子公式。在这项工作中，我们扩展了Statman的结果，并表明，任何命题（可能模态）结构逻辑满足一个特定的配方的子公式原则是在PSPACE。如果逻辑包含最小纯蕴涵逻辑，那么它是PSPACE-完全的。因此，EXPTIME完全命题逻辑，如PDL和至少有2个主体的常识认知逻辑满足这个特定的子公式原则，当且仅当PSPACE=EXPTIME。我们还展示了如何我们的技术可以用来证明，任何多值逻辑有它的重言式集在PSPACE。
2015-04-10 cs.LO
