Combining Propositional Logic Based Decision Diagrams with Decision Making in Urban Systems

易处理命题片段中的遗忘现象

On Forgetting in Tractable Propositional Fragments

从知识库中提取与字母表子集相关的部分，这被认为是遗忘，已经引起了人工智能社区的广泛兴趣。在标准命题逻辑中，对于可满足性易处理的各种片段，仍然缺乏一种通用的遗忘算法及其面向计算的研究。本文旨在填补这一空白。在讨论了命题逻辑中遗忘的一些基本性质后，给出了CNF片段的基于分解的遗忘算法，并给出了Horn、可重命名Horn、q-Horn、Krom、DNF和CNF片段的遗忘复杂度结果.

模糊命题变量可能性逻辑规划的完全演算

A Complete Calculus for Possibilistic Logic Programming with Fuzzy Propositional Variables

本文提出了一种用于可能性不确定性推理和表示模糊知识的命题逻辑程序设计语言。公式由对（A，c）表示，其中A是多值命题，c是单位区间[0，1]中的值，它表示关于A的信念在必要性测度方面的下界。信念状态的所有多值解释的集合上的可能性分布建模。在这个框架中，（i）定义了一般不确定性逻辑的语法和语义，（ii）给出了Horn-规则子语言的一个前件式演算，并证明了它对于确定模糊命题变量从公式集合中导出的最大可能性信念度是完备的;最后，（iii）我们展示了如何计算模糊命题变量之间的部分匹配，在必要性措施的模糊集，可以包括在我们的逻辑编程系统。

命题Krom逻辑程序的最小模型与一致等价的代数刻画

Algebraic characterizations of least model and uniform equivalence of propositional Krom logic programs

该研究针对命题Krom逻辑程序，给出了其最小模型、包含关系与一致等价的代数刻画结果。

基于逻辑的溯因的新多项式类

New Polynomial Classes for Logic-Based Abduction

我们解决基于命题逻辑的溯因问题，即，根据给定的命题知识库，为给定的命题观测寻找最佳解释的问题。我们给出了一个通用的算法，投影的概念的基础上，然后我们研究的知识库和查询的表示限制，并找到新的多项式类的绑架问题。

累积命题依赖逻辑的表示定理

Representation Theorems for Cumulative Propositional Dependence Logics

本文研究了累积命题依赖逻辑和累积命题逻辑（具有团队语义）的表示定理，证明了其与特定模型的等价性，并为其他累积逻辑的表示定理提供了证明方法。

逻辑程序修改是命题修改的扩展的特征

Characterization of Logic Program Revision as an Extension of Propositional Revision

我们解决了逻辑程序的信念修正问题，即，如何将一个新逻辑程序Q合并到一个逻辑程序P中。基于SE解释的结构，Delaware等人将著名的AGM框架应用于逻辑程序（LP）修订。他们确定了LP修正的合理行为，并引入了一些特定的算子。在本文中，所有的理性LP修订运营商的建设性的特征，给出了在命题解释的顺序与特定的SE解释的一些进一步的条件。它提供了一个直观的，完整的过程，所有合理的LP修订运营商的建设，并使其语义和计算性能的理解更容易。我们特别考虑非常一般形式的逻辑程序，即，广义逻辑程序。我们表明，每一个合理的GLP修订运营商是来自一个命题的修订运营商满足原来的AGM假设。有趣的是，特定于GLP修订的进一步条件独立于GLP修订操作符所基于的提议修订操作符。利用我们的表征结果，我们将GLP修正运算符嵌入到布尔格的结构中，这使我们能够揭示适应性AGM假设中的一些潜在弱点。为了说明我们的主张，我们引入和公理化的（理性）GLP修订运营商，可以说有一个激烈的行为两个特定的类的特征。我们还考虑了逻辑程序的两种更受限制的形式，即，析取逻辑程序（DLP）和正常逻辑程序（NLP）的特征化，并使我们的特征化结果适应DLP和NLP修正算子。

动态命题逻辑表

Tableaux for Dynamic Logic of Propositional Assignments

动态命题推理逻辑（DL-PA）是近年来研究的命题动态逻辑（PDL）的一种替代方案。在DL-PA中，PDL的抽象原子程序被命题变量到真值的赋值所取代。这使得DL-PA具有PDL所没有的一些有趣的元逻辑性质，如Kleene星的可消除性、紧性和插值性。我们定义和分析tableaux演算DL-PA，并表明它符合已知的复杂性结果。

