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

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

Prime Implicates and Prime Implicants: From Propositional to Modal Logic

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

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…

ASPPS -一个基于命题模式的答案集程序设计的实现

aspps --- an implementation of answer-set programming with propositional schemata

我们提出了一个答案集编程范例的实现，称为aspps（答案集编程与命题模式的缩写）。系统aspps是为处理PS+理论而设计的。它包括两个基本模块。第一个模块psgrnd为PS+理论奠定了基础。第二个模块，称为aspps，是一个求解器。它计算地面PS+理论的模型。

命题逻辑程序的顺序组合

Sequential composition of propositional logic programs

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

具有命题连接词和集合的逻辑程序

Logic programs with propositional connectives and aggregates

答案集编程（ASP）是一种逻辑编程范式，可用于解决复杂的组合搜索问题。聚合是一种ASP构造，在许多应用程序中起着重要作用。定义一个令人满意的语义聚合原来是一个困难的问题，在本文中，我们提出了一个新的方法，基于聚合和命题连接词之间的类比。首先，我们扩展了答案集/稳定模型的定义，以涵盖任意命题理论;然后，我们将聚合定义为原始构造和公式的缩写。我们的集合的定义结合了表达性和简单性，它继承了许多关于嵌套表达式程序的定理，如强等价和分裂定理。

面向命题型KLM风格可废止立场逻辑

Towards Propositional KLM-Style Defeasible Standpoint Logics

本文提出可废止受限立场逻辑DRSL，整合排序解释与立场结构构建其语义，将KLM的理性闭包扩展到该逻辑并给出等价的算法与语义刻画，验证其蕴涵检验复杂度与命题KLM一致。

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

A Complete Calculus for Possibilistic Logic Programming with Fuzzy Propositional Variables

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

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

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修正算子。

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

Reasoning about Minimal Belief and Negation as Failure

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

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

Encoding Argumentation Frameworks to Propositional Logic Systems

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

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

Representation Theorems for Cumulative Propositional Dependence Logics

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

动态命题逻辑表

Tableaux for Dynamic Logic of Propositional Assignments

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

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

A Primer for Preferential Non-Monotonic Propositional Team Logics

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

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

On the Complexity of Entailment for Cumulative Propositional Dependence Logics

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

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

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的一些重要结果。

命题测度逻辑

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…

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

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公式的一些结果。

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

Decidability and Undecidability Results for Propositional Schemata

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

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

Extending Defeasibility for Propositional Standpoint Logics

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

命题可废止逻辑具有线性复杂度

Propositional Defeasible Logic has Linear Complexity

可废止逻辑是一种基于规则的非单调逻辑，它既有严格规则，又有可废止规则，而且规则上存在优先关系。我们表明，推理的命题形式的逻辑可以在线性时间。这与大多数其他命题非单调逻辑形成鲜明对比，其中推理是棘手的。

在命题论证系统中嵌入缺省逻辑

Embedding Default Logic in Propositional Argumentation Systems

在本文中，我们提出了一个转换的有限命题默认理论到所谓的命题论证系统。这种转换允许表征所有概念的赖特的默认逻辑的框架内的论证系统。因此，计算扩展，或确定是否一个给定的公式属于一个扩展或所有扩展可以回答，而不离开经典命题逻辑领域。所提出的转换是线性的默认值的数量。

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

The intuitionistic fragment of computability logic at the propositional level

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

扩充了基数约束的命题逻辑的局部搜索技术

Local-search techniques for propositional logic extended with cardinality constraints

我们研究了局部搜索可满足性求解器扩展的基数原子命题逻辑，也就是说，表达式，提供明确的方式来模型的基数集的约束。将基数原子添加到命题逻辑的语言中有助于对搜索问题进行建模，并且通常会导致简洁的编码。我们提出了两个“本地”本地搜索求解器的理论在扩展语言。我们还描述了技术，以减少问题的标准命题可满足性，并允许我们使用现成的SAT求解器。我们对这些方法进行了实验研究。我们的总体发现是，专门为扩展语言设计的本地求解器比依赖于SAT求解器的间接方法执行得更好。

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

On Forgetting in Tractable Propositional Fragments

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

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.

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

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

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

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

Solving multiagent problems can be an uphill task due to uncertainty in the environment, partial observability, and scalability of the problem at hand. Especially in an urban setting, there are more challenges since we also need to maintain safety for all users while minimizing congestion of the agents as well as their travel times. To this end, we tackle the problem of multiagent pathfinding under uncertainty and partial observability where the agents are tasked to move from their starting points to ending points while also satisfying some constraints, e.g., low congestion, and model it as a …

命题逻辑驱动的社会选择规则

Social choice rules driven by propositional logic

社会选择的几个规则进行审查，从一个统一的观点，把它们看作是根据某些特定的逻辑约束，修改信仰程度的系统的程序。在这里，信仰是一种社会属性，其程度是由赞同某一观点的人的比例来衡量的。不同的已知的规则和一些新的，得到取决于特定的约束条件。这些限制允许对不同的精致概念进行建模。特别地，我们给出了一个新的方法来处理赞成-反对-优先投票。

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

New Polynomial Classes for Logic-Based Abduction

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

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

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

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

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

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

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

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

Fuzzy Propositional Formulas under the Stable Model Semantics

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

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

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

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

原则上确定一般先验

In principle determination of generic priors

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