Title: Toward Entailment Checking: Explore Eigenmarking Search Show Chinese title

Title: 迈向蕴涵检查：探索特征标记搜索

Abstract: Logic entailment is essential to reasoning, but entailment checking has the worst-case complexity of an exponential of the variable size. With recent development, quantum computing when mature may allow an effective approach for various combinatorial problems, including entailment checking. Grover algorithm uses Grover operations, selective phase inversion and amplitude amplification to address a search over unstructured data with quadratic improvement from a classical method. Its original form is intended to a single-winner scenario: exactly one match is promised. Its extension to multiple-winner cases employs probabilistic control over a number of applications of Grover operations, while a no-winner case is handled by time-out. Our study explores various schemes of ``eigenmarking'' approach. Still relying on Grover operations, but the approach introduces additional qubits to tag the eigenstates. The tagged eigenstates are to facilitate an interpretation of the measured results and enhance identification of a no-winner case (related to no logic violation in entailment context). Our investigation experiments three variations of eigenmarking on a two-qubit system using an IBM Aer simulator. The results show strong distinguishability in all schemes with the best relative distinguishabilities of 19 and 53 in worst case and in average case, respectively. Our findings reveal a viable quantum mechanism to differentiate a no-winner case from other scenarios, which could play a pivot role in entailment checking and logic reasoning in general. Show Chinese abstract

Abstract: 逻辑蕴涵对于推理至关重要，但蕴涵检查在最坏情况下的复杂度是变量规模的指数级。随着最近的发展，成熟的量子计算可能会为各种组合问题提供一种有效的解决方法，包括蕴涵检查。 Grover算法使用Grover操作、选择性相位反转和振幅放大来处理无结构数据的搜索，与经典方法相比具有平方级别的改进。其原始形式适用于单赢家场景：保证只有一个匹配项。将其扩展到多赢家情况时，通过控制Grover操作的应用次数来实现概率控制，而无赢家情况则通过超时来处理。 我们的研究探索了多种“特征标记”方法。尽管仍然依赖于Grover操作，但该方法引入了额外的量子比特来标记特征态。这些标记的特征态有助于解释测量结果，并增强对无赢家情况（在蕴涵上下文中与无逻辑矛盾相关）的识别。 我们在一个两量子比特系统上使用IBM Aer模拟器对特征标记的三种变体进行了实验研究。结果显示，在所有方案中均表现出强烈的可区分性，最坏情况下和平均情况下的最佳相对可区分性分别为19和53。我们的发现揭示了一种可行的量子机制，可以区分无赢家情况与其他情况，这可能在蕴涵检查和一般逻辑推理中发挥关键作用。