“全布尔函数”的一个完备性定理

在取消草地上进行总计算的直线指令序列完备性

Straight-line instruction sequence completeness for total calculation on cancellation meadows

结合程序代数与理论的草地设计导致理论的计算代数结构使用除了零测试和复制指令的指令集$\{x \Leftarrow 0, x \Leftarrow 1, x\Leftarrow -x, x\Leftarrow x^{-1}, x\Leftarrow x+y, x\Leftarrow x\cdot y\}$。本文证明了在消去草地上的全函数可以用最多5个辅助变量的直线程序来计算。一个类似的结果是获得签署草甸。

On the Complexity of Horn and Krom Fragments of Second-Order Boolean Logic

Second-order Boolean logic is a generalization of QBF, whose constant alternation fragments are known to be complete for the levels of the exponential time hierarchy. We consider two types of restriction of this logic: 1) restrictions to term constructions, 2) restrictions to the form of the Boolean matrix. Of the first sort, we consider two kinds of restrictions: firstly, disallowing nested use of proper function variables, and secondly stipulating that each function variable must appear with a fixed sequence of arguments. Of the second sort, we consider Horn, Krom, and core fragments of the …

Extending rational choice behavior: The decision problem for Boolean set theory with a choice correspondence

Given the family $P$ of all nonempty subsets of a set $U$ of alternatives, a choice over $U$ is a function $c \colon Ω\to P$ such that $Ω\subseteq P$ and $c(B) \subseteq B$ for all menus $B \in Ω$. A choice is total if $Ω= P$, and partial otherwise. In economics, an agent is considered rational whenever her choice behavior satisfies suitable axioms of consistency, which are properties quantified over menus. Here we address the following lifting problem: Given a partial choice satisfying one or more axioms of consistency, is it possible to extend it to a total choice satisfying the same axioms?…

弱长度归纳与慢增长深度布尔电路

Weak length induction and slow growing depth boolean circuits

我们定义了一个电路复杂性类LD^i的层次，其深度是Ackermann层次中函数的逆。然后，我们引入了长度归纳法的极弱形式，并构造了一个有界算术理论L^i_2，它的可证全函数恰好对应于LD^i电路可计算的函数。最后，我们证明了L^i_2与一个对应于类AC^0的较弱理论AC^0CA之间的一个非守恒性结果。我们的证明利用KPT见证定理。

仿射逼近的二元决策图

Binary Decision Diagrams for Affine Approximation

Selman和Kautz关于“知识编译”的工作建立了如何近似（加强和/或削弱）命题知识库可以用来加速查询处理，以牺牲完整性为代价。在这种经典的方法中，查询使用给定知识库的Horn过近似和欠近似，该知识库表示为合取范式（CNF）中的命题公式。除了Horn函数类之外，人们还可以想象其他布尔函数类，它们可能具有相同的目的，因为它们具有与Horn函数类似的有吸引力的演绎计算性质。事实上，Zanuttini已经提出仿射布尔函数类在知识编译中可能是有用的，并提出了仿射近似算法。由于CNF是笨拙的仿射函数，Zanuttini认为这两个集的模型表示和使用模2同余方程。在本文中，我们提出了一种基于约简有序二叉决策图（ROBDDs）的算法。这导致了一个表示，这是更紧凑的模型集，一旦我们建立了一些有用的性质仿射布尔函数，一个更有效的算法。

道义行动逻辑：一种模块化代数视角

Deontic Action Logics: A Modular Algebraic Perspective

本文从模块化代数视角重新研究 DAL，提出由两个 Boolean 代数及许可、禁止映射构成的道义行动代数，刻画 DAL 家族并引入四种变体且证明其代数完备性。

关于和与移位上的代数电路以及带可除性的存在Presburger算术

NEXP-Completeness of Existential Presburger Arithmetic with Divisibility

研究带可除性谓词的存在Presburger算术（EPAD）的可满足性问题，证明其为PP-hard，从而否定其属于NP的预期，并定义可多项式时间识别的片段MergeAbs。

基于隐式的布尔可满足性全解并行求解器

Implicant based parallel all solution solver for Boolean satisfiability

本文发展了一种并行计算求解器，用于计算由多元布尔函数定义的布尔方程组的所有满意赋值。虽然有我们已知的CNF形式的布尔公式的可满足性的求解器，但这些主要是为了确定公式的可满足性而设计的，并且没有解决找到所有满意解的问题。而可满足性问题的并行求解器的开发仍然是计算机科学尚未完成的课题。本文提出的求解器旨在用并行算法表示布尔公式的所有解，即使没有CNF形式。将所提出的算法应用于布尔函数的代数范式（ANF）。该算法的基本思想是用布尔函数的一组完整的蕴涵式来表示满足的赋值，这些蕴涵式作为布尔公式的因子。该算法主要在公式的因子稀疏（即具有变量总数的一小部分）的情况下有效。这允许一次一个地计算单个因子的一组完整的蕴涵式，并在每一步减少公式。本文还提出了一个求ANF中函数正交蕴涵的完备集的算法。该算法的一个优点是所有的解都可以用蕴涵式来表示。最后，由于在每一步的小和分布式计算，以及在独立的线程计算，本文提出的求解器预计将是有用的开发一个良好的可扩展性的并行求解器的大规模问题的布尔可满足性在大量的处理器。