Optimising Clifford circuits with Quantomatic

Andrew Fagan, Ross Duncan

Research output: Contribution to journalConference articlepeer-review

10 Citations (Scopus)
6 Downloads (Pure)


We present a system of equations between Clifford circuits, all derivable in the ZX-calculus, and formalised as rewrite rules in the Quantomatic proof assistant. By combining these rules with some non-trivial simplification procedures defined in the Quantomatic tactic language, we demonstrate the use of Quantomatic as a circuit optimisation tool. We prove that the system always reduces Clifford circuits of one or two qubits to their minimal form, and give numerical results demonstrating its performance on larger Clifford circuits.
Original languageEnglish
Pages (from-to)85-105
Number of pages21
JournalElectronic Proceedings in Theoretical Computer Science
Publication statusPublished - 29 Jan 2019
Event15th International Conference on Quantum Physics and Logic - Dalhousie University, Halifax, Canada
Duration: 3 Jun 20187 Jun 2018


  • quantum computation
  • Clifford circuits
  • Quantomatic


Dive into the research topics of 'Optimising Clifford circuits with Quantomatic'. Together they form a unique fingerprint.

Cite this