Toward Entailment Checking: Explore Eigenmarking Search

TL;DR

This paper explores a quantum computing approach using eigenmarking with Grover's algorithm to improve entailment checking by distinguishing no-winner cases, potentially advancing logic reasoning methods.

Contribution

It introduces eigenmarking schemes that enhance Grover's algorithm for entailment checking, enabling better identification of no-winner scenarios in quantum logic reasoning.

Findings

Strong distinguishability achieved in all schemes

Best relative distinguishability of 19 and 53

Viable quantum mechanism for differentiating no-winner cases

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.