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)


SQuInT Chief Organizer
Akimasa Miyake, Associate Professor

SQuInT Co-Organizer
Brian Smith, Associate Professor UO

SQuInT Program Committee
Postdoctoral Fellows:
Markus Allgaier (UO OMQ)
Sayonee Ray (UNM CQuIC)
Pablo Poggi (UNM CQuIC)
Valerian Thiel (UO OMQ)

SQuInT Event Co-Organizers (Oregon)
Jorjie Arden
Holly Lynn

SQuInT Event Administrator (Oregon)
Brandy Todd

SQuInT Administrator (CQuIC)
Gloria Cordova
505 277-1850

SQuInT Founder
Ivan Deutsch, Regents' Professor, CQuIC Director

Tweet About SQuInT 2020!