Dixon, Lucas and Duncan, Ross (2009) Graphical reasoning in compact closed categories for quantum computation. Annals of Mathematics and Artificial Intelligence, 56 (1). pp. 23-43. ISSN 1012-2443Full text not available in this repository. (Request a copy from the Strathclyde author)
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.
|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, Electronic computers. Computer science, Computer Science(all)|
|Subjects:||Science > Mathematics > Electronic computers. Computer science|
|Department:||Faculty of Science > Computer and Information Sciences|
|Depositing user:||Pure Administrator|
|Date Deposited:||23 Oct 2013 09:27|
|Last modified:||22 Mar 2017 12:59|