Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
History and Prospects for First-Order Automated Deduction Read chapter Read first chapter

2015 | OriginalPaper | Chapter

Quantomatic: A Proof Assistant for Diagrammatic Reasoning

Authors : Aleks Kissinger, Vladimir Zamdzhiev

Published in: Automated Deduction - CADE-25

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

Monoidal algebraic structures consist of operations that can have multiple outputs as well as multiple inputs, which have applications in many areas including categorical algebra, programming language semantics, representation theory, algebraic quantum information, and quantum groups. String diagrams provide a convenient graphical syntax for reasoning formally about such structures, while avoiding many of the technical challenges of a term-based approach. Quantomatic is a tool that supports the (semi-)automatic construction of equational proofs using string diagrams. We briefly outline the theoretical basis of Quantomatic’s rewriting engine, then give an overview of the core features and architecture and give a simple example project that computes normal forms for commutative bialgebras.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter Quantifier-Free Equational Logic and Prime Implicate Generation
next chapter Cooperating Proof Attempts
Footnotes
1
Non-linear term rewriting can be encoded by introducing special ‘copy’ and ‘delete’ nodes which obey certain naturality conditions. However, when \(\otimes \ne \times \), these don’t exist in general.
 
Literature
1.
Abramsky, S., Coecke, B.: A categorical semantics of quantum protocols. In: LICS 2004, pp. 415–425. IEEE Computer Society (2004)
2.
3.
Bonchi, F., Sobociński, P., Zanasi, F.: Interacting bialgebras are frobenius. In: Muscholl, A. (ed.) FOSSACS 2014 (ETAPS). LNCS, vol. 8412, pp. 351–365. Springer, Heidelberg (2014) CrossRef
4.
Bonchi, F., Sobociński, P., Zanasi, F.: Full abstraction for signal flow graphs. In: Principles of Programming Languages, POPL 2015 (2015)
5.
Clark, S., Coecke, B., Sadrzadeh, M.: Mathematical foundations for a compositional distributed model of meaning. Linguist. Anal. 36, 1–4 (2011)
6.
Coecke, B., Duncan, R.: Interacting quantum observables: categorical algebra and diagrammatics. New J. Phys. 13(4), 043016 (2011)MathSciNetCrossRef
7.
Danos, V., Feret, J., Fontana, W., Harmer, R., Krivine, J.: Abstracting the differential semantics of rule-based models: exact and automated model reduction. In: LICS (2010)
8.
9.
Duncan, R., Lucas, M.: Verifying the steane code with quantomatic. In: Quantum Physics and Logic, vol. 2013 (2013)
10.
Duncan, R., Perdrix, S.: Rewriting measurement-based quantum computations with generalised flow. In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F., Spirakis, P.G. (eds.) ICALP 2010. LNCS, vol. 6199, pp. 285–296. Springer, Heidelberg (2010) CrossRef
11.
Grefenstette, E., Sadrzadeh, M.: Experimental support for a categorical compositional distributional model of meaning. In: Proceedings of the Conference on Empirical Methods in Natural Language Processing (2011)
12.
Grov, G., Kissinger, A., Lin, Y.: Tinker, tailor, solver, proof. In: UITP (2014)
13.
Hillebrand, A.: Quantum protocols involving multiparticle entanglement and their representations in the ZX-calculus. Master’s thesis, Oxford University (2011)
14.
15.
16.
Kissinger, A.: Pictures of Processes: Automated Graph Rewriting for Monoidal Categories and Applications to Quantum Computing. Ph.d. thesis, Oxford (2012)
17.
18.
Kissinger, A., Merry, A., Soloviev, M.: Pattern graph rewrite systems. In: Proceedings of DCM (2012)
19.
Kissinger, A., Quick, D.: Tensors, !-graphs, and non-commutative quantum structures. In: QPL 2014, vol. 172 of EPTCS, pp. 56–67 (2014)
20.
Kissinger, A., Zamdzhiev, V.: !-graphs with trivial overlap are context-free. In: Proceedings Graphs as Models, GaM 2015, London, UK, pp. 11–12 , April 2015
21.
Melliès, P.-A.: Local states in string diagrams. In: Dowek, G. (ed.) RTA-TLCA 2014. LNCS, vol. 8560, pp. 334–348. Springer, Heidelberg (2014)
22.
Merry, A.: Reasoning with !-graphs. Ph.d. thesis, Oxford University (2013)
23.
Michaelson, G., Grov, G.: Reasoning about multi-process systems with the box calculus. In: Zsók, V., Horváth, Z., Plasmeijer, R. (eds.) CEFP. LNCS, vol. 7241, pp. 279–338. Springer, Heidelberg (2012) CrossRef
24.
Penrose, R.: Applications of negative dimensional tensors. In: Dowling, T.A., Penrose, R. (eds.) Combinatorial Mathematics and its Applications, pp. 221–244. Academic Press, San Diego (1971)
25.
Rensink, A.: The GROOVE simulator: a tool for state space generation. In: Pfaltz, J.L., Nagl, M., Böhlen, B. (eds.) AGTIVE 2003. LNCS, vol. 3062, pp. 479–485. Springer, Heidelberg (2004) CrossRef
26.
Schürr, A.: PROGRESS: a VHL-language based on graph grammars. In: Ehrig, H., Kreoswki, H.-J., Rozenberg, G. (eds.) Graph Grammars and Their Application to Computer Science. LNCS, vol. 532. Springer, Heidelberg (1991)
27.
Sobociński, P.: Representations of petri net interactions. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 554–568. Springer, Heidelberg (2010) CrossRef
28.
Taentzer, G.: AGG: A graph transformation environment for modeling and validation of software. In: Pfaltz, J.L., Nagl, M., Böhlen, B. (eds.) AGTIVE 2003. LNCS, vol. 3062, pp. 446–453. Springer, Heidelberg (2004) CrossRef
Metadata
Title
Quantomatic: A Proof Assistant for Diagrammatic Reasoning
Authors
Aleks Kissinger
Vladimir Zamdzhiev
Copyright Year
2015
Book
Automated Deduction - CADE-25

Print ISBN: 978-3-319-21400-9

Electronic ISBN: 978-3-319-21401-6

Copyright Year: 2015

DOI
https://doi.org/10.1007/978-3-319-21401-6_22

Premium Partner

    Image Credits