It was recently shown by van den Broeck at al. that the symmetric weighted
first-order model counting problem (WFOMC) for sentences of two-variable logic
FO2 is in polynomial time, while it is Sharp-P_1 complete for some
FO3-sentences. We extend the result for FO2 in two independent directions: to
sentences of the form "phi and \forall\exists^=1 psi" with phi and psi in FO2,
and to sentences formulated in the uniform one-dimensional fragment of FO, a
recently introduced extension of two-variable logic with the capacity to deal
with relation symbols of all arities. Note that the former generalizes the
extension of FO2 with a functional relation symbol. We also identify a complete
classification of first-order prefix classes according to whether WFOMC is in
polynomial time or Sharp-P_1 complete.

本研究将 van den Broeck 等人最近的对第二阶逻辑 FO2 下的对称加权一阶模型计数问题 (WFOMC) 多项式时间可解性证明，扩展到了两个独立方向：格式为 “phi 和∀∃^=1 psi” 的 FO2 句子以及在 FO 的一维均匀片段中构造的语句。同时，我们也鉴定了一阶前缀类的完整分类，以表明 WFOMC 在多项式时间或 Sharp-P_1 完备性之间的区别。

超越双变量逻辑的加权模型计数

Weighted model counting beyond two-variable logic

The uniform one-dimensional fragment of first-order logic, U1, is a formalism
that extends two-variable logic in a natural way to contexts with relations of
all arities. We survey properties of U1 and investigate its relationship to
description logics designed to accommodate higher arity relations, with
particular attention given to DLR_reg. We also define a description logic
version of a variant of U1 and prove a range of new results concerning the
expressivity of U1 and related logics.

论文探讨了一维统一片段（U1）的性质，以及 U1 与适应更高元关系的描述逻辑（DLR_reg）的关系，并定义了一个描述逻辑版本的 U1 变体，并证明了与 U1 和其他相关逻辑的表现力有关的一系列新结果。