命题逻辑中的依赖：公式-公式依赖和公式遗忘--在信念更新和保守扩展中的应用

Dependence in Propositional Logic: Formula-Formula Dependence and Formula Forgetting -- Application to Belief Update and Conservative Extension

依赖性是人工智能中许多任务的重要概念。通过丢弃与任务无关的东西，可以更有效地执行任务。本文提出了命题逻辑中两个新的依赖概念：公式-公式依赖和公式遗忘。第一个是公式之间的关系，捕获公式是否依赖于另一个公式，而第二个是独立于公式返回最强结果的操作。我们还将这两个概念应用于两个著名的问题：信念更新和保守扩展。首先，我们定义了一个新的更新操作的基础上公式公式依赖。此外，我们把保守扩张归结为公式遗忘。

偏好非单调命题团队逻辑入门

A Primer for Preferential Non-Monotonic Propositional Team Logics

该文在命题团队语义框架下研究KLM风格偏好非单调推理，证明团队命题逻辑可生成累积非单调后承，给出满足System P的命题依赖逻辑偏好模型的精确刻画，并说明经典及依赖逻辑后承的非平凡偏好模型表示方法。

稳定模型语义下的模糊命题公式

Fuzzy Propositional Formulas under the Stable Model Semantics

本研究定义了模糊命题公式的稳定模型语义，推广了模糊命题逻辑与经典命题公式的稳定模型语义，支持含分级真度的动态域的可配置非单调推理，扩展了布尔稳定模型的性质并梳理了与相关方法的关系。

关于最小信念和否定为失败的推理

Reasoning about Minimal Belief and Negation as Failure

我们研究MBNF的命题片段中的推理问题，Lifschitz引入的最小信念和否定的逻辑，它可以被认为是几个非单调形式主义的统一框架，包括默认逻辑，自认知逻辑，限定，认知查询和逻辑编程。我们描述的复杂性，并提供算法的命题MBNF推理。特别是，我们表明，蕴涵命题MBNF位于第三级的多项式层次，因此，它比推理在所有上述命题形式主义的非单调推理。我们还证明了MBNF中的否定失败和摩尔的自认知逻辑中的否定内省之间的确切对应关系。

关于累积命题依赖逻辑蕴含复杂性的研究

On the Complexity of Entailment for Cumulative Propositional Dependence Logics

本文研究了累积命题依赖逻辑和累积命题逻辑（带有团队语义）的蕴含问题的复杂性，通过关系模型确定了其复杂性结果。

命题理论强等价于逻辑程序

Propositional theories are strongly equivalent to logic programs

本文给出了在回答集语义下命题理论的一个性质（一般语法称为均衡逻辑）：任何理论总是可以被重新表示为强等价的析取逻辑程序，可能在头部带有否定。我们提供了两个不同的证明这一结果：一个涉及到一个句法转换，和一个，构建一个程序从这里和那里的中间逻辑的理论的反模型。

LPC（ID）：一个扩展了归纳定义的命题逻辑顺序演算证明系统

LPC(ID): A Sequent Calculus Proof System for Propositional Logic Extended with Inductive Definitions

逻辑FO（ID）使用来自逻辑编程领域的思想来扩展具有非单调归纳定义的一阶逻辑。这种逻辑形式上扩展了逻辑程序设计、溯因逻辑程序设计和数据逻辑，从而将对这些形式主义的看法形式化为（广义）归纳定义的逻辑。本文的目标是研究FO（ID）的命题片段PC（ID）的演绎推理方法。我们引入了一个正式的证明系统的基础上的演算（根森式演绎系统），这种逻辑。由于PC（ID）是经典命题逻辑和命题归纳定义的集成，我们的推理演算证明系统集成了命题演算和定义的推理规则。我们提出了这个证明系统的可靠性和完整性，相对于PC（ID）的一个略有限制的片段。我们还提供了PC（ID）的一些复杂性结果。通过对PC（ID）证明系统的开发，有助于加深对FO（ID）证明理论基础的理解，从而研究FO（ID）的有效证明系统。

命题逻辑程序的顺序分解

