Skip to main content

Quantomatic: Automated Reasoning with Open Graphs

Recent graph-based formalisms of quantum computation provide an abstract and symbolic way to represent and simulate computations. However, manual manipulation of such graphs is slow and error prone. This project employs a formalism, based on compact closed categories, that supports mechanised reasoning about such graphs. This gives a compositional account of graph rewriting that preserves the underlying categorical semantics.

Using this representation, we are developing a generic system with a fixed logical kernel that supports reasoning about models of compact closed category. A salient feature of the system is that it provides a formal and declarative account of derived results that can include ellipses-style notation. The main application is to develop a graph-based language for reasoning about quantum computation: Quantomatic.

See the Quantomatic website for more information.

Contact for Activity

Alex Merry


Past Members

Bob Coecke
Ross Duncan
(Free University of Brussels)
Alex Merry
David Quick
Vladimir Zamdzhiev

Selected Publications

View All