Southwest Quantum Information and Technology

A quantum algorithm for verifying first-order logic

Presenting Author: Daniel Briseno, Chapman University
Contributing Author(s): Justin Dressel, M. Andrew Moshier, Olivia Wissa

The verification of first-order-logic formulas is a question of particular importance in computer science, since an efficient algorithm for doing so would have important consequences for automated theorem proving, the 3-SAT problem and model checking. We take inspiration from a nested version of Grover's quantum database search algorithm and propose a similar nested algorithm to address first-order logic verification. Grover's search scales in time as O(√N) in the size N of the database, while we expect our proposed algorithm to scale similarly as O(〖√N〗^n) where n is the number of quantifiers in the logic formula with N terms.

(Session : from 5:00pm - 7:00pm)