Sequential decomposition of propositional logic programs

本文通过研究程序间在半群理论中著名的Green关系$\mathcal{L,R,J}$，探讨了命题逻辑程序的顺序分解问题，为迈向逻辑程序设计的代数理论迈出了进一步的一步。

答案集程序设计中的命题可满足性

Propositional satisfiability in answer-set programming

我们表明，命题逻辑及其扩展可以支持答案集编程的方式一样，稳定的逻辑编程和析取逻辑编程。为此，我们介绍了一个逻辑的基础上的逻辑命题图式和封闭世界假设的一个版本。我们称之为CWA（PS+，符号）命题图式的扩展逻辑。这种逻辑的一个重要特征是它支持对集合基数的约束进行显式建模。在本文中，我们刻画了一类问题，可以解决的有限PS+理论。我们实现了一个基于PS+逻辑的编程系统，并在PS+中设计和实现了一个处理理论的求解器。我们提出了令人鼓舞的性能结果，我们的方法-我们表明，它是有竞争力的模型，一个国家的最先进的答案集编程系统的基础上稳定的逻辑编程。

从命题逻辑到合情推理：一个唯一性定理

From Propositional Logic to Plausible Reasoning: A Uniqueness Theorem

我们考虑了将命题逻辑扩展为似然推理逻辑的问题，以及任何这样的扩展应满足的四个要求。每一个都要求经典命题逻辑的某些性质在扩展逻辑中得到保留;因此，这些要求比考克斯定理及其变体中使用的要求更简单，问题更少。与考克斯定理一样，我们的要求意味着扩展逻辑必须同构于（有限集）概率论。我们还得到了概率的具体数值，恢复了概率作为定理的经典定义，满足前提的真值分配扮演了“可能情况”的角色。"

偏好命题依赖逻辑的复杂性与性质

On the Complexity and Properties of Preferential Propositional Dependence Logic

本文研究命题依赖逻辑中的 KLM 风格偏好推理，刻画其满足 System P 的条件，分析与团队命题逻辑的差异，并给出模型表示及两种表示下的复杂性结果。

合情推理与命题合情逻辑的原理与实例

Principles and Examples of Plausible Reasoning and Propositional Plausible Logic

似是而非的推理涉及的情况，其固有的缺乏精确性是没有量化的;也就是说，没有程度或水平的精确性，因此没有使用数字，如概率。一个希望全面的原则，阐明了什么是一个形式逻辑做似是而非的推理。定义了一种新的命题逻辑，称为命题似然逻辑（PPL），并将其应用于一些重要的例子。PPL是我们所知道的唯一一个满足所有原则并对所有示例进行正确推理的非数值非单调逻辑。证明了关于PPL的一些重要结果。

命题逻辑片段中的信念合并

Belief merging within fragments of propositional logic

最近，在命题逻辑片段的框架内的信念变化得到了越来越多的关注。以往的研究主要集中在Horn片段上的信念收缩和信念修正。然而，在命题逻辑的片段的信念合并的问题一直被忽视。本文提出了一种通用的方法来定义新的合并运算符来自现有的，这样的合并结果仍然在考虑中的片段。我们的方法不仅限于霍恩片段的情况下，但适用于任何片段的命题逻辑的特点是封闭属性的模型集的公式。我们研究的逻辑属性的建议运营商的合并假设的满意度，特别考虑到基于距离的合并运营商的霍恩和克罗姆片段。

命题测度逻辑

Propositional Measure Logic

本研究提出具有概率语义的命题测度逻辑，用[0,1]区间的实值测度表示公式真度，保留经典逻辑演绎结构，证明了系统可靠性，可用于不确定性推理，并尝试解决贝叶斯网络中的一个难题。

PVS Embeddings of Propositional and Quantified Modal Logic

Modal logics allow reasoning about various modes of truth: for example, what it means for something to be possibly true, or to know that something is true as opposed to merely believing it. This report describes embeddings of propositional and quantified modal logic in the PVS verification system. The resources of PVS allow this to be done in an attractive way that supports much of the standard syntax of modal logic, while providing effective automation. The report introduces and formally specifies and verifies several standard topics in modal logic such as relationships between the standard m…

均衡逻辑中的插值与答案集规划：命题案例

