{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:20:02Z","timestamp":1750220402388,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":43,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,9,6]],"date-time":"2021-09-06T00:00:00Z","timestamp":1630886400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2021,9,6]]},"DOI":"10.1145\/3479394.3479405","type":"proceedings-article","created":{"date-parts":[[2021,10,7]],"date-time":"2021-10-07T22:23:02Z","timestamp":1633645382000},"page":"1-13","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["A Superposition-Based Calculus for Diagrammatic Reasoning"],"prefix":"10.1145","author":[{"given":"Rachid","family":"Echahed","sequence":"first","affiliation":[{"name":"Univ. Grenoble Alpes, LIG, CNRS\/GINP, France"}]},{"given":"Mnacho","family":"Echenim","sequence":"additional","affiliation":[{"name":"Univ. Grenoble Alpes, LIG, CNRS\/GINP, France"}]},{"given":"Mehdi","family":"Mhalla","sequence":"additional","affiliation":[{"name":"Univ. Grenoble Alpes, LIG, CNRS\/GINP, France"}]},{"given":"Nicolas","family":"Peltier","sequence":"additional","affiliation":[{"name":"Univ. Grenoble Alpes, LIG, CNRS\/GINP, France"}]}],"member":"320","published-online":{"date-parts":[[2021,10,7]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/4.3.217"},{"key":"e_1_3_2_1_2_1","volume-title":"15th Annual Conference of Quantum Physics and Logic (QPL). arXiv:1805","author":"Backens Miriam","year":"2018","unstructured":"Miriam Backens and Aleks Kissinger . 2018 . ZH: A complete graphical calculus for quantum computations involving classical non-linearity . In 15th Annual Conference of Quantum Physics and Logic (QPL). arXiv:1805 .02175. Miriam Backens and Aleks Kissinger. 2018. ZH: A complete graphical calculus for quantum computations involving classical non-linearity. In 15th Annual Conference of Quantum Physics and Logic (QPL). arXiv:1805.02175."},{"volume-title":"Handbook of Theoretical Computer Science","author":"Barendregt Hendrik\u00a0Pieter","key":"e_1_3_2_1_3_1","unstructured":"Hendrik\u00a0Pieter Barendregt . 1990. Functional Programming and Lambda Calculus . In Handbook of Theoretical Computer Science , Volume B: Formal Models and Semantics, Jan van Leeuwen (Ed.). Elsevier and MIT Press, 321\u2013 363 . https:\/\/doi.org\/10.1016\/b978-0-444-88074-1.50012-3 10.1016\/b978-0-444-88074-1.50012-3 Hendrik\u00a0Pieter Barendregt. 1990. Functional Programming and Lambda Calculus. In Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, Jan van Leeuwen (Ed.). Elsevier and MIT Press, 321\u2013363. https:\/\/doi.org\/10.1016\/b978-0-444-88074-1.50012-3"},{"volume-title":"PARLE, Parallel Architectures and Languages Europe, Volume II: Parallel Languages(LNCS, Vol.\u00a0259)","author":"Barendregt Hendrik\u00a0Pieter","key":"e_1_3_2_1_4_1","unstructured":"Hendrik\u00a0Pieter Barendregt , Marko C. J.\u00a0D. van Eekelen , John R.\u00a0W. Glauert , Richard Kennaway , Marinus\u00a0 J. Plasmeijer , and M.\u00a0 Ronan Sleep . 1987. Term Graph Rewriting . In PARLE, Parallel Architectures and Languages Europe, Volume II: Parallel Languages(LNCS, Vol.\u00a0259) . Springer , 141\u2013158. https:\/\/doi.org\/10.1007\/3-540-17945-3_8 10.1007\/3-540-17945-3_8 Hendrik\u00a0Pieter Barendregt, Marko C. J.\u00a0D. van Eekelen, John R.\u00a0W. Glauert, Richard Kennaway, Marinus\u00a0J. Plasmeijer, and M.\u00a0Ronan Sleep. 1987. Term Graph Rewriting. In PARLE, Parallel Architectures and Languages Europe, Volume II: Parallel Languages(LNCS, Vol.\u00a0259). Springer, 141\u2013158. https:\/\/doi.org\/10.1007\/3-540-17945-3_8"},{"key":"e_1_3_2_1_5_1","volume-title":"USA","author":"Baumgartner Peter","year":"2013","unstructured":"Peter Baumgartner and Uwe Waldmann . 2013 . Hierarchic Superposition with Weak Abstraction. In Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction, Lake Placid, NY , USA , June 9-14, 2013. Proceedings(Lecture Notes in Computer Science, Vol.\u00a07898), Maria\u00a0Paola Bonacina (Ed.). Springer, 39\u201357. https:\/\/doi.org\/10.1007\/978-3-642-38574-2_3 10.1007\/978-3-642-38574-2_3 Peter Baumgartner and Uwe Waldmann. 2013. Hierarchic Superposition with Weak Abstraction. In Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings(Lecture Notes in Computer Science, Vol.\u00a07898), Maria\u00a0Paola Bonacina (Ed.). Springer, 39\u201357. https:\/\/doi.org\/10.1007\/978-3-642-38574-2_3"},{"key":"e_1_3_2_1_6_1","volume-title":"Superposition for Lambda-Free Higher-Order Logic. Log. Methods Comput. Sci. 17, 2","author":"Bentkamp Alexander","year":"2021","unstructured":"Alexander Bentkamp , Jasmin Blanchette , Simon Cruanes , and Uwe Waldmann . 2021. Superposition for Lambda-Free Higher-Order Logic. Log. Methods Comput. Sci. 17, 2 ( 2021 ). https:\/\/lmcs.episciences.org\/7349 Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, and Uwe Waldmann. 2021. Superposition for Lambda-Free Higher-Order Logic. Log. Methods Comput. Sci. 17, 2 (2021). https:\/\/lmcs.episciences.org\/7349"},{"key":"e_1_3_2_1_7_1","volume-title":"IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings(Lecture Notes in Computer Science, Vol.\u00a010900)","author":"Blanchette Jasmin\u00a0Christian","year":"2018","unstructured":"Jasmin\u00a0Christian Blanchette , Nicolas Peltier , and Simon Robillard . 2018 . Superposition with Datatypes and Codatatypes. In Automated Reasoning - 9th International Joint Conference , IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings(Lecture Notes in Computer Science, Vol.\u00a010900) , Didier Galmiche, Stephan Schulz, and Roberto Sebastiani (Eds.). Springer, 370\u2013387. https:\/\/doi.org\/10.1007\/978-3-319-94205-6_25 10.1007\/978-3-319-94205-6_25 Jasmin\u00a0Christian Blanchette, Nicolas Peltier, and Simon Robillard. 2018. Superposition with Datatypes and Codatatypes. In Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings(Lecture Notes in Computer Science, Vol.\u00a010900), Didier Galmiche, Stephan Schulz, and Roberto Sebastiani (Eds.). Springer, 370\u2013387. https:\/\/doi.org\/10.1007\/978-3-319-94205-6_25"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_6"},{"key":"e_1_3_2_1_9_1","volume-title":"Proving Correctness of Logically Decorated Graph Rewriting Systems. In 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016","author":"Brenas Jon\u00a0Ha\u00ebl","year":"2016","unstructured":"Jon\u00a0Ha\u00ebl Brenas , Rachid Echahed , and Martin Strecker . 2016 . Proving Correctness of Logically Decorated Graph Rewriting Systems. In 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016 , June 22-26, 2016, Porto, Portugal(LIPIcs, Vol.\u00a052). Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 14:1\u201314:15. https:\/\/doi.org\/10.4230\/LIPIcs.FSCD. 2016.14 10.4230\/LIPIcs.FSCD.2016.14 Jon\u00a0Ha\u00ebl Brenas, Rachid Echahed, and Martin Strecker. 2016. Proving Correctness of Logically Decorated Graph Rewriting Systems. In 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016, June 22-26, 2016, Porto, Portugal(LIPIcs, Vol.\u00a052). Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 14:1\u201314:15. https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2016.14"},{"key":"e_1_3_2_1_10_1","unstructured":"Titouan Carette Dominic Horsman and Simon Perdrix. 2019. SZX-calculus: Scalable graphical quantum reasoning. arXiv preprint arXiv:1905.00041(2019).  Titouan Carette Dominic Horsman and Simon Perdrix. 2019. SZX-calculus: Scalable graphical quantum reasoning. arXiv preprint arXiv:1905.00041(2019)."},{"key":"e_1_3_2_1_11_1","unstructured":"Alexandre Cl\u00e9ment and Simon Perdrix. 2020. PBS-calculus: A Graphical Language for Quantum-Controlled Computations. arXiv preprint arXiv:2002.09387(2020).  Alexandre Cl\u00e9ment and Simon Perdrix. 2020. PBS-calculus: A Graphical Language for Quantum-Controlled Computations. arXiv preprint arXiv:2002.09387(2020)."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1088\/1367-2630\/13\/4\/043016"},{"key":"e_1_3_2_1_13_1","volume-title":"International Workshop on Reversible Computation. Springer, 1\u201313","author":"Coecke Bob","year":"2012","unstructured":"Bob Coecke and Ross Duncan . 2012 . Tutorial: Graphical calculus for quantum circuits . In International Workshop on Reversible Computation. Springer, 1\u201313 . Bob Coecke and Ross Duncan. 2012. Tutorial: Graphical calculus for quantum circuits. In International Workshop on Reversible Computation. Springer, 1\u201313."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2018.12.003"},{"key":"e_1_3_2_1_15_1","volume-title":"ICGT 2006(LNCS, Vol.\u00a04178)","author":"Corradini Andrea","year":"2006","unstructured":"Andrea Corradini , Tobias Heindel , Frank Hermann , and Barbara K\u00f6nig . 2006 . Sesqui-Pushout Rewriting. In Graph Transformations , ICGT 2006(LNCS, Vol.\u00a04178) . Springer, 30\u201345. https:\/\/doi.org\/10.1007\/1 1841883_4 10.1007\/11841883_4 Andrea Corradini, Tobias Heindel, Frank Hermann, and Barbara K\u00f6nig. 2006. Sesqui-Pushout Rewriting. In Graph Transformations, ICGT 2006(LNCS, Vol.\u00a04178). Springer, 30\u201345. https:\/\/doi.org\/10.1007\/11841883_4"},{"key":"e_1_3_2_1_16_1","volume-title":"Programming and symbolic computation in Maude. J. Log. Algebraic Methods Program. 110","author":"Dur\u00e1n Francisco","year":"2020","unstructured":"Francisco Dur\u00e1n , Steven Eker , Santiago Escobar , Narciso Mart\u00ed-Oliet , Jos\u00e9 Meseguer , Rub\u00e9n Rubio , and Carolyn\u00a0 L. Talcott . 2020. Programming and symbolic computation in Maude. J. Log. Algebraic Methods Program. 110 ( 2020 ). https:\/\/doi.org\/10.1016\/j.jlamp.2019.100497 10.1016\/j.jlamp.2019.100497 Francisco Dur\u00e1n, Steven Eker, Santiago Escobar, Narciso Mart\u00ed-Oliet, Jos\u00e9 Meseguer, Rub\u00e9n Rubio, and Carolyn\u00a0L. Talcott. 2020. Programming and symbolic computation in Maude. J. Log. Algebraic Methods Program. 110 (2020). https:\/\/doi.org\/10.1016\/j.jlamp.2019.100497"},{"key":"e_1_3_2_1_17_1","volume-title":"ICGT 2008(LNCS, Vol.\u00a05214)","author":"Echahed Rachid","year":"2008","unstructured":"Rachid Echahed . 2008 . Inductively Sequential Term-Graph Rewrite Systems. In Graph Transformations , ICGT 2008(LNCS, Vol.\u00a05214) . Springer, 84\u201398. https:\/\/doi.org\/10.1007\/978-3-540-87405-8_7 10.1007\/978-3-540-87405-8_7 Rachid Echahed. 2008. Inductively Sequential Term-Graph Rewrite Systems. In Graph Transformations, ICGT 2008(LNCS, Vol.\u00a05214). Springer, 84\u201398. https:\/\/doi.org\/10.1007\/978-3-540-87405-8_7"},{"volume-title":"Fundamentals of Algebraic Graph Transformation","author":"Ehrig Hartmut","key":"e_1_3_2_1_18_1","unstructured":"Hartmut Ehrig , Karsten Ehrig , Ulrike Prange , and Gabriele Taentzer . 2006. Fundamentals of Algebraic Graph Transformation . Springer . https:\/\/doi.org\/10.1007\/3-540-31188-2 10.1007\/3-540-31188-2 Hartmut Ehrig, Karsten Ehrig, Ulrike Prange, and Gabriele Taentzer. 2006. Fundamentals of Algebraic Graph Transformation. Springer. https:\/\/doi.org\/10.1007\/3-540-31188-2"},{"key":"e_1_3_2_1_19_1","volume-title":"Graph-Grammars: An Algebraic Approach. In 14th Annual Symposium on Switching and Automata Theory","author":"Ehrig Hartmut","year":"1973","unstructured":"Hartmut Ehrig , Michael Pfender , and Hans\u00a0J\u00fcrgen Schneider . 1973 . Graph-Grammars: An Algebraic Approach. In 14th Annual Symposium on Switching and Automata Theory , Iowa City, Iowa, USA , October 15-17, 1973. 167\u2013180. https:\/\/doi.org\/10.1109\/SWAT.1973.11 10.1109\/SWAT.1973.11 Hartmut Ehrig, Michael Pfender, and Hans\u00a0J\u00fcrgen Schneider. 1973. Graph-Grammars: An Algebraic Approach. In 14th Annual Symposium on Switching and Automata Theory, Iowa City, Iowa, USA, October 15-17, 1973. 167\u2013180. https:\/\/doi.org\/10.1109\/SWAT.1973.11"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"crossref","unstructured":"Joost Engelfriet and Grzegorz Rozenberg. 1997. Node Replacement Graph Grammars. In Handbook of Graph Grammars and Computing by Graph Transformations Volume 1: Foundations. World Scientific 1\u201394.  Joost Engelfriet and Grzegorz Rozenberg. 1997. Node Replacement Graph Grammars. In Handbook of Graph Grammars and Computing by Graph Transformations Volume 1: Foundations. World Scientific 1\u201394.","DOI":"10.1142\/9789812384720_0001"},{"key":"e_1_3_2_1_21_1","unstructured":"Jonathan Gorard Manojna Namuduri and Xerxes\u00a0D. Arsiwalla. 2021. ZX-Calculus and Extended Wolfram Model Systems II: Fast Diagrammatic Reasoning with an Application to Quantum Circuit Simplification. CoRR abs\/2103.15820(2021). arxiv:2103.15820https:\/\/arxiv.org\/abs\/2103.15820  Jonathan Gorard Manojna Namuduri and Xerxes\u00a0D. Arsiwalla. 2021. ZX-Calculus and Extended Wolfram Model Systems II: Fast Diagrammatic Reasoning with an Application to Quantum Circuit Simplification. CoRR abs\/2103.15820(2021). arxiv:2103.15820https:\/\/arxiv.org\/abs\/2103.15820"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"crossref","unstructured":"A. Habel K-H. Pennemann and A. Rensink. 2006. Weakest Preconditions for High-Level Programs. In Graph Transformations (ICGT) Natal Brazil(Natal Brazil) (LNCS Vol.\u00a04178). Springer Verlag Berlin 445\u2013460.  A. Habel K-H. Pennemann and A. Rensink. 2006. Weakest Preconditions for High-Level Programs. In Graph Transformations (ICGT) Natal Brazil(Natal Brazil) (LNCS Vol.\u00a04178). Springer Verlag Berlin 445\u2013460.","DOI":"10.1007\/11841883_31"},{"key":"e_1_3_2_1_23_1","volume-title":"The algebra of entanglement and the geometry of composition. PhD","author":"Hadzihasanovic Amar","year":"2017","unstructured":"Amar Hadzihasanovic . 2017. The algebra of entanglement and the geometry of composition. PhD , University of Oxford , arXiv:1709.08086( 2017 ). Amar Hadzihasanovic. 2017. The algebra of entanglement and the geometry of composition. PhD, University of Oxford, arXiv:1709.08086(2017)."},{"volume-title":"Programming Logics - Essays in Memory of Harald Ganzinger(Lecture Notes in Computer Science, Vol.\u00a07797)","author":"Hanus Michael","key":"e_1_3_2_1_24_1","unstructured":"Michael Hanus . 2013. Functional Logic Programming: From Theory to Curry . In Programming Logics - Essays in Memory of Harald Ganzinger(Lecture Notes in Computer Science, Vol.\u00a07797) , Andrei Voronkov and Christoph Weidenbach (Eds.). Springer , 123\u2013168. https:\/\/doi.org\/10.1007\/978-3-642-37651-1_6 10.1007\/978-3-642-37651-1_6 Michael Hanus. 2013. Functional Logic Programming: From Theory to Curry. In Programming Logics - Essays in Memory of Harald Ganzinger(Lecture Notes in Computer Science, Vol.\u00a07797), Andrei Voronkov and Christoph Weidenbach (Eds.). Springer, 123\u2013168. https:\/\/doi.org\/10.1007\/978-3-642-37651-1_6"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"crossref","DOI":"10.21236\/ADA087640","volume-title":"Canonical Forms and Unification. In 5th Conference on Automated Deduction","author":"Hullot Jean-Marie","year":"1980","unstructured":"Jean-Marie Hullot . 1980 . Canonical Forms and Unification. In 5th Conference on Automated Deduction , Les Arcs, France , July 8-11, 1980, Proceedings(Lecture Notes in Computer Science, Vol.\u00a087), Wolfgang Bibel and Robert\u00a0A. Kowalski (Eds.). Springer, 318\u2013334. https:\/\/doi.org\/10.1007\/3-540-10009-1_25 10.1007\/3-540-10009-1_25 Jean-Marie Hullot. 1980. Canonical Forms and Unification. In 5th Conference on Automated Deduction, Les Arcs, France, July 8-11, 1980, Proceedings(Lecture Notes in Computer Science, Vol.\u00a087), Wolfgang Bibel and Robert\u00a0A. Kowalski (Eds.). Springer, 318\u2013334. https:\/\/doi.org\/10.1007\/3-540-10009-1_25"},{"volume-title":"Programming in Haskell(2 ed.)","author":"Hutton Graham","key":"e_1_3_2_1_26_1","unstructured":"Graham Hutton . 2016. Programming in Haskell(2 ed.) . Cambridge University Press . https:\/\/doi.org\/10.1017\/CBO9781316784099 10.1017\/CBO9781316784099 Graham Hutton. 2016. Programming in Haskell(2 ed.). Cambridge University Press. https:\/\/doi.org\/10.1017\/CBO9781316784099"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177577"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"crossref","unstructured":"D. Knuth and P. Bendix. 1970. Simple word problems in universal algebra. In Computational Problems in Abstract Algebra John Leech (Ed.). Pergamon Press 263\u2013297.  D. Knuth and P. Bendix. 1970. Simple word problems in universal algebra. In Computational Problems in Abstract Algebra John Leech (Ed.). Pergamon Press 263\u2013297.","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"key":"e_1_3_2_1_29_1","unstructured":"Yves Lafont. 2009. Diagram Rewriting and Operads. Lecture given at the Thematic school : Operads CIRM Luminy (Marseille).  Yves Lafont. 2009. Diagram Rewriting and Operads. Lecture given at the Thematic school : Operads CIRM Luminy (Marseille)."},{"volume-title":"Rewriting Techniques and Applications, Andrei \u201dVoronkov (Ed.)","author":"Lafont Yves","key":"e_1_3_2_1_30_1","unstructured":"Yves Lafont and Pierre Rannou . 2008. Diagram Rewriting for Orthogonal Matrices: A Study of Critical Peaks . In Rewriting Techniques and Applications, Andrei \u201dVoronkov (Ed.) . Springer Berlin Heidelberg , 232\u2013245. Yves Lafont and Pierre Rannou. 2008. Diagram Rewriting for Orthogonal Matrices: A Study of Critical Peaks. In Rewriting Techniques and Applications, Andrei \u201dVoronkov (Ed.). Springer Berlin Heidelberg, 232\u2013245."},{"volume-title":"The resolution calculus","author":"Leitsch A.","key":"e_1_3_2_1_31_1","unstructured":"A. Leitsch . 1997. The resolution calculus . Springer . Texts in Theoretical Computer Science. A. Leitsch. 1997. The resolution calculus. Springer. Texts in Theoretical Computer Science."},{"volume-title":"Definition of standard ML","author":"Milner Robin","key":"e_1_3_2_1_32_1","unstructured":"Robin Milner , Mads Tofte , and Robert Harper . 1990. Definition of standard ML . MIT Press . Robin Milner, Mads Tofte, and Robert Harper. 1990. Definition of standard ML. MIT Press."},{"key":"#cr-split#-e_1_3_2_1_33_1.1","doi-asserted-by":"crossref","unstructured":"Detlef Plump. 2005. Confluence of Graph Transformation Revisited. In Processes Terms and Cycles: Steps on the Road to Infinity Essays Dedicated to Jan Willem Klop on the Occasion of His 60th Birthday(Lecture Notes in Computer Science Vol.\u00a03838) Aart Middeldorp Vincent van Oostrom Femke van Raamsdonk and Roel\u00a0C. de\u00a0Vrijer (Eds.). Springer 280-308. https:\/\/doi.org\/10.1007\/11601548_16 10.1007\/11601548_16","DOI":"10.1007\/11601548_16"},{"key":"#cr-split#-e_1_3_2_1_33_1.2","doi-asserted-by":"crossref","unstructured":"Detlef Plump. 2005. Confluence of Graph Transformation Revisited. In Processes Terms and Cycles: Steps on the Road to Infinity Essays Dedicated to Jan Willem Klop on the Occasion of His 60th Birthday(Lecture Notes in Computer Science Vol.\u00a03838) Aart Middeldorp Vincent van Oostrom Femke van Raamsdonk and Roel\u00a0C. de\u00a0Vrijer (Eds.). Springer 280-308. https:\/\/doi.org\/10.1007\/11601548_16","DOI":"10.1007\/11601548_16"},{"volume-title":"5th International Conference on Graph Transformations (ICGT2010)","author":"M.","key":"e_1_3_2_1_34_1","unstructured":"Christopher\u00a0 M. Poskitt and Detlef Plump. 2010. A Hoare Calculus for Graph Programs . In 5th International Conference on Graph Transformations (ICGT2010) (LNCS, Vol.\u00a06372). Springer, 139\u2013154. Christopher\u00a0M. Poskitt and Detlef Plump. 2010. A Hoare Calculus for Graph Programs. In 5th International Conference on Graph Transformations (ICGT2010)(LNCS, Vol.\u00a06372). Springer, 139\u2013154."},{"key":"e_1_3_2_1_35_1","volume-title":"The GROOVE Simulator: A Tool for State Space Generation. In Second International Workshop on Applications of Graph Transformations with Industrial Relevance, AGTIVE 2003(LNCS, Vol.\u00a03062)","author":"Rensink Arend","year":"2003","unstructured":"Arend Rensink . 2003 . The GROOVE Simulator: A Tool for State Space Generation. In Second International Workshop on Applications of Graph Transformations with Industrial Relevance, AGTIVE 2003(LNCS, Vol.\u00a03062) . Springer, 479\u2013485. Arend Rensink. 2003. The GROOVE Simulator: A Tool for State Space Generation. In Second International Workshop on Applications of Graph Transformations with Industrial Relevance, AGTIVE 2003(LNCS, Vol.\u00a03062). Springer, 479\u2013485."},{"key":"e_1_3_2_1_36_1","volume-title":"Proceedings of the International Joint Conference on Automated Reasoning (IJCAR\u201901)","author":"Riazanov A.","year":"2083","unstructured":"A. Riazanov and A. Voronkov . 2001. Vampire 1.1 (System Description) . In Proceedings of the International Joint Conference on Automated Reasoning (IJCAR\u201901) . Springer LNCS 2083 , 376\u2013380. A. Riazanov and A. Voronkov. 2001. Vampire 1.1 (System Description). In Proceedings of the International Joint Conference on Automated Reasoning (IJCAR\u201901). Springer LNCS 2083, 376\u2013380."},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/321250.321253"},{"key":"e_1_3_2_1_38_1","unstructured":"S. Schulz. [n.d.]. The E Equational Theorem Prover. http:\/\/www4.informatik.tu-muenchen.de\/\u00a0schulz\/WORK\/eprover.html.  S. Schulz. [n.d.]. The E Equational Theorem Prover. http:\/\/www4.informatik.tu-muenchen.de\/\u00a0schulz\/WORK\/eprover.html."},{"key":"e_1_3_2_1_39_1","first-page":"2","article-title":"Automated Formal Verification of Visual Modeling Languages by Model Checking","volume":"3","author":"Varr\u00f3 D\u00e1niel","year":"2004","unstructured":"D\u00e1niel Varr\u00f3 . 2004 . Automated Formal Verification of Visual Modeling Languages by Model Checking . Journal of Software and Systems Modeling 3 , 2 (May 2004), 85\u2013113. D\u00e1niel Varr\u00f3. 2004. Automated Formal Verification of Visual Modeling Languages by Model Checking. Journal of Software and Systems Modeling 3, 2 (May 2004), 85\u2013113.","journal-title":"Journal of Software and Systems Modeling"},{"key":"e_1_3_2_1_40_1","volume-title":"Completeness of the ZX-Calculus. Logical Methods in Computer Science 16","author":"Vilmart Renaud","year":"2020","unstructured":"Renaud Vilmart , Simon Perdrix , and Emmanuel Jeandel . 2020. Completeness of the ZX-Calculus. Logical Methods in Computer Science 16 ( 2020 ). Renaud Vilmart, Simon Perdrix, and Emmanuel Jeandel. 2020. Completeness of the ZX-Calculus. Logical Methods in Computer Science 16 (2020)."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1006\/jsco.2002.0536"},{"key":"e_1_3_2_1_42_1","first-page":"378","article-title":"System Description: SPASS version 1.0.0. In Proceedings of the 16th Conference on Automated Deduction (CADE-16)","volume":"1632","author":"Weidenbach C.","year":"2001","unstructured":"C. Weidenbach , B. Afshordel , U. Brahm , C. Cohrs , T. Engel , E. Keen , C. Theobalt , and D. Topic . 2001 . System Description: SPASS version 1.0.0. In Proceedings of the 16th Conference on Automated Deduction (CADE-16) . Springer LNCS 1632 , 378 \u2013 382 . C. Weidenbach, B. Afshordel, U. Brahm, C. Cohrs, T. Engel, E. Keen, C. Theobalt, and D. Topic. 2001. System Description: SPASS version 1.0.0. In Proceedings of the 16th Conference on Automated Deduction (CADE-16). Springer LNCS 1632, 378\u2013382.","journal-title":"Springer LNCS"}],"event":{"name":"PPDP 2021: 23rd International Symposium on Principles and Practice of Declarative Programming","acronym":"PPDP 2021","location":"Tallinn Estonia"},"container-title":["23rd International Symposium on Principles and Practice of Declarative Programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3479394.3479405","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3479394.3479405","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:18:52Z","timestamp":1750191532000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3479394.3479405"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,9,6]]},"references-count":43,"alternative-id":["10.1145\/3479394.3479405","10.1145\/3479394"],"URL":"https:\/\/doi.org\/10.1145\/3479394.3479405","relation":{},"subject":[],"published":{"date-parts":[[2021,9,6]]},"assertion":[{"value":"2021-10-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}