As a contribution to quantitative set-theoretic inferencing, a translation is proposed of conjunctions of literals of the forms $x=y\setminus z$, $x \neq y\setminus z$, and $z =\{x\}$, where $x,y,z$ stand for variables ranging over the von Neumann universe of sets, into unquantified Boolean formulae of a rather simple conjunctive normal form. The formulae in the target language involve variables ranging over a Boolean ring of sets, along with a difference operator and relators designating equality, non-disjointness and inclusion. Moreover, the result of each translation is a conjunction of literals of the forms $x=y\setminus z$, $x\neq y\setminus z$ and of implications whose antecedents are isolated literals and whose consequents are either inclusions (strict or non-strict) between variables, or equalities between variables. Besides reflecting a simple and natural semantics, which ensures satisfiability-preservation, the proposed translation has quadratic algorithmic time-complexity, and bridges two languages both of which are known to have an NP-complete satisfiability problem.
Pegaso University（佩加索大学）；University of Padua（帕多瓦大学）；CNRS, LIPN, Université Sorbonne Paris Nord（法国国家科学研究中心，LIPN，索邦巴黎北大学）；University of Napoli ``Federico II''（那不勒斯费德里科二世大学）
A Set-Theoretic Decision Procedure for Quantifier-Free, Decidable Languages Extended with Restricted Quantifiers
设$\mathcal{L}_{\mathcal{X}}$是一阶可判定理论$\mathcal{X}$的语言。考虑一种语言$\mathcal{L}_{\mathcal{RQ}}(\mathcal{X})$，它用$\forall x \in A: ϕ$（限制全称量词，RUQ）和$\exists x \in A: ϕ$（限制存在量词，REQ）形式的公式扩展了$\mathcal{L}_{\mathcal{X}}$，其中$A$是一个有限集，$ϕ$是由$\mathcal{X}$ -公式，RUQ和REQ组成的公式。也就是说，$\mathcal{L}_{\mathcal{RQ}}(\mathcal{X})$允许嵌套的限制量词。在本文中，我们提出了一个决策过程$\mathcal{L}_{\mathcal{RQ}}(\mathcal{X})$的基础上，决策过程已经定义的有限集的布尔代数扩展的限制内涵集（$\mathcal{L}_\mathcal{RIS}$）。还介绍了作为$\{log\}$（“setlog”）工具一部分的决策程序的执行情况。该方法的实用性是通过一些来自现实世界的案例研究的例子。
Generalising unit-refutation completeness and SLUR via nested input resolution
College of Science, Swansea University（斯旺西大学理学院）
我们介绍了两个层次的子句集，SLUR_k和UC_k，基于类SLUR（单前瞻单元反驳），在1995年推出，和UC（单元反驳完成），在1994年推出。在[Annexstein et al，1995]中引入的类SLUR是子句集的类，对于该子句集，单位子句传播（由r_1表示）检测不可满足性，或者在其他情况下迭代分配，通过前瞻避免明显的错误分配，总是产生令人满意的分配。考虑如何形成基于SLUR的层次结构是很自然的。此类研究始于[Cepek et al，2012]和[Balyo et al，2012]。我们提出了我们认为的“极限层次”SLUR_k，根据推广r_1的r_k，也就是说，使用广义单位子句传播介绍[Kullmann，1999年，2004年]。在[Del Val，1994]中研究的UC类是单位反驳完备子句集类，即在任意证伪指派下，r_1都可判定其不可满足性的子句集。对于不可满足子句集F，使r_k决定F的不可满足性的最小值k正是F的“硬度”，如[Ku 99，04]中所介绍的。对于可满足的F，我们现在使用[Ansotegui et al，2008]中提到的扩展：硬度是最小的k，使得在应用任何伪造部分赋值之后，r_k确定不可满足性。类UC_k由硬度<= k的子句集给出。我们观察到UC_1恰好是UC。UC_k具有证明论性质，这是由于硬度和树分辨率之间的关系，而SLUR_k具有算法性质。r_k与k…
