A Superposition-Based Calculus for Quantum Diagrammatic Reasoning and Beyond

TL;DR

This paper introduces a superposition calculus for quantum diagrammatic reasoning, using rooted graphs to encode circuits and a set-theoretic rewrite system to handle equations and disequations, advancing formal reasoning in quantum computing.

Contribution

It presents a novel superposition calculus tailored for quantum diagrammatic reasoning, integrating graph encoding and rewrite systems for improved formal analysis.

Findings

Developed a complete superposition calculus for quantum graphs

Enabled formal reasoning over quantum and classical circuits

Provided a set-theoretic framework for rewrite systems

Abstract

We introduce a class of rooted graphs which allows one to encode various kinds of classical or quantum circuits. We then follow a set-theoretic approach to define rewrite systems over the considered graphs and propose a new complete Superposition callculus which handles sets of formulas consisting of equations or disequations over these graphs.