Interpolation in Equilibrium Logic and Answer Set Programming: the Propositional Case

插值是经典逻辑和许多非经典逻辑的重要性质，在计算机科学和人工智能中有着重要的应用。在这里，我们研究的插值性质的命题版本的非单调系统的平衡逻辑，建立较弱或较强的形式的插值依赖于推理关系的精确解释。这些结果也产生了一种形式的插值地面逻辑程序下的回答集语义。对于析取逻辑程序，我们还研究了与变量遗忘概念密切相关的一致插值的性质。

Extending and Automating Basic Probability Theory with Propositional Computability Logic

Classical probability theory is formulated using sets. In this paper, we extend classical probability theory with propositional computability logic. Unlike other formalisms, computability logic is built on the notion of events/games, which is central to probability theory. The probability theory based on CoL is therefore useful for {\it automating} uncertainty reasoning. We describe some basic properties of this new probability theory. We also discuss a novel isomorphism between the set operations and computability logic operations.

命题逻辑公式可满足性的概率方法

A Probabilistic Approach to Satisfiability of Propositional Logic Formulae

我们提出了一个版本的WalkSAT算法，命名为BetaWalkSAT。该方法使用概率推理来偏置局部搜索算法的起始状态。Beta分布用于对文字的布尔值的置信度建模。我们的研究结果表明，提出的BetaWalkSAT算法可以优于其他的不知情的局部搜索方法复杂的布尔可满足性问题。

Linear Temporal Logic and Propositional Schemata，Back and Forth（英语：Linear Temporal Logic and Propositional Schemata，Back and Forth）

Linear Temporal Logic and Propositional Schemata, Back and Forth (extended version)

本文将著名的线性时态逻辑与作者提出的命题图式逻辑联系起来。我们证明了LTL是等价于一类图式的意义上，多项式时间减少存在从一个逻辑到其他。给出了关于复杂性的一些结论。我们报告的第一个实验和现有的实现可能的改进的后果进行了分析。

逻辑中的冗余II：2CNF与Horn命题公式

Redundancy in Logic II: 2CNF and Horn Propositional Formulae

我们报告的复杂性结果的冗余公式的2CNF形式。我们首先考虑的问题，检查冗余，并显示一些算法，略优于平凡的。然后，我们分析了相关的问题，找到非冗余等价子集（I.E.S.）一个给定的集合。循环性的概念被证明与这些问题的复杂性有关。给出了Horn公式的一些结果。

素蕴涵与素蕴涵：从命题逻辑到模态逻辑

Prime Implicates and Prime Implicants: From Propositional to Modal Logic

素蕴涵和素蕴涵已经被证明与人工智能的许多领域相关，最显著的是溯因推理和知识编译。本文的目的是研究如何将这些概念从命题逻辑适当地扩展到模态逻辑K。我们在论文的开头考虑了K的子句和术语的一些可能的定义。不同的定义进行评估方面的一组句法，语义和复杂性理论的性质特征的命题定义。然后，我们比较的定义方面的性质的概念，他们诱导的素蕴涵和素蕴涵。虽然没有定义，完美地概括了命题的概念，我们表明，确实存在一个定义，满足许多理想的性质的命题的情况下。在论文的后半部分，我们考虑了所选定义的计算性质。为此，我们提供了健全的和完整的算法生成和识别总理牵连，我们表明总理牵连识别任务是PSPACE完成。我们还证明了上界和下界的大小和数量的素数蕴涵。虽然本文的重点是逻辑K，我们所有的结果同样适用于多模态K和描述逻辑ALC中的概念表达式。

命题逻辑程序的顺序组合

Sequential composition of propositional logic programs

本文研究命题逻辑程序的顺序组合与分解，证明无环程序可分解为单规则程序，并利用组合表示直接后果算子以计算最小模型，从而弥合语法与语义的鸿沟。

命题模式的可判定性和不可判定性结果

Decidability and Undecidability Results for Propositional Schemata

我们定义了一个逻辑的命题公式图式添加到语法的命题逻辑索引命题和迭代连接词范围内的算术变量参数化的区间。可满足性问题是不可判定的，这个新的逻辑，但我们引入了一个非常一般的类的模式，称为有界线性，这个问题变得可判定。这个结果是通过减少到一个特定的类称为定期的模式，我们提供了一个健全的和完整的终止证明过程。这种模式演算允许一个捕获证明模式对应于一个大类的命题逻辑中指定的问题。我们还表明，可满足性问题再次成为不可判定的轻微扩展这一类，从而表明，有界线性模式代表了一个很好的妥协之间的表达性和可判定性。

