Abstract
| Language | English |
|---|---|
| Pages | 23-43 |
| Number of pages | 20 |
| Journal | Annals of Mathematics and Artificial Intelligence |
| Volume | 56 |
| Issue number | 1 |
| DOIs | |
| Publication status | Published - May 2009 |
Fingerprint
Keywords
- graphical reasoning
- compact
- closed categories
- quantum computation
- 05C20
- 81P68
- graph rewriting
- quantum computing
- categorical logic
- interactive theorem proving
- graphical calculi
- ellipses notation
- 03G30
- 18C10
- 03G12
Cite this
}
Graphical reasoning in compact closed categories for quantum computation. / Dixon, Lucas; Duncan, Ross.
In: Annals of Mathematics and Artificial Intelligence, Vol. 56, No. 1, 05.2009, p. 23-43.Research output: Contribution to journal › Article
TY - JOUR
T1 - Graphical reasoning in compact closed categories for quantum computation
AU - Dixon, Lucas
AU - Duncan, Ross
PY - 2009/5
Y1 - 2009/5
N2 - Compact closed categories provide a foundational formalism for a variety of important domains, including quantum computation. These categories have a natural visualisation as a form of graphs. We present a formalism for equational reasoning about such graphs and develop this into a generic proof system with a fixed logical kernel for equational reasoning about compact closed categories. Automating this reasoning process is motivated by the slow and error prone nature of manual graph manipulation. A salient feature of our system is that it provides a formal and declarative account of derived results that can include `ellipses'-style notation. We illustrate the framework by instantiating it for a graphical language of quantum computation and show how this can be used to perform symbolic computation.
AB - Compact closed categories provide a foundational formalism for a variety of important domains, including quantum computation. These categories have a natural visualisation as a form of graphs. We present a formalism for equational reasoning about such graphs and develop this into a generic proof system with a fixed logical kernel for equational reasoning about compact closed categories. Automating this reasoning process is motivated by the slow and error prone nature of manual graph manipulation. A salient feature of our system is that it provides a formal and declarative account of derived results that can include `ellipses'-style notation. We illustrate the framework by instantiating it for a graphical language of quantum computation and show how this can be used to perform symbolic computation.
KW - graphical reasoning
KW - compact
KW - closed categories
KW - quantum computation
KW - 05C20
KW - 81P68
KW - graph rewriting
KW - quantum computing
KW - categorical logic
KW - interactive theorem proving
KW - graphical calculi
KW - ellipses notation
KW - 03G30
KW - 18C10
KW - 03G12
U2 - 10.1007/s10472-009-9141-x
DO - 10.1007/s10472-009-9141-x
M3 - Article
VL - 56
SP - 23
EP - 43
JO - Annals of Mathematics and Artificial Intelligence
T2 - Annals of Mathematics and Artificial Intelligence
JF - Annals of Mathematics and Artificial Intelligence
SN - 1012-2443
IS - 1
ER -