Weighted propositional configuration logics: A specification language for architectures with quantitative features
本文引入并研究了交换半环上的加权命题配置逻辑。我们的逻辑旨在作为一个规约语言的软件体系结构的定量功能。证明了该逻辑中全范式的有效构造和公式等价的可判定性。我们说明了这项工作的动机，通过描述著名的架构配备了定量的特点，在我们的逻辑公式。
2020-01-17 cs.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 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
Non-expansive Fuzzy ALC
为平衡模糊描述逻辑中 Lukasiewicz 基的高复杂性与 Zadeh 基的低表达力，提出非扩张性模糊 ALC，引入常数移位算子，并设计 EXPTIME 复杂度的 tableau 推理方法。
2025-10-10 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
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
Classical propositional logic and decidability of variables in intuitionistic propositional logic
我们改进了这个问题的答案：当一个公式中的命题变元在经典命题逻辑中是可证明的时候，在直觉主义命题逻辑中，什么样的被排除的中间集足以证明这个公式。
2014-08-06 cs.LO math.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
On the Expressive Power of Sub-Propositional Fragments of Modal Logic
模态逻辑是计算机科学中几种有用和适用的形式系统的范式。它通常保留了经典命题逻辑的低复杂性，但在描述、时间和空间逻辑领域存在明显的例外，其中最具表达力的形式主义具有非常高的复杂性，甚至是不可判定的。为了寻找计算上表现良好的片段，时态和描述逻辑的小句形式和其他子命题限制最近被研究。这种对子命题逻辑的新兴趣主要集中在各种片段的复杂性上，这就提出了关于它们的相对表达能力的自然问题，我们试图在这里回答基本的多模态逻辑Kn。我们考虑霍恩和克罗姆限制，以及模态逻辑的组合限制（称为核心片段），以及正交，通过不允许方块或菱形从正文字出现的片段。我们在一个非常一般的环境中研究这个问题，以便于将我们的结果转移到其他有意义的案例中。
2016-09-14 cs.LO
A Canonical Fuzzy Logic
介绍了基本概念和操作a）的命题演算的一个变种的模糊逻辑-规范模糊逻辑，CFL -并在一个更简洁和介绍性的方式，b）理论的模糊集根据相同的逻辑。如果一个参数$w$的数值仅限于0和1这两种可能性，则二价经典逻辑和经典集合论的命题演算可以看作CFL相应理论的特例.
2021-05-25 cs.LO math.LO
A Fixed-Parameter Study on Propositional Dynamic Logic
本文围绕命题动态逻辑（PDL）相关问题的复杂性展开固定参数研究，给出 PL 与 PDL 若干特殊情形的结果。
2024-01-22 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
Resolution in Linguistic Propositional Logic based on Linear Symmetrical Hedge Algebra
本文介绍了一个命题语言逻辑，作为自动不确定推理的语言信息的基础。首先，我们建立了一个基于线性对称对冲代数的真值域语言逻辑系统。然后，我们考虑哥德尔的t-范数和t-连接词来定义我们逻辑的逻辑连接词。接下来，我们提出了一个决议推理规则，其中两个条款有矛盾的语言真值可以解决。我们还给出了可靠性的概念，以捕捉的近似性质的决议推理规则。最后，我们提出了一个解决方案的最大可靠性。
2013-07-30 cs.LO
Non-commutative propositional logic with short-circuited biconditional and NAND
短路求值（Short-circuit evaluation）表示命题连接词的语义，其中只有当第一个参数不足以确定表达式的值时，才对第二个参数求值。在程序设计中，短路求值被广泛使用，左序合取和析取作为原始连接词。我们考虑左序，非交换命题逻辑，也被称为MSCL（记忆短路逻辑），并从以前出版的，等式公理化。首先，我们扩展这个逻辑的左序版本的双连续连接，这使得一个优雅的axiomatisation的MSCL。接下来，我们考虑一个左顺序版本的NAND操作（谢弗中风），并再次给出一个完整的，等式axiomatisation相应的变体MSCL。最后，我们认为这些逻辑系统中的一个三值设置为“未定义”的常数，并再次提供完整性的结果。
2022-03-17 cs.LO
Propositional Logics of Dependence
本文在命题层次上研究依赖逻辑。我们证明了几个有趣的命题依赖逻辑，包括命题依赖逻辑，命题直觉依赖逻辑以及命题查询逻辑，是表达完备的，并且具有析取或合取范式.我们提供了演绎系统，并证明了这些逻辑的完备性定理。
2016-03-07 cs.LO math.LO
Finitely-valued propositional dynamic logic
我们研究了命题动态逻辑的一个多值推广，其中Kripke模型的状态公式和状态之间的可达性关系在有限FL-代数中求值。对这个框架的一个自然的解释是关于执行结构化行动的成本的推理。证明了有限FL-代数上的PDL是可判定的。我们还建立了一类基于具有典型常数的交换积分FL-代数的PDL的一般完备性结果。
2020-12-22 cs.LO
Optimal and Cut-free Tableaux for Propositional Dynamic Logic with Converse
本文给出了一个最优的（EXPTIME）、可靠的和完全的基于表的判定逆命题动态逻辑（CPDL）可满足性的算法，该算法不需要使用解析割。我们的主要贡献是一个健全的methodto结合我们以前的最佳方法跟踪最少不动点的PDL与我们以前的最佳方法处理逆的描述逻辑ALCI。扩展是不平凡的，因为这两个方法不能简单地组合。我们提供了足够的细节，以便其他人能够实现。我们的OCaml实现似乎是CPDL的第一个定理证明器。
2010-04-15 cs.LO
Logical Characterizations of Fuzzy Bisimulations in Fuzzy Modal Logics over Residuated Lattices
描述逻辑中的模糊自动机、模糊标号转移系统、模糊Kripke模型和模糊解释等模糊结构之间存在清晰和模糊两种互模拟。完全剩余格上的模糊自动机之间的模糊互模拟已经在2012年由Kririć等人引入。扇入在2015年（分别是Nguyen等人在2020年）提供了剩余格[0，1]上具有Gödel t-范数的模糊Kripke模型（分别是描述逻辑中的模糊解释）之间模糊互模拟的逻辑刻画。一般剩余格上的模糊图结构之间的模糊互模拟缺乏逻辑刻画，剩余格[0，1]上的模糊图结构之间的模糊互模拟也缺乏逻辑刻画.本文给出并证明了剩余格上模糊模态逻辑中模糊互模拟的逻辑刻画。所考虑的逻辑是模糊命题动态逻辑及其片段。我们的逻辑刻画涉及模糊互模拟下公式的不变性和模糊互模拟的Hennessy-Milner性质。它们可以重新表述为其他模糊结构，如模糊标签转换系统和描述逻辑中的模糊解释。
2021-06-15 cs.LO
A van Benthem Theorem for Fuzzy Modal Logic
我们提出了一个模糊（或定量）版本的范本特姆定理，其特点是命题模态逻辑作为一阶逻辑的互模拟不变片段。具体来说，我们考虑一阶模糊谓词逻辑及其模态片段，并表明，模糊一阶公式是非扩张的w.r.t.互模拟距离的自然概念正好是那些可以通过模糊模态公式来近似的概念。
2018-02-05 cs.LO
A Complete Axiom System for Propositional Interval Temporal Logic with Infinite Time
区间时态逻辑（Interval Temporal Logic，ITL）是一种用于时间段推理的时态逻辑。25年来，国际交易日志以多种方式得到应用，并对若干国际交易日志变体、公理系统和工具进行了研究。我们解决了长期以来的开放问题，找到一个完整的公理系统的基本量词自由命题ITL（PITL）的无限时间分析非终止计算系统。我们的完整性证明使用减少到完整的PITL有限时间和传统的命题线性时间时序逻辑。与非初等计算复杂性同样表达逻辑的完整性证明不同，我们的语义方法不使用表格，子公式关闭或明确的演绎涉及编码的欧米茄自动机和非平凡的技术，以补充它们。我们相信，我们的结果也提供了基于区间推理的自然性的证据。
2012-08-10 cs.LO
A Non-wellfounded, Labelled Proof System for Propositional Dynamic Logic
我们定义了PDL的无穷标号代数演算G3 PDL ^{ \infty }.然后给出了一个有限可表示的循环系统G3 PDL ^ω。我们表明，这两个是健全的和完整的PDL的标准模型，并进一步，G3 PDL ^{ \infty }是无割完全的。此外，我们还研究了证明搜索策略的循环系统的片段PDL没有测试。
2019-05-16 cs.LO
Sahlqvist Correspondence Theory for Second-Order Propositional Modal Logic
带有命题量词的模态逻辑（即二阶命题模态逻辑（SOPML））在模态逻辑的早期就被考虑过。它的表达能力和复杂度都很高，并且它的van-Benthem-Rosen定理和Goldblatt-Goldblason定理已经被ten Cate（2006）证明。然而，Sahlqvist理论的SOPML尚未被认为在文献中。在本文中，我们填补了这一空白。我们发展了SOPML的Sahlqvist对应理论，它涵盖并适当地扩展了基本模态逻辑中现有的Sahlqvist公式。我们定义类的Sahlqvist公式SOMPL一步一步的分层方式，其中每个公式被证明有一个一阶对应的Kripke框架有效地计算的算法$ALBA^{SOMPL}$。此外，我们表明，某些$Π_2$规则对应于$Π_2$ -Sahlqvist公式在SOMPL，进一步对应于一阶条件，即使是非常简单的SOMPL Sahlqvist公式，他们可能已经是非规范的。
2021-10-16 cs.LO
Separating the Expressive Power of Propositional Dynamic and Modal Fixpoint Logics
我们调查的表达能力的两种主要类型的程序逻辑复杂的，非常规的程序属性在文献中发现：那些扩展命题动态逻辑（PDL），和那些扩展模态μ演算。这是受到最近发现的一种可判定程序逻辑的启发，这种逻辑被称为具有Chop的可见下推定点逻辑，它将模态μ演算和PDL扩展到可见下推语言上，到目前为止，这构成了可判定程序逻辑的两个支柱。在这里，我们表明这个逻辑不仅比它的两个片段中的任何一个更具表达力，而且事实上比它们的结合更具表达力。因此，程序逻辑之间的可判定性边界已经被适当地推高。我们完成了图片提供的结果分离所有的PDL为基础的和模态不动点逻辑与定期，明显下推和任意上下文无关的建设。
2021-08-24 cs.LO
Probabilistic Model Checking for Propositional Projection Temporal Logic
命题投影时序逻辑（Propositional Projection Temporal Logic，PPTL）是一种用于硬件和软件系统中时间段推理的有用形式，可以处理顺序和并行组合。本文基于离散时间马尔可夫链，研究了PPTL的概率模型检验方法，用于检验任意线性时间性质。我们首先定义一个范式图，表示为NFG_inf，捕捉PPTL公式的无限路径。由于离散时间马尔可夫链是确定性的概率模型，我们进一步根据Safra的构造方法给出了确定和最小化非确定性NFG_inf的算法。
2010-11-05 cs.LO
On complexity of propositional Linear-time Temporal Logic with finitely many variables
众所周知[DemriSchnoebelen 02]，命题线性时间时态逻辑LTL的可满足性和模型检查问题，在语言中只有一个命题变量，都是PSPACE完全的，这与LTL的这些问题的复杂性相一致，具有任意数量的命题变量[SislaClarke 85]。在本文中，我们表明，通过修改[SislaClarke 85]中LTL的空间硬度的原始证明，可以得到相同的结果;即，我们展示了如何修改来自[SislaClarke 85]的构造，以仅使用一个变量的公式来模拟多项式空间约束的图灵机的计算。我们相信，我们对[DemriSchnoebelen 02]结果的替代证明提供了对LTL的语义和计算特性的额外见解。
2018-11-25 cs.LO
Relating Sequent Calculi for Bi-intuitionistic Propositional Logic
双直觉主义逻辑是直觉主义逻辑的保守推广，具有一个与蕴涵有关的联结对偶。它有时被认为是经典逻辑的一个对称构造子系统。本文比较了双直觉命题逻辑中的三种推理演算：（1）基本标准式推理演算，它将蕴涵右推理和蕴涵左推理的前提分别限制为单结论;（2）Gore等人的嵌套序列演算，其中一个完整的类的削减被封装到特殊的“unnest”规则和（3）削减自由标记的逻辑的Kripke语义派生的演算。我们表明，这些演算可以相互转化，并讨论了不可消除的削减标准风格的微积分。
2011-01-28 cs.LO
Why Does Propositional Quantification Make Modal and Temporal Logics on Trees Robustly Hard?
本文研究树语义下带命题量词的模态与时态逻辑的复杂性，证明限制于EX的tQCTL已是Tower困难，并在N有界树上为AExpPol完全，同时推广到多种模态逻辑。
2022-08-04 cs.LO
Interpolation in Classical Propositional Logic
Vrije Universiteit Amsterdam（阿姆斯特丹自由大学）；University of Potsdam（波茨坦大学）；University of Liverpool（利物浦大学）
研究经典命题逻辑中的插值法等相关概念，提出通过量词消去等四种方法计算插值，最后探讨了插值规模与电路复杂性的关系。
2026-07-08 cs.LO
Abductive Reasoning in Intuitionistic Propositional Logic via Theorem Synthesis
借助一个紧凑的Prolog为基础的定理证明直觉命题逻辑，我们合成的最小假设下，一个给定的公式公式成为一个定理。应用我们的合成算法，以涵盖基本的溯因推理机制后，我们合成的字面量，模仿行的真值表在经典或中间逻辑和我们的条件假设，把经典或中间逻辑的定理，在直觉逻辑。更进一步，我们推广我们的溯因推理机制，合成更有表现力的前置条件，使用最小的一组规范公式，在微积分中的任意公式可以减少，同时保持其可证明性。组织作为一个独立的文学Prolog程序，本文支持其内容的交互式探索，并确保我们的结果完全可复制。
2022-05-11 cs.LO
Towards a Coalgebraic Interpretation of Propositional Dynamic Logic
用Kripke模型解释命题动态逻辑要求解释Kripke模型的关系密切地观察模态算子的句法。这对通过随机Kripke模型解释PDL提出了重大挑战，因为程序的操作并不总是在随机关系集中有自然的对应物。我们使用重写规则来建立PDL的解释。它表明，每个程序对应于一个基本上是唯一的不可约树，这反过来又被分配一个谓词提升，作为程序的解释。本文建立并研究了这一解释。它讨论了概率模型的表达PDL和相关的属性，如逻辑和行为的等价性或双相似性的Kripke模型的一个密切相关的Hennessy-Milner类型的非动态逻辑的相应属性。
2011-09-16 cs.LO
Axiomatizing Propositional Dependence Logics
通过扩展已有的命题逻辑和模态逻辑的公理化，给出了命题依赖逻辑（PD）、模态依赖逻辑（MDL）和扩展模态依赖逻辑（EMDL）的完备的希尔伯特式公理化.此外，我们给新的标记tableau演算PD，MDL，和EMDL。我们证明了每一个标记的结石的合理性，完整性和终止。
2014-10-19 cs.LO math.LO
Complexity of validity for propositional dependence logics
研究了命题依赖逻辑、模态依赖逻辑和扩展模态依赖逻辑的有效性问题。我们证明了命题依赖逻辑的有效性问题是NEXPTIME-完全的。此外，我们建立了相应的问题的模态依赖逻辑和扩展的模态依赖逻辑是NEXPTIME困难的，在NEXPTIME^NP。
2014-08-26 cs.CC cs.LO
Labelled Sequent Calculi for Propositional Team Logics
University of Helsinki（赫尔辛基大学）；University of Amsterdam, University of Southern Denmark（阿姆斯特丹大学，南丹麦大学）；University of Bern（伯尔尼大学）；Utrecht University（乌得勒支大学）
为基于团队语义的四种逻辑（基本探究逻辑、命题直觉主义依赖逻辑及其张量析取扩展）提供了可靠且完备的带标签矢列演算，并证明了弱化、收缩和切割规则的可容许性，最后给出了带简化标签的终止证明搜索过程。
2026-07-01 cs.LO
Axiomatizations of Team Logics
在一个模块化的方法，我们提升希尔伯特式证明系统的命题，模态和一阶逻辑广义系统为各自的团队为基础的扩展。我们对Väänänen的一阶群逻辑TL的无依赖片段FO（~），命题群逻辑PTL，量化命题群逻辑QPTL，模态群逻辑MTL，以及相应的依赖、独立、包含和排除逻辑，得到了合理而完整的公理化.作为完备性证明的关键步骤，我们证明了上述逻辑在某种意义上承认从公式中消除模态和量词的语义保持性。
2018-03-26 cs.LO
New Proofs of Weak Normalization for Propositional Logic
Chennai Mathematical Institute（钦奈数学研究所）
本文提出直觉主义自然演绎弱规范化的新证明，仅处理割，提供局部规则选择收缩或归约子证明，并在Lean中形式化，给出确定性算法。
2026-10-01 cs.LO
Characterizing Crisp Simulations and Crisp Directed Simulations between Fuzzy Labeled Transition Systems by Using Fuzzy Modal Logics
我们制定和证明清晰的模拟和清晰的模糊标记的过渡系统之间的模拟模糊模态逻辑，使用一般的t-范数为基础的语义的逻辑特征。所考虑的逻辑片段的模糊命题动态逻辑与Baaz投影算子。的逻辑刻画关注保存的积极存在（分别为正）模式下的清晰模拟（分别为清晰定向模拟），以及Hennessy-Milner属性的模拟公式。
2021-09-06 cs.LO
Propositional Dynamic Logic for Message-Passing Systems
我们研究了一个双向命题动态逻辑（PDL）有限和无限消息序列图（MSC）扩展LTL和TLC-。通过这种多模态逻辑，我们可以表达事件的整个未来和过去的属性。路径表达式加强了时态逻辑的经典until算子。对于每个定义MSC语言的公式，我们构造了一个接受相同语言的通信有限状态机（CFM）。得到的CFM在公式的大小上具有大小指数。该合成问题完全一般性地解决，即，也适用于具有无界通道的MSC。CFMs和HMSC的模型检验问题对于存在有界MSC是PSPACE问题。最后，我们表明，对于PDL的交集，公式的语义不能被捕获的CFM了。
2010-09-07 cs.LO
A tableau for set-satisfiability for extended fuzzy logic BL
本文给出了一种表演算，用于求扩展的模糊逻辑BL、具有附加Baaz联结子和对合否定的模糊逻辑BL的公式的集合可满足有限集的模型，如果这样的模型存在的话。该演算是BL的Tableau演算的推广，它基于连续t-范数的分解定理。上述BL的表演算用于证明扩展BL的公式A对于所有连续t-范数是有效的，或者用于找到连续t-范数 * 和命题原子到[0，1]的赋值V，使得 *-求值V*（A）<1。本文提出的表演算使得对于扩展BL的有限公式集F和[0，1]的子集K，可以找到一个连续的t-范数 * 和命题原子到[0，1]的赋值V，使得对于所有属于F的公式A，*-求值V*（A）属于K，或者证明这样的模型不存在。
2014-07-11 cs.LO
Separation of Test-Free Propositional Dynamic Logics over Context-Free Languages
对于一类语言L，让PDL[L]是命题动态逻辑的扩展，它允许程序使用L语言而不仅仅是正则的。如果L包含非正则语言，则PDL[L]可以表示非正则属性，与纯PDL相反。对于规则的，可见的下推和确定性上下文无关的语言，各自的PDL的分离可以通过自动机理论技术来证明。然而，这些技术在自动机方面引入了非确定性。由于非确定性也是DCFL和CFL之间的区别，因此这些技术似乎不适合将PDL[DCFL]与PDL[CFL]分开。然而，这种分离是显示，但程序没有测试操作符。
2011-06-07 cs.LO
A polynomial time complete disjunction property in intuitionistic propositional logic
我们扩展了Buss和Mints（APAL 1999）和Ferrari，Fiorentini和Fiorino（LPAR 2002）的多项式时间算法，使其在直觉命题逻辑中具有多项式时间完全析取性质.
2013-12-11 cs.LO math.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
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
Epistemic extensions of combined classical and intuitionistic propositional logic
逻辑$L$是由Lewitzka [7]引入的，作为一个结合了直觉主义和经典逻辑的模态系统：$L$是CPC的保守扩展，它通过嵌入$φ\mapsto\squareφ$包含IPC的副本。在这篇文章中，我们考虑$L3$，即$L$增广与S3模态公理，定义基本的认知扩展和证明完全性w.r.t.代数语义学由此产生的逻辑结合了经典知识和信仰与直觉真理。阿特莫夫和普罗波佩斯库[1]所研究的直觉主义认识逻辑的一些认识规律反映在经典模态原理中。特别是，“直觉真理$\Rightarrow$知识$\Rightarrow$经典真理”的影响是由我们的逻辑$EL3$的定理$\squareφ\rightarrow Kφ$和$Kφ\rightarrowφ$表示的，在这里我们处理的是经典而不是直觉知识。最后，我们表明，修改我们的语义产生代数模型的直觉主义认知逻辑系统介绍了[1]。
2017-02-27 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
Counting proofs in propositional logic
本文给出了一个计算各种命题逻辑中公式的不同证明的方法。这个数字要么是整数（如果公式不可证明，则可能是0），要么是无限大。
2009-05-18 cs.LO math.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