扩展命题立场逻辑的可废止性

Extending Defeasibility for Propositional Standpoint Logics

本文通过整合多种可废止性概念与立场逻辑，提出了一种新的命题立场逻辑可废止版本，支持在蕴涵、模态算子和立场锐化层面表达可废止性，并提供了偏好语义、可靠完备的tableau演算及PSpace复杂度证明。

可计算性逻辑在命题层次上的直观片段

The intuitionistic fragment of computability logic at the propositional level

从可计算性逻辑的语义出发，给出命题直觉演算的可靠性和完备性证明。后者将公式解释为交互式计算问题，形式化为机器与其环境之间的游戏。直觉主义蕴涵被理解为在最弱的可能性-因此最自然-意义上的算法还原，析取和合取作为问题的确定性选择组合（析取=机器的选择，合取=环境的选择），而“荒谬”作为普遍力量的计算问题。请访问http://www.cis.upenn.edu/~giorgi/cl.html以获得关于可计算性逻辑的全面在线资源。

将论证框架编码到命题逻辑系统

Encoding Argumentation Frameworks to Propositional Logic Systems

本文将论证框架编码从二值命题逻辑推广到三值和模糊命题逻辑，通过正规编码和正则编码建立Dung经典语义、Gabbay实数等式语义与多种编码语义的对应关系，并提出新的模糊编码语义，为构造新论证语义提供框架。

Explainability via Short Formulas: the Case of Propositional Logic with Implementation

We conceptualize explainability in terms of logic and formula size, giving a number of related definitions of explainability in a very general setting. Our main interest is the so-called special explanation problem which aims to explain the truth value of an input formula in an input model. The explanation is a formula of minimal size that (1) agrees with the input formula on the input model and (2) transmits the involved truth value to the input formula globally, i.e., on every model. As an important example case, we study propositional logic in this setting and show that the special explaina…

LogicLearner：命题逻辑证明引导练习工具

LogicLearner: A Tool for the Guided Practice of Propositional Logic Proofs

LogicLearner是一款Web应用，通过逐步界面和自动求解器提供命题逻辑证明的引导练习，试点反馈积极，是唯一提供端到端无评判反馈的练习工具。

弯曲布尔逻辑：命题逻辑的上下文推广及其算法推论

Curved Boolean Logic: A Contextual Generalization of Propositional Logic with Algorithmic Consequences

弯曲布尔逻辑（CBL）通过引入局部真值赋值推广命题逻辑，提出上下文感知证明演算及CBL-SAT复杂度分析，提供操作算子与噪声建模，并探讨其与SAT/CSP及大语言模型稳定性的联系。

基于神经机器翻译的直觉命题逻辑证明综合

Towards Proof Synthesis Guided by Neural Machine Translation for Intuitionistic Propositional Logic

受深度神经网络（DNN）在机器学习中的最新发展的启发，我们探索了它们在PL相关主题中的应用。本文是实现这一目标的第一步;我们提出了一种无否定命题逻辑的证明合成方法，其中我们使用DNN来获得证明搜索的指南。这个想法是把证明综合问题看作是从命题到其证明的转换。我们训练seq 2seq，这是神经机器翻译中的一个流行网络，因此它生成一个编码为给定命题的$λ$ -项的证明。我们实现了整个框架，并根据经验观察到，生成的证明项在AST的树编辑距离方面接近于正确的证明。这一观察结果证明了使用经过训练的seq 2seq模型的输出作为证据搜索的指导是合理的。

原则上确定一般先验

In principle determination of generic priors

作为扩展逻辑的概率论是完备的，使得基本上任何概率都可以被确定。这是通过考虑命题逻辑（相对于谓词逻辑）作为句法足够和强加一个对称命题逻辑。它表明如何的概念的“可能性”和“属性”可能是充分表示在命题逻辑，使1）的原则无差异下降，并成为本质上组合和2）一个可以适当地表示假设，其中一个假设有一个空间的可能性，但不承担空间的大小。