Computer Science – Artificial Intelligence
Scientific paper
2012-02-27
Computer Science
Artificial Intelligence
10 pages, 22 figures. Shortened and one theorem added
Scientific paper
In recent years, diagrammatic languages have been shown to be a powerful and expressive tool for reasoning about physical, logical, and semantic processes represented as morphisms in a monoidal category. In particular, categorical quantum mechanics, or "Quantum Picturalism", aims to turn concrete features of quantum theory into abstract structural properties, expressed in the form of diagrammatic identities. One way we search for these properties is to start with a concrete model (e.g. a set of linear maps or finite relations) and start composing generators into diagrams and looking for graphical identities. Naively, we could automate this procedure by enumerating all diagrams up to a given size and check for equalities, but this is intractable in practice because it produces far too many equations. Luckily, many of these identities are not primitive, but rather derivable from simpler ones. In 2010, Johansson, Dixon, and Bundy developed a technique called conjecture synthesis for automatically generating conjectured term equations to feed into an inductive theorem prover. In this extended abstract, we adapt this technique to diagrammatic theories, expressed as graph rewrite systems, and demonstrate its application by synthesising a graphical theory for studying entangled quantum states.
No associations
LandOfFree
Synthesising Graphical Theories does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Synthesising Graphical Theories, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Synthesising Graphical Theories will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-605233