@article{AcclHornStra:22:An-Analy:wo, author = {Acclavio, Matteo and Horne, Ross and Straßburger, Lutz}, date-added = {2022-11-02 19:39:44 +0000}, date-modified = {2022-11-02 19:39:44 +0000}, doi = {10.46298/lmcs-18(4:1)2022}, journal = {Logical Methods in Computer Science}, keywords = {deep inference}, number = {4}, pages = {1:1--80}, title = {An Analytic Propositional Proof System on Graphs}, url = {https://arxiv.org/abs/2012.01102}, volume = {18}, year = {2022}, bdsk-url-1 = {https://doi.org/10.46298/lmcs-18(4:1)2022}} @inproceedings{AcclHornMauwStra:22:A-Graphi:cz, author = {Acclavio, Matteo and Horne, Ross and Mauw, Sjouke and Straßburger, Lutz}, booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD)}, date-added = {2022-11-02 19:39:44 +0000}, date-modified = {2022-11-02 19:39:44 +0000}, doi = {10.4230/LIPICS.FSCD.2022.22}, editor = {Felty, Amy P.}, keywords = {deep inference}, pages = {22:1--25}, publisher = {Schloss Dagstuhl--Leibniz-Zentrum für Informatik}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, title = {A Graphical Proof Theory of Logical Time}, url = {https://drops.dagstuhl.de/opus/volltexte/2022/16303/pdf/LIPIcs-FSCD-2022-22.pdf}, volume = {228}, year = {2022}, bdsk-url-1 = {https://drops.dagstuhl.de/opus/volltexte/2022/16303/}, bdsk-url-2 = {https://doi.org/10.4230/LIPICS.FSCD.2022.22}} @inproceedings{AcclGuer:20:A-Deep-I:gw, author = {Acclavio, Matteo and Guerrieri, Giulio}, booktitle = {Linearity \& Trends in Linear Logic and Applications (Linearity\&TLLA)}, date-added = {2022-11-02 19:39:44 +0000}, date-modified = {2022-11-02 19:39:44 +0000}, doi = {10.4204/eptcs.353.2}, editor = {Dal Lago, Ugo and de Paiva, Valeria}, keywords = {deep inference}, pages = {26--49}, publisher = {Open Publishing Association}, series = {Electronic Proceedings in Theoretical Computer Science}, title = {A Deep Inference System for Differential Linear Logic}, url = {https://arxiv.org/pdf/2112.14963.pdf}, volume = {353}, year = {2020}, bdsk-url-1 = {https://doi.org/10.4204%2Feptcs.353.2}, bdsk-url-2 = {https://doi.org/10.4204/eptcs.353.2}} @inproceedings{Accl:20:Exponent:lk, author = {Acclavio, Matteo}, booktitle = {Linearity \& Trends in Linear Logic and Applications (Linearity\&TLLA)}, date-added = {2022-11-02 19:39:44 +0000}, date-modified = {2022-11-02 19:39:44 +0000}, doi = {10.4204/eptcs.353.1}, editor = {Dal Lago, Ugo and de Paiva, Valeria}, keywords = {deep inference}, pages = {1--25}, publisher = {Open Publishing Association}, series = {Electronic Proceedings in Theoretical Computer Science}, title = {Exponentially Handsome Proof Nets and Their Normalization}, url = {https://arxiv.org/pdf/2112.14962.pdf}, volume = {353}, year = {2020}, bdsk-url-1 = {https://doi.org/10.4204/eptcs.353.1}} @inproceedings{AcclHornStra:20:Logic-Be:gy, author = {Acclavio, Matteo and Horne, Ross and Straßburger, Lutz}, booktitle = {35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)}, date-added = {2020-12-09 19:57:18 +0000}, date-modified = {2020-12-09 20:13:01 +0000}, doi = {10.1145/3373718.3394763}, editor = {Kobayashi, Naoki}, keywords = {deep inference}, pages = {38--52}, publisher = {ACM}, title = {Logic Beyond Formulas: {A} Proof System on Graphs}, url = {https://satoss.uni.lu/members/ross/pdf/LBF.pdf}, year = {2020}, bdsk-url-1 = {https://satoss.uni.lu/members/ross/pdf/LBF.pdf}, bdsk-url-2 = {https://doi.org/10.1145/3373718.3394763}} @article{AlenOlivPozz:13:Nested-S:xw, author = {Alenda, Régis and Olivetti, Nicola and Pozzato, Gian Luca}, date-added = {2014-04-26 16:03:05 +0000}, date-modified = {2016-04-13 11:26:39 +0000}, doi = {10.1093/logcom/ext034}, journal = {Journal of Logic and Computation}, keywords = {deep inference}, number = {1}, pages = {7--50}, title = {Nested Sequent Calculi for Normal Conditional Logics}, url = {http://www.di.unito.it/~pozzato/papers/JLC2013.pdf}, volume = {26}, year = {2016}, bdsk-url-1 = {http://www.di.unito.it/~pozzato/papers/JLC2013.pdf}, bdsk-url-2 = {http://dx.doi.org/10.1093/logcom/ext034}} @inproceedings{alenda2012nested, author = {Alenda, Régis and Olivetti, Nicola and Pozzato, Gian Luca}, booktitle = {Logics in Artificial Intelligence (JELIA)}, date-added = {2013-03-05 20:13:34 +0000}, date-modified = {2016-12-31 10:11:37 +0000}, doi = {10.1007/978-3-642-33353-8\_2}, editor = {Fariñas del Cerro, Luis and Herzig, Andreas and Mengin, Jérôme}, keywords = {deep inference}, pages = {14--27}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {Nested Sequent Calculi for Conditional Logics}, url = {http://www.di.unito.it/~argo/papers/2012_JELIAb.pdf}, volume = {7519}, year = {2012}, bdsk-url-1 = {http://www.di.unito.it/~argo/papers/2012_JELIAb.pdf}} @article{AlerGugl:18:Subatomi:ty, author = {Aler Tubella, Andrea and Guglielmi, Alessio}, date-added = {2017-03-31 14:28:52 +0000}, date-modified = {2023-05-26 17:40:29 +0100}, doi = {10.1145/3173544}, journal = {ACM Transactions on Computational Logic}, keywords = {deep inference}, number = {1}, pages = {5:1--33}, title = {Subatomic Proof Systems: {S}plittable Systems}, url = {https://arxiv.org/pdf/1703.10258.pdf}, volume = {19}, year = {2018}, bdsk-url-1 = {https://arxiv.org/pdf/1703.10258.pdf}} @inproceedings{AlerGuglRalp:17:Removing:oq, author = {Aler Tubella, Andrea and Guglielmi, Alessio and Ralph, Benjamin}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL)}, date-added = {2017-06-20 09:56:44 +0000}, date-modified = {2017-08-18 14:23:13 +0000}, doi = {10.4230/LIPIcs.CSL.2017.9}, editor = {Goranko, Valentin and Dam, Mads}, keywords = {deep inference}, pages = {9:1--17}, publisher = {Schloss Dagstuhl--Leibniz-Zentrum für Informatik}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, title = {Removing Cycles from Proofs}, url = {http://drops.dagstuhl.de/opus/volltexte/2017/7700/pdf/LIPIcs-CSL-2017-9.pdf}, volume = {82}, year = {2017}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/RCP.pdf}} @phdthesis{Aler:16:A-Study-:hc, author = {Aler Tubella, Andrea}, date-added = {2017-02-09 07:14:34 +0000}, date-modified = {2018-03-23 19:39:13 +0000}, keywords = {deep inference}, school = {University of Bath}, title = {A Study of Normalisation Through Subatomic Logic}, url = {https://people.bath.ac.uk/ag248/aat/phd.pdf}, year = {2017}, bdsk-url-1 = {https://aalertubelladotcom.files.wordpress.com/2017/02/thesis.pdf}} @article{ArisDasStra:15:On-Neste:df, author = {Arisaka, Ryuta and Das, Anupam and Straßburger, Lutz}, date-added = {2016-04-13 10:55:57 +0000}, date-modified = {2016-04-13 10:59:46 +0000}, doi = {10.2168/LMCS-11(3:7)2015}, journal = {Logical Methods in Computer Science}, keywords = {deep inference}, number = {3}, pages = {7:1--33}, title = {On Nested Sequents for Constructive Modal Logics}, url = {http://arxiv.org/pdf/1505.06896.pdf}, volume = {11}, year = {2015}, bdsk-url-1 = {http://arxiv.org/pdf/1505.06896.pdf}, bdsk-url-2 = {http://dx.doi.org/10.2168/LMCS-11(3:7)2015}} @article{BarrGugl:22:A-Subato:yr, author = {Barrett, Chris and Guglielmi, Alessio}, date-added = {2022-11-02 19:39:44 +0000}, date-modified = {2022-11-02 19:39:44 +0000}, doi = {10.1145/3545116}, journal = {ACM Transactions on Computational Logic}, keywords = {deep inference}, number = {4}, pages = {26:1--25}, title = {A Subatomic Proof System for Decision Trees}, url = {https://arxiv.org/pdf/2105.01382.pdf}, volume = {23}, year = {2022}, bdsk-url-1 = {https://doi.org/10.1145/3545116}} @inproceedings{BarrGugl:21:Totally-:zm, author = {Barrett, Victoria and Guglielmi, Alessio}, booktitle = {5th International Workshop on Trends in Linear Logic and Applications (TLLA)}, date-added = {2021-06-28 12:20:08 +0100}, date-modified = {2022-11-02 19:55:31 +0000}, keywords = {deep inference}, pages = {1--7}, title = {Totally Linear Proofs}, url = {https://hal-lirmm.ccsd.cnrs.fr/lirmm-03271417}, year = {2021}, bdsk-url-1 = {https://hal-lirmm.ccsd.cnrs.fr/lirmm-03271417}} @inproceedings{Bilk:11:A-Note-o:fk, author = {Bílková, Marta}, booktitle = {Logic, Language, and Computation (TbiLLC 2009)}, date-added = {2013-03-05 19:49:05 +0000}, date-modified = {2016-12-31 18:48:28 +0000}, doi = {10.1007/978-3-642-22303-7\_3}, editor = {Bezhanishvili, Nick and Löbner, Sebastian and Schwabe, Kerstin and Spada, Luca}, keywords = {deep inference}, pages = {30--45}, publisher = {Springer}, series = {Lecture Notes in Artificial Intelligence}, title = {A Note on Uniform Interpolation Proofs in Modal Deep Inference Calculi}, volume = {6618}, year = {2011}, bdsk-url-1 = {http://dx.doi.org/10.1007/978-3-642-22303-7%5C_3}} @article{BlutPanaSlav:09:Deep-Inf:kb, author = {Blute, Richard and Panangaden, Prakash and Slavnov, Sergey}, date-added = {2009-03-19 15:12:35 +0100}, date-modified = {2014-04-11 00:43:36 +0000}, doi = {10.1007/s10485-010-9241-0}, journal = {Applied Categorical Structures}, keywords = {deep inference}, pages = {209--228}, title = {Deep Inference and Probabilistic Coherence Spaces}, url = {http://www.cs.mcgill.ca/~prakash/Pubs/seqcats.pdf}, volume = {20}, year = {2012}, bdsk-url-1 = {http://www.cs.mcgill.ca/~prakash/Pubs/seqcats.pdf}, bdsk-url-2 = {http://dx.doi.org/10.1007/s10485-010-9241-0}} @incollection{BlutGuglIvanPana:10:A-Logica:uq, author = {Blute, Richard F. and Guglielmi, Alessio and Ivanov, Ivan T. and Panangaden, Prakash and Straßburger, Lutz}, booktitle = {Categories and Types in Logic, Language, and Physics}, date-added = {2010-06-01 10:20:30 +0200}, date-modified = {2014-04-10 22:23:03 +0000}, doi = {10.1007/978-3-642-54789-8\_6}, editor = {Casadio, Claudia and Coecke, Bob and Moortgat, Michael and Scott, Philip}, keywords = {deep inference}, pages = {90--107}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {A Logical Basis for Quantum Evolution and Entanglement}, url = {https://people.bath.ac.uk/ag248/p/LBQEE.pdf}, volume = {8222}, year = {2014}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/LBQEE.pdf}, bdsk-url-2 = {http://dx.doi.org/10.1007/978-3-642-54789-8%5C_6}} @misc{BlutPanaStra:08:The-Logi:lh, author = {Blute, Rick and Panangaden, Prakash and Straßburger, Lutz}, booktitle = {Trends in Logic {VI}: {L}ogic and the Foundations of Physics: {S}pace, Time and Quanta}, date-added = {2009-03-19 14:38:26 +0100}, date-modified = {2015-02-08 11:48:46 +0000}, keywords = {deep inference}, title = {The Logic {BV} and Quantum Causality}, url = {http://www.lix.polytechnique.fr/~lutz/papers/BVlocative.pdf}, year = {2008}, bdsk-url-1 = {http://www.lix.polytechnique.fr/~lutz/papers/BVlocative.pdf}} @inproceedings{BrusStra:17:On-the-L:qr, author = {Bruscoli, Paola and Straßburger, Lutz}, booktitle = {24th International Workshop on Logic, Language, Information, and Computation (WoLLIC)}, date-added = {2017-07-14 08:51:55 +0000}, date-modified = {2017-09-01 10:16:16 +0000}, doi = {10.1007/978-3-662-55386-2\_5}, editor = {Kennedy, Juliette and de Queiroz, Ruy J.G.B.}, keywords = {deep inference}, pages = {68--79}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {On the Length of Medial-Switch-Mix Derivations}, url = {http://opus.bath.ac.uk/56221/1/sm_length.pdf}, volume = {10388}, year = {2017}, bdsk-url-1 = {http://dx.doi.org/10.1007/978-3-662-55386-2%5C_5}} @article{BrusGuglGundPari:09:Quasipol:kx, author = {Bruscoli, Paola and Guglielmi, Alessio and Gundersen, Tom and Parigot, Michel}, date-added = {2009-03-25 12:29:53 +0100}, date-modified = {2017-12-04 12:09:05 +0000}, doi = {10.2168/LMCS-12(2:5)2016}, journal = {Logical Methods in Computer Science}, keywords = {deep inference}, number = {1}, pages = {5:1--30}, title = {Quasipolynomial Normalisation in Deep Inference Via Atomic Flows and Threshold Formulae}, url = {https://lmcs.episciences.org/1637/pdf}, volume = {12}, year = {2016}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/QuasiPolNormDI.pdf}} @misc{BrusGuglGundPari:11:A-Quasip:uq, author = {Bruscoli, Paola and Guglielmi, Alessio and Gundersen, Tom and Parigot, Michel}, date-added = {2010-01-25 08:58:41 +0100}, date-modified = {2015-10-07 23:39:44 +0000}, keywords = {deep inference}, title = {A Quasipolynomial Normalisation Procedure in Deep Inference}, url = {https://people.bath.ac.uk/ag248/p/QPNPDI.pdf}, year = {2011}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/QPNPDI.pdf}} @inproceedings{BrusGuglGundPari:09:A-Quasip:fk, author = {Bruscoli, Paola and Guglielmi, Alessio and Gundersen, Tom and Parigot, Michel}, booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-16)}, date-added = {2011-05-04 17:41:54 +0100}, date-modified = {2015-04-13 09:46:45 +0000}, doi = {10.1007/978-3-642-17511-4\_9}, editor = {Clarke, Edmund M. and Voronkov, Andrei}, keywords = {deep inference}, pages = {136--153}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {A Quasipolynomial Cut-Elimination Procedure in Deep Inference Via Atomic Flows and Threshold Formulae}, url = {https://people.bath.ac.uk/ag248/p/QPNDI.pdf}, volume = {6355}, year = {2010}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/QPNDI.pdf}, bdsk-url-2 = {http://dx.doi.org/10.1007/978-3-642-17511-4%5C_9}} @misc{BrusGugl:09:On-Analy:kx, author = {Bruscoli, Paola and Guglielmi, Alessio}, date-added = {2009-11-23 23:46:58 +0100}, date-modified = {2014-05-08 14:34:37 +0000}, keywords = {deep inference}, title = {On Analyticity in Deep Inference}, url = {https://people.bath.ac.uk/ag248/p/ADI.pdf}, year = {2009}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/ADI.pdf}} @article{BrusGugl:07:On-the-P:fk, author = {Bruscoli, Paola and Guglielmi, Alessio}, date-added = {2007-08-25 21:18:04 +0100}, date-modified = {2014-04-12 10:54:05 +0000}, doi = {10.1145/1462179.1462186}, journal = {ACM Transactions on Computational Logic}, keywords = {deep inference}, number = {2}, pages = {14:1--34}, title = {On the Proof Complexity of Deep Inference}, url = {https://people.bath.ac.uk/ag248/p/PrComplDI.pdf}, volume = {10}, year = {2009}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/PrComplDI.pdf}, bdsk-url-2 = {http://dx.doi.org/10.1145/1462179.1462186}} @misc{BrusGugl:07:On-Analy:uq, author = {Bruscoli, Paola and Guglielmi, Alessio}, date-added = {2007-09-22 14:54:48 +0100}, date-modified = {2014-05-08 14:34:58 +0000}, keywords = {deep inference}, title = {On Analytic Inference Rules in the Calculus of Structures}, url = {https://people.bath.ac.uk/ag248/p/Onan.pdf}, year = {2007}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/Onan.pdf}} @inproceedings{Brus:02:A-Purely:wd, author = {Bruscoli, Paola}, booktitle = {Logic Programming, 18th International Conference (ICLP)}, date-modified = {2014-04-11 12:25:06 +0000}, doi = {10.1007/3-540-45619-8\_21}, editor = {Peter J. Stuckey}, keywords = {deep inference}, pages = {302--316}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {A Purely Logical Account of Sequentiality in Proof Search}, url = {http://cs.bath.ac.uk/pb/bvl/bvl.pdf}, volume = {2401}, year = {2002}, bdsk-url-1 = {http://cs.bath.ac.uk/pb/bvl/bvl.pdf}, bdsk-url-2 = {http://dx.doi.org/10.1007/3-540-45619-8%5C_21}} @inproceedings{Brus:02:A-purely:nx, author = {Bruscoli, Paola}, booktitle = {17. WLP: Workshop Logische Programmierung, {TU} {D}resden, {D}ecember 11--13, 2002}, date-modified = {2014-05-08 15:09:53 +0000}, editor = {Bertram Fronhöfer and Steffen Hölldobler}, keywords = {deep inference}, note = {ISSN 1430--211X}, number = {TUD--FI03--03}, organization = {TU Dresden, 01062 Dresden}, pages = {97--101}, publisher = {Technische Universität Dresden}, series = {Technische Berichte der Fakultät Informatik}, title = {A Purely Logical Account of Sequentiality in Proof Search -- Extended Abstract}, year = {2002}} @article{BrunStud:12:Syntacti:fk, author = {Brünnler, Kai and Studer, Thomas}, date-added = {2013-04-23 17:43:44 +0100}, date-modified = {2016-12-31 18:02:56 +0000}, doi = {10.1016/j.apal.2012.04.006}, journal = {Annals of Pure and Applied Logic}, keywords = {deep inference}, number = {12}, pages = {1838---1853}, title = {Syntactic Cut-Elimination for a Fragment of the Modal Mu-Calculus}, url = {http://www.iam.unibe.ch/ltgpub/2012/bs12.pdf}, volume = {163}, year = {2012}, bdsk-url-1 = {http://www.iam.unibe.ch/ltgpub/2012/bs12.pdf}} @inproceedings{BrunGoetKuzn:10:A-Syntac:uq, author = {Brünnler, Kai and Goetschi, Remo and Kuznets, Roman}, booktitle = {Advances in Modal Logic (AiML)}, date-added = {2010-11-28 17:17:19 +0000}, date-modified = {2014-04-26 17:06:13 +0000}, editor = {Lev Beklemishev and Valentin Goranko and Valentin Shehtman}, keywords = {deep inference}, pages = {39--58}, publisher = {College Publications}, title = {A Syntactic Realization Theorem for Justification Logics}, url = {https://people.bath.ac.uk/ag248/kai/2010srtjl.pdf}, volume = {8}, year = {2010}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/kai/2010srtjl.pdf}} @inproceedings{Brun:10:How-to-U:kx, author = {Brünnler, Kai}, booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-17)}, date-added = {2010-11-28 17:53:20 +0000}, date-modified = {2016-12-31 10:10:05 +0000}, doi = {10.1007/978-3-642-16242-8\_13}, editor = {Fermüller, Christian G. and Voronkov, Andrei}, keywords = {deep inference}, pages = {172--186}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {How to Universally Close the Existential Rule}, url = {https://people.bath.ac.uk/ag248/kai/2010hucer.pdf}, volume = {6397}, year = {2010}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/kai/2010hucer.pdf}} @unpublished{Brun:10:Nested-S:fk, author = {Brünnler, Kai}, date-added = {2010-04-13 18:27:25 +0200}, date-modified = {2016-06-13 05:46:22 +0000}, keywords = {deep inference}, note = {Habilitation Thesis}, school = {Universität Bern}, title = {Nested Sequents}, url = {http://arxiv.org/pdf/1004.1845.pdf}, year = {2010}, bdsk-url-1 = {http://arxiv.org/pdf/1004.1845}} @article{Brun:07:Deep-Seq:fk, author = {Brünnler, Kai}, date-added = {2007-08-26 10:54:46 +0100}, date-modified = {2016-12-31 18:08:08 +0000}, doi = {10.1007/s00153-009-0137-3}, journal = {Archive for Mathematical Logic}, keywords = {deep inference}, number = {6}, pages = {551--577}, title = {Deep Sequent Systems for Modal Logic}, url = {https://people.bath.ac.uk/ag248/kai/2009dssml.pdf}, volume = {48}, year = {2009}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/kai/2009dssml.pdf}} @inproceedings{BrunStra:09:Modular-:ys, author = {Brünnler, Kai and Straßburger, Lutz}, booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux)}, date-added = {2009-05-08 16:15:49 +0200}, date-modified = {2016-12-31 18:51:34 +0000}, doi = {10.1007/978-3-642-02716-1\_12}, keywords = {deep inference}, pages = {152--166}, publisher = {Springer}, series = {Lecture Notes in Artificial Intelligence}, title = {Modular Sequent Systems for Modal Logic}, url = {https://people.bath.ac.uk/ag248/kai/2009mssml.pdf}, volume = {5607}, year = {2009}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/kai/2009mssml.pdf}} @article{BrunStud:09:Syntacti:yq, author = {Brünnler, Kai and Studer, Thomas}, date-added = {2009-05-06 13:13:02 +0200}, date-modified = {2016-12-31 18:02:54 +0000}, doi = {10.1016/j.apal.2009.01.014}, journal = {Annals of Pure and Applied Logic}, keywords = {deep inference}, number = {1}, pages = {82--95}, title = {Syntactic Cut-Elimination for Common Knowledge}, url = {https://people.bath.ac.uk/ag248/kai/infck.pdf}, volume = {160}, year = {2009}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/kai/infck.pdf}} @inproceedings{BrunStud::Syntacti:vn, author = {Brünnler, Kai and Studer, Thomas}, booktitle = {5th Workshop on Methods for Modalities (M4M5 2007)}, date-added = {2007-12-02 20:59:00 +0000}, date-modified = {2009-03-22 15:51:11 +0100}, editor = {Areces, Carlos and Demri, Stéphane}, keywords = {deep inference}, pages = {227--240}, publisher = {Elsevier}, series = {Electronic Notes in Theoretical Computer Science}, title = {Syntactic Cut-Elimination for Common Knowledge}, url = {https://people.bath.ac.uk/ag248/kai/m4m5.pdf}, volume = {231}, year = {2009}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/kai/m4m5.pdf}} @inproceedings{BrunMcKi:08:An-Algor:wq, author = {Brünnler, Kai and McKinley, Richard}, booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning (LPAR)}, date-added = {2008-07-01 12:05:07 +0100}, date-modified = {2016-12-31 10:11:06 +0000}, doi = {10.1007/978-3-540-89439-1\_34}, editor = {Cervesato, Iliano and Veith, Helmut and Voronkov, Andrei}, keywords = {deep inference}, pages = {482---496}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {An Algorithmic Interpretation of a Deep Inference System}, url = {https://people.bath.ac.uk/ag248/kai/2008aidis.pdf}, volume = {5330}, year = {2008}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/kai/2008aidis.pdf}} @article{Brun:06:Cut-Elim:cq, author = {Brünnler, Kai}, date-modified = {2015-07-28 06:35:53 +0000}, doi = {10.1007/s11225-006-6605-4}, journal = {Studia Logica}, keywords = {deep inference}, number = {1}, pages = {51--71}, title = {Cut Elimination Inside a Deep Inference System for Classical Predicate Logic}, url = {https://people.bath.ac.uk/ag248/kai/q.pdf}, volume = {82}, year = {2006}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/kai/q.pdf}} @inproceedings{Brun:06:Deep-Inf:qy, author = {Brünnler, Kai}, booktitle = {Logical Approaches to Computational Barriers---2nd Conference on Computability in Europe}, date-added = {2006-07-16 14:57:44 +0100}, date-modified = {2016-12-31 10:10:25 +0000}, doi = {10.1007/11780342\_7}, editor = {Beckmann, Arnold and Berger, Ulrich and Löwe, Benedikt and Tucker, John V.}, keywords = {deep inference}, pages = {65--74}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {Deep Inference and Its Normal Form of Derivations}, url = {https://people.bath.ac.uk/ag248/kai/n.pdf}, volume = {3988}, year = {2006}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/kai/n.pdf}} @inproceedings{Brun::Deep-Seq:ay, author = {Brünnler, Kai}, booktitle = {Advances in Modal Logic (AiML)}, date-added = {2006-03-30 17:44:13 +0100}, date-modified = {2014-04-26 17:06:13 +0000}, editor = {Guido Governatori and Ian Hodkinson and Yde Venema}, keywords = {deep inference}, pages = {107--119}, publisher = {College Publications}, title = {Deep Sequent Systems for Modal Logic}, url = {http://www.aiml.net/volumes/volume6/Bruennler.ps}, volume = {6}, year = {2006}, bdsk-url-1 = {http://www.aiml.net/volumes/volume6/Bruennler.ps}} @article{Brun:06:Locality:zh, author = {Brünnler, Kai}, date-modified = {2015-06-08 11:01:59 +0000}, doi = {10.1305/ndjfl/1168352668}, journal = {Notre Dame Journal of Formal Logic}, keywords = {deep inference}, number = {4}, pages = {557--580}, title = {Locality for Classical Logic}, url = {https://people.bath.ac.uk/ag248/kai/LocalityClassical.pdf}, volume = {47}, year = {2006}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/kai/LocalityClassical.pdf}} @inproceedings{BrunLeng:05:On-Two-F:jf, author = {Brünnler, Kai and Lengrand, Stéphane}, booktitle = {Structures and Deduction}, date-modified = {2006-12-24 12:12:26 +0000}, editor = {Paola Bruscoli and François Lamarche and Charles Stewart}, keywords = {deep inference}, note = {ICALP Workshop. ISSN 1430-211X}, pages = {69--80}, publisher = {Technische Universität Dresden}, title = {On Two Forms of Bureaucracy in Derivations}, url = {https://people.bath.ac.uk/ag248/kai/sd05.pdf}, year = {2005}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/kai/sd05.pdf}} @incollection{BrunGugl:04:A-First-:ys, author = {Brünnler, Kai and Guglielmi, Alessio}, booktitle = {First-Order Logic Revisited}, city = {Berlin}, date-modified = {2013-03-17 17:21:34 +0000}, editor = {Hendricks, Vincent and Neuhaus, Fabian and Pedersen, Stig Andur and Scheffler, Uwe and Wansing, Heinrich}, keywords = {deep inference}, pages = {59--74}, publisher = {Logos Verlag}, series = {Logische Philosophie}, title = {A First Order System with Finite Choice of Premises}, url = {https://people.bath.ac.uk/ag248/kai/FinFOL.pdf}, year = {2004}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/kai/FinFOL.pdf}} @book{Brun:04:Deep-Inf:rq, address = {Berlin}, author = {Brünnler, Kai}, date-modified = {2006-07-13 13:12:55 +0100}, keywords = {deep inference}, publisher = {Logos Verlag}, title = {Deep Inference and Symmetry in Classical Proofs}, url = {https://people.bath.ac.uk/ag248/kai/phd.pdf}, year = {2004}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/kai/phd.pdf}} @inproceedings{Brun:03:Atomic-C:oz, author = {Brünnler, Kai}, booktitle = {Computer Science Logic (CSL)}, date-modified = {2016-12-31 10:10:46 +0000}, doi = {10.1007/978-3-540-45220-1\_9}, editor = {M. Baaz and J. A. Makowsky}, keywords = {deep inference}, pages = {86--97}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {Atomic Cut Elimination for Classical Logic}, url = {https://people.bath.ac.uk/ag248/kai/ace.pdf}, volume = {2803}, year = {2003}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/kai/ace.pdf}} @article{Brun:03:Two-Rest:mn, author = {Brünnler, Kai}, date-modified = {2021-12-23 16:46:30 +0000}, doi = {10.1093/jigpal/11.5.525}, journal = {Logic Journal of the {IGPL}}, keywords = {deep inference}, number = {5}, pages = {525--529}, title = {Two Restrictions on Contraction}, url = {https://people.bath.ac.uk/ag248/kai/RestContr.pdf}, volume = {11}, year = {2003}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/kai/RestContr.pdf}} @techreport{BrunGugl:02:Consiste:kn, author = {Brünnler, Kai and Guglielmi, Alessio}, date-modified = {2006-07-13 13:12:55 +0100}, institution = {Technische Universität Dresden}, keywords = {deep inference}, number = {WV-02-16}, title = {Consistency Without Cut Elimination}, url = {https://people.bath.ac.uk/ag248/p/AG4.pdf}, year = {2002}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/AG4.pdf}} @inproceedings{BrunTiu:01:A-Local-:mz, author = {Brünnler, Kai and Tiu, Alwen Fernanto}, booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning (LPAR)}, date-modified = {2014-05-20 03:32:27 +0000}, doi = {10.1007/3-540-45653-8\_24}, editor = {R. Nieuwenhuis and Voronkov, Andrei}, keywords = {deep inference}, pages = {347--361}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {A Local System for Classical Logic}, url = {https://people.bath.ac.uk/ag248/kai/lcl-lpar.pdf}, volume = {2250}, year = {2001}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/kai/lcl-lpar.pdf}, bdsk-url-2 = {http://dx.doi.org/10.1007/3-540-45653-8%5C_24}} @techreport{BrunTiu:01:A-Local-:ly, author = {Brünnler, Kai and Tiu, Alwen Fernanto}, date-modified = {2014-04-15 09:32:52 +0000}, institution = {Technische Universität Dresden}, keywords = {deep inference}, number = {WV-01-02}, title = {A Local System for Classical Logic}, year = {2001}, bdsk-url-1 = {http://iccl.tu-dresden.de/~kai/LocalClassicalLogic-tr.pdf}} @inproceedings{ChauMariStra:16:Modular-:fk, author = {Chaudhuri, Kaustuv and Marin, Sonia and Straßburger, Lutz}, booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD)}, date-added = {2016-05-02 11:12:58 +0000}, date-modified = {2016-12-31 19:51:02 +0000}, doi = {10.4230/LIPIcs.FSCD.2016.16}, editor = {Kesner, Delia and Pientka, Brigitte}, keywords = {deep inference}, pages = {16:1--18}, publisher = {Schloss Dagstuhl--Leibniz-Zentrum für Informatik}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, title = {Modular Focused Proof Systems for Intuitionistic Modal Logics}, url = {http://www.lix.polytechnique.fr/~lutz/papers/fscd16focint.pdf}, volume = {52}, year = {2016}, bdsk-url-1 = {http://kaustuv.chaudhuri.info/papers/fossacs16focnest.pdf}, bdsk-url-2 = {http://dx.doi.org/10.1007/978-3-662-49630-5%5C_23}} @inproceedings{ChauMariStra:16:Focused-:uk, author = {Chaudhuri, Kaustuv and Marin, Sonia and Straßburger, Lutz}, booktitle = {Foundations of Software Science and Computation Structures (FoSSaCS)}, date-added = {2016-04-13 09:55:11 +0000}, date-modified = {2016-04-13 09:58:01 +0000}, doi = {10.1007/978-3-662-49630-5\_23}, editor = {Jacobs, Bart and Löding, Christof}, keywords = {deep inference}, pages = {390--407}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {Focused and Synthetic Nested Sequents}, url = {http://kaustuv.chaudhuri.info/papers/fossacs16focnest.pdf}, volume = {9634}, year = {2016}, bdsk-url-1 = {http://kaustuv.chaudhuri.info/papers/fossacs16focnest.pdf}, bdsk-url-2 = {http://dx.doi.org/10.1007/978-3-662-49630-5%5C_23}} @inproceedings{ChauGuen:14:Equality:rt, author = {Chaudhuri, Kaustuv and Guenot, Nicolas}, booktitle = {Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic (CSL) and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)}, date-added = {2014-04-26 14:14:04 +0000}, date-modified = {2015-04-13 08:26:24 +0000}, doi = {10.1145/2603088.2603140}, editor = {Henzinger, Thomas and Miller, Dale}, keywords = {deep inference}, pages = {30:1--10}, publisher = {ACM}, title = {Equality and Fixpoints in the Calculus of Structures}, url = {http://chaudhuri.info/papers/csllics14eqfix.pdf}, year = {2014}, bdsk-url-1 = {http://chaudhuri.info/papers/csllics14eqfix.pdf}} @inproceedings{ChauGuenStra:11:The-Focu:fk, author = {Chaudhuri, Kaustuv and Guenot, Nicolas and Straßburger, Lutz}, booktitle = {Computer Science Logic (CSL)}, date-added = {2012-07-07 12:52:40 +0100}, date-modified = {2014-04-12 11:05:02 +0000}, doi = {10.4230/LIPIcs.CSL.2011.159}, editor = {Bezem, Marc}, keywords = {deep inference}, pages = {159--173}, publisher = {Schloss Dagstuhl--Leibniz-Zentrum für Informatik}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, title = {The Focused Calculus of Structures}, url = {http://drops.dagstuhl.de/opus/volltexte/2011/3229/}, volume = {12}, year = {2011}, bdsk-url-1 = {http://drops.dagstuhl.de/opus/volltexte/2011/3229/pdf/16.pdf}, bdsk-url-2 = {http://drops.dagstuhl.de/opus/volltexte/2011/3229/}, bdsk-url-3 = {http://dx.doi.org/10.4230/LIPIcs.CSL.2011.159}} @inproceedings{CiobHorn:15:Behaviou:ye, author = {Ciobanu, Gabriel and Horne, Ross}, booktitle = {Perspectives of System Informatics (PSI)}, date-added = {2016-06-30 13:04:02 +0000}, date-modified = {2019-04-04 18:04:58 +0100}, doi = {10.1007/978-3-319-41579-6\_8}, editor = {Mazzara, Manuel and Voronkov, Andrei}, keywords = {deep inference}, pages = {91--106}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {Behavioural Analysis of Sessions Using the Calculus of Structures}, url = {http://satoss.uni.lu/members/ross/pdf/sessions.pdf}, volume = {9609}, year = {2015}, bdsk-url-1 = {http://www.ntu.edu.sg/home/rhorne/psi.pdf}, bdsk-url-2 = {http://dx.doi.org/10.1007/978-3-319-41579-6%5C_8}} @inproceedings{ClouDawsGoreTiu:13:Annotati:sy, author = {Clouston, Ranald and Dawson, Jeremy and Goré, Rajeev and Tiu, Alwen}, booktitle = {Computer Science Logic (CSL)}, date-added = {2014-04-26 16:39:15 +0000}, date-modified = {2014-04-26 16:45:01 +0000}, doi = {10.4230/LIPIcs.CSL.2013.197}, editor = {Ronchi Della Rocca, Simona}, keywords = {deep inference}, note = {Extended version at \url{http://arxiv.org/abs/1307.0289}}, pages = {197--214}, publisher = {Schloss Dagstuhl--Leibniz-Zentrum für Informatik}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, title = {Annotation-Free Sequent Calculi for Full Intuitionistic Linear Logic}, volume = {23}, year = {2013}, bdsk-url-1 = {http://dx.doi.org/10.4230/LIPIcs.CSL.2013.197}} @inproceedings{DasRice:21:New-Mini:wt, author = {Das, Anupam and Rice, Alex A.}, booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD)}, date-added = {2021-12-23 15:49:36 +0000}, date-modified = {2021-12-23 15:53:10 +0000}, doi = {10.4230/LIPIcs.FSCD.2021.14}, editor = {Kobayashi, Naoki}, keywords = {deep inference}, pages = {14:1--14:19}, publisher = {Schloss Dagstuhl--Leibniz-Zentrum für Informatik}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, title = {New Minimal Linear Inferences in Boolean Logic Independent of Switch and Medial}, url = {https://drops.dagstuhl.de/opus/volltexte/2021/14252/pdf/LIPIcs-FSCD-2021-14.pdf}, volume = {195}, year = {2021}, bdsk-url-1 = {https://drops.dagstuhl.de/opus/volltexte/2021/14252/pdf/LIPIcs-FSCD-2021-14.pdf}, bdsk-url-2 = {https://doi.org/10.4230/LIPIcs.FSCD.2021.14}} @misc{Das:17:An-Unavo:ty, author = {Das, Anupam}, date-added = {2017-06-24 21:53:36 +0000}, date-modified = {2017-06-24 21:55:56 +0000}, keywords = {deep inference}, title = {An Unavoidable Contraction Loop in Monotone Deep Inference}, url = {https://people.bath.ac.uk/ag248/das/con-loop.pdf}, year = {2017}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/das/con-loop.pdf}} @article{DasStra:16:On-Linea:uk, author = {Das, Anupam and Straßburger, Lutz}, date-added = {2017-02-28 06:35:00 +0000}, date-modified = {2017-02-28 06:45:22 +0000}, doi = {10.2168/LMCS-12(4:9)2016}, journal = {Logical Methods in Computer Science}, keywords = {deep inference}, number = {4}, pages = {9:1--27}, title = {On Linear Rewriting Systems for Boolean Logic and Some Applications to Proof Theory}, url = {https://arxiv.org/pdf/1610.08772.pdf}, volume = {12}, year = {2016}, bdsk-url-1 = {https://arxiv.org/pdf/1610.08772.pdf}, bdsk-url-2 = {http://dx.doi.org/10.2168/LMCS-12(4:9)2016}} @inproceedings{Das:16:From-Pos:vn, author = {Das, Anupam}, booktitle = {31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)}, date-added = {2016-04-13 08:28:33 +0000}, date-modified = {2020-12-09 20:06:03 +0000}, doi = {10.1145/2933575.2934570}, editor = {Shankar, Natarajan}, keywords = {deep inference}, pages = {126--135}, publisher = {ACM}, title = {From Positive and Intuitionistic Bounded Arithmetic to Monotone Proof Complexity}, url = {http://www.anupamdas.com/items/pos-int-bdarith-mon-pc/pos-int-bdarith-mon-pc.pdf}, year = {2016}, bdsk-url-1 = {http://www.anupamdas.com/items/pos-int-bdarith-mon-pc/pos-int-bdarith-mon-pc.pdf}} @inproceedings{DasStra:15:No-Compl:yg, author = {Das, Anupam and Straßburger, Lutz}, booktitle = {26th International Conference on Rewriting Techniques and Applications (RTA)}, date-added = {2015-04-13 06:50:56 +0000}, date-modified = {2016-04-13 10:23:08 +0000}, doi = {10.4230/LIPIcs.RTA.2015.127}, editor = {Fernández, Maribel}, keywords = {deep inference}, pages = {127--142}, publisher = {Schloss Dagstuhl--Leibniz-Zentrum für Informatik}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, title = {No Complete Linear Term Rewriting System for Propositional Logic}, url = {http://drops.dagstuhl.de/opus/volltexte/2015/5193/pdf/13.pdf}, volume = {36}, year = {2015}, bdsk-url-1 = {http://www.anupamdas.com/items/NoCompLinSys/NoCompLinSys.pdf}} @article{Das:13:Some-Res:fk, author = {Das, Anupam}, date-added = {2013-04-06 17:28:37 +0100}, date-modified = {2015-04-13 09:25:38 +0000}, doi = {10.2168/LMCS-11(1:4)2015}, journal = {Logical Methods in Computer Science}, keywords = {deep inference}, number = {1}, pages = {4:1--27}, title = {On the Relative Proof Complexity of Deep Inference Via Atomic Flows}, url = {http://arxiv.org/pdf/1502.05860.pdf}, volume = {11}, year = {2015}, bdsk-url-1 = {http://www.anupamdas.com/items/RelCompFull/RelCompFull.pdf}} @phdthesis{Das:14:The-Comp:eu, author = {Das, Anupam}, date-added = {2016-04-13 08:36:10 +0000}, date-modified = {2016-04-13 08:37:27 +0000}, keywords = {deep inference}, school = {University of Bath}, title = {The Complexity of Propositional Proofs in Deep Inference}, url = {http://www.anupamdas.com/items/thesis/Thesis-AnupamDas.pdf}, year = {2014}, bdsk-url-1 = {http://www.anupamdas.com/items/thesis/Thesis-AnupamDas.pdf}} @inproceedings{Das:13:The-Pige:fk, author = {Das, Anupam}, booktitle = {Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic (CSL) and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)}, date-added = {2013-03-05 20:50:34 +0000}, date-modified = {2015-04-13 08:28:14 +0000}, doi = {10.1145/2603088.2603164}, editor = {Henzinger, Thomas and Miller, Dale}, keywords = {deep inference}, pages = {36:1--10}, publisher = {ACM}, title = {On the Pigeonhole and Related Principles in Deep Inference and Monotone Systems}, url = {http://www.anupamdas.com/items/WeakMonProofsPHP/WeakMonProofsPHP.pdf}, year = {2014}, bdsk-url-1 = {http://www.anupamdas.com/items/WeakMonProofsPHP/WeakMonProofsPHP.pdf}, bdsk-url-2 = {http://dx.doi.org/10.1145/2603088.2603164}} @inproceedings{Das:13:Rewritin:uq, author = {Das, Anupam}, booktitle = {24th International Conference on Rewriting Techniques and Applications (RTA)}, date-added = {2013-03-05 20:52:11 +0000}, date-modified = {2014-04-26 16:27:15 +0000}, doi = {10.4230/LIPIcs.RTA.2013.158}, editor = {van Raamsdonk, Femke}, keywords = {deep inference}, pages = {158--173}, publisher = {Schloss Dagstuhl--Leibniz-Zentrum für Informatik}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, title = {Rewriting with Linear Inferences in Propositional Logic}, url = {http://www.anupamdas.com/items/RewritingWithLinearInferences/RewritingWithLinearInferences.pdf}, volume = {21}, year = {2013}, bdsk-url-1 = {http://www.anupamdas.com/items/RewritingWithLinearInferences/RewritingWithLinearInferences.pdf}, bdsk-url-2 = {http://dx.doi.org/10.4230/LIPIcs.RTA.2013.158}} @inproceedings{Das:12:Complexi:kx, author = {Das, Anupam}, booktitle = {Computability in Europe}, date-added = {2012-07-07 15:09:55 +0100}, date-modified = {2015-04-13 09:47:13 +0000}, doi = {10.1007/978-3-642-30870-3\_15}, editor = {Cooper, S. Barry and Dawar, Anuj and Löwe, Benedikt}, keywords = {deep inference}, pages = {139--150}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {Complexity of Deep Inference Via Atomic Flows}, url = {http://www.anupamdas.com/items/RelComp/RelComp.pdf}, volume = {7318}, year = {2012}, bdsk-url-1 = {http://www.anupamdas.com/items/RelComp/RelComp.pdf}, bdsk-url-2 = {http://dx.doi.org/10.1007/978-3-642-30870-3%5C_15}} @inproceedings{Das:11:On-the-P:fk, author = {Das, Anupam}, booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux)}, date-added = {2011-05-04 11:55:58 +0100}, date-modified = {2016-12-31 18:51:26 +0000}, doi = {10.1007/978-3-642-22119-4\_12}, editor = {Brünnler, Kai and Metcalfe, George}, keywords = {deep inference}, pages = {134--148}, publisher = {Springer}, series = {Lecture Notes in Artificial Intelligence}, title = {On the Proof Complexity of Cut-Free Bounded Deep Inference}, url = {http://www.anupamdas.com/items/PrCompII/ProofComplexityBoundedDI.pdf}, volume = {6793}, year = {2011}, bdsk-url-1 = {http://www.anupamdas.com/items/PrCompII/ProofComplexityBoundedDI.pdf}, bdsk-url-2 = {http://dx.doi.org/10.1007/978-3-642-22119-4%5C_12}} @inproceedings{Di-G:04:Structur:wy, author = {Di Gianantonio, Pietro}, booktitle = {Computer Science Logic (CSL)}, date-modified = {2016-06-13 05:31:05 +0000}, doi = {10.1007/978-3-540-30124-0\_13}, editor = {J. Marcinkowski and A. Tarlecki}, keywords = {deep inference}, pages = {130--144}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {Structures for Multiplicative Cyclic Linear Logic: {D}eepness Vs Cyclicity}, url = {https://users.dimi.uniud.it/~pietro.digianantonio/papers/copy_pdf/smcll.pdf}, volume = {3210}, year = {2004}, bdsk-url-1 = {http://www.dimi.uniud.it/~pietro/papers/Soft-copy-ps/scll.ps.gz}} @inproceedings{DonaStruWern:22:A-Drag-a:de, author = {Donato, Pablo and Strub, Pierre-Yves and Werner, Benjamin}, booktitle = {11th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP)}, date-added = {2022-11-02 19:39:44 +0000}, date-modified = {2022-11-02 19:39:44 +0000}, doi = {10.1145/3497775.3503692}, editor = {Popescu, Andrei and Zdancewic, Steve}, keywords = {deep inference}, pages = {197--209}, publisher = {ACM}, title = {A Drag-and-Drop Proof Tactic}, url = {http://www.lix.polytechnique.fr/Labo/Pablo.DONATO/papers/cpp-article.pdf}, year = {2022}, bdsk-url-1 = {https://doi.org/10.1145%2F3497775.3503692}, bdsk-url-2 = {https://doi.org/10.1145/3497775.3503692}} @article{DyckSadrTruf:13:Algebra-:fe, author = {Dyckhoff, Roy and Sadrzadeh, Mehrnoosh and Truffaut, Julien}, date-added = {2014-04-26 15:30:34 +0000}, date-modified = {2016-06-12 10:27:51 +0000}, doi = {10.1145/2536740.2536742}, journal = {ACM Transactions on Computational Logic}, keywords = {deep inference}, number = {4}, pages = {34:1--37}, title = {Algebra, Proof Theory and Applications for an Intuitionistic Logic of Propositions, Actions and Adjoint Modal Operators}, url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.307.1219&rep=rep1&type=pdf}, volume = {14}, year = {2013}, bdsk-url-1 = {http://tocl.acm.org/accepted/dyckhoff_algebra.pdf}, bdsk-url-2 = {http://dx.doi.org/10.1145/2536740.2536742}} @article{FittKuzn:15:Modal-In:dw, author = {Fitting, Melvin and Kuznets, Roman}, date-added = {2016-04-13 10:31:20 +0000}, date-modified = {2016-06-13 06:08:22 +0000}, doi = {doi:10.1016/j.apal.2014.11.002}, journal = {Annals of Pure and Applied Logic}, keywords = {deep inference}, number = {3}, pages = {274--305}, title = {Modal Interpolation Via Nested Sequents}, url = {https://sites.google.com/site/kuznets/interpolation.pdf?attredirects=1}, volume = {166}, year = {2015}, bdsk-url-1 = {http://is.gd/tp01QD}, bdsk-url-2 = {http://dx.doi.org/10.1016/j.apal.2014.11.002}} @article{Fitt:11:Nested-S:kx, author = {Fitting, Melvin}, date-added = {2012-07-05 17:08:40 +0100}, date-modified = {2016-06-14 04:46:24 +0000}, doi = {10.1215/00294527-2377869}, journal = {Notre Dame Journal of Formal Logic}, keywords = {deep inference}, number = {1}, pages = {41--61}, title = {Nested Sequents for Intuitionistic Logics}, url = {http://melvinfitting.org/bookspapers/pdf/papers/IntuitionisticNested.pdf}, volume = {55}, year = {2014}, bdsk-url-1 = {http://comet.lehman.cuny.edu/fitting/bookspapers/pdf/papers/IntuitionisticNested.pdf}} @article{Fitt:12:Prefixed:fk, author = {Fitting, Melvin}, date-added = {2012-07-05 16:01:17 +0100}, date-modified = {2016-06-14 04:44:35 +0000}, doi = {10.1016/j.apal.2011.09.004}, journal = {Annals of Pure and Applied Logic}, keywords = {deep inference}, number = {3}, pages = {291--313}, title = {Prefixed Tableaus and Nested Sequents}, url = {http://melvinfitting.org/bookspapers/pdf/papers/NestedSequentsPostingVersion/PrefixedDeep.pdf}, volume = {163}, year = {2012}, bdsk-url-1 = {http://comet.lehman.cuny.edu/fitting/bookspapers/pdf/papers/NestedSequentsPostingVersion/PrefixedDeep.pdf}} @incollection{Fitt:11:Proving-:uq, author = {Fitting, Melvin}, booktitle = {Logic without Frontiers}, date-added = {2012-07-05 16:48:58 +0100}, date-modified = {2016-06-14 04:36:08 +0000}, editor = {Béziau, Jean-Yves and Coniglio, Marcelo Esteban}, keywords = {deep inference}, pages = {145--154}, publisher = {College Publications}, series = {Tributes}, title = {Proving Completeness for Nested Sequent Calculi}, url = {http://www.melvinfitting.org/bookspapers/pdf/papers/Carnielli.pdf}, volume = {17}, year = {2011}, bdsk-url-1 = {http://comet.lehman.cuny.edu/fitting/bookspapers/pdf/papers/Carnielli.pdf}} @inproceedings{GimeMose:13:The-Stru:fk, author = {Gimenez, Stéphane and Moser, Georg}, booktitle = {Computer Science Logic (CSL)}, date-added = {2013-07-07 22:14:45 +0000}, date-modified = {2014-04-11 17:18:55 +0000}, doi = {10.4230/LIPIcs.CSL.2013.316}, editor = {Ronchi Della Rocca, Simona}, keywords = {deep inference}, pages = {316--331}, publisher = {Schloss Dagstuhl--Leibniz-Zentrum für Informatik}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, title = {The Structure of Interaction}, url = {http://cl-informatik.uibk.ac.at/users/sgimenez/data/articles/soi.pdf}, volume = {23}, year = {2013}, bdsk-url-1 = {http://cl-informatik.uibk.ac.at/users/sgimenez/data/articles/soi.pdf}, bdsk-url-2 = {http://dx.doi.org/10.4230/LIPIcs.CSL.2013.316}} @inproceedings{GirlStra:20:MOIN:-A-:qm, author = {Girlando, Marianna and Straßburger, Lutz}, booktitle = {Automated Reasoning -- 10th International Joint Conference (IJCAR)}, date-added = {2021-02-07 12:02:52 +0000}, date-modified = {2021-02-07 12:12:13 +0000}, doi = {10.1007/978-3-030-51054-1\_25}, editor = {Sofronie-Stokkermans, Viorica and Peltier, Nicolas}, keywords = {deep inference}, pages = {398--407}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {{MOIN}: {A} Nested Sequent Theorem Prover for Intuitionistic Modal Logics (System Description)}, url = {https://hal.inria.fr/hal-02457240v3/document}, volume = {12166}, year = {2020}, bdsk-url-1 = {https://hal.inria.fr/hal-02457240v3/document}, bdsk-url-2 = {https://doi.org/10.1007/978-3-030-51054-1%5C_25}} @inproceedings{GoreRama:12:Labelled:fk, author = {Goré, Rajeev and Ramanayake, Revantha}, booktitle = {Advances in Modal Logic (AiML)}, date-added = {2012-07-08 16:26:52 +0100}, date-modified = {2016-06-13 06:09:42 +0000}, editor = {Bolander, Thomas and Braüner, Torben and Ghilardi, Silvio and Lawrence Moss}, keywords = {deep inference}, pages = {279--299}, publisher = {College Publications}, title = {Labelled Tree sequents, Tree Hypersequents and Nested (Deep) Sequents}, url = {http://users.cecs.anu.edu.au/~rpg/Publications/AiML2012/gore-ramanayake-aiml12.pdf}, volume = {9}, year = {2012}, bdsk-url-1 = {http://rsise.anu.edu.au/~rpg/Publications/AiML2012/gore-ramanayake-aiml12.pdf}} @article{GorePostTiu:11:On-the-C:fk, author = {Goré, Rajeev and Postniece, Linda and Tiu, Alwen}, date-added = {2011-05-05 07:11:03 +0100}, date-modified = {2016-06-13 05:48:18 +0000}, doi = {10.2168/LMCS-7(2:8)2011}, journal = {Logical Methods in Computer Science}, keywords = {deep inference}, number = {2}, pages = {8:1--38}, title = {On the Correspondence Between Display Postulates and Deep Inference in Nested Sequent Calculi for Tense Logics}, url = {http://arxiv.org/pdf/1103.5286.pdf}, volume = {7}, year = {2011}, bdsk-url-1 = {http://arxiv.org/pdf/1103.5286}} @inproceedings{GorePostTiu:10:Cut-Elim:vn, author = {Goré, Rajeev and Postniece, Linda and Tiu, Alwen}, booktitle = {Advances in Modal Logic (AiML)}, date-added = {2010-11-28 18:18:12 +0000}, date-modified = {2014-04-26 17:06:13 +0000}, editor = {Lev Beklemishev and Valentin Goranko and Valentin Shehtman}, keywords = {deep inference}, pages = {156--177}, publisher = {College Publications}, title = {Cut-Elimination and Proof Search for Bi-Intuitionistic Tense Logic}, url = {http://www.aiml.net/volumes/volume8/Gore-Postniece-Tiu.pdf}, volume = {8}, year = {2010}, bdsk-url-1 = {http://www.aiml.net/volumes/volume8/Gore-Postniece-Tiu.pdf}} @inproceedings{GorePostTiu:09:Taming-D:rt, author = {Goré, Rajeev and Postniece, Linda and Tiu, Alwen}, booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux)}, date-added = {2009-05-08 15:46:50 +0200}, date-modified = {2016-12-31 18:51:31 +0000}, doi = {10.1007/978-3-642-02716-1\_15}, keywords = {deep inference}, pages = {189--204}, publisher = {Springer}, series = {Lecture Notes in Artificial Intelligence}, title = {Taming Displayed Tense Logics Using Nested Sequents With Deep Inference}, url = {http://users.cecs.anu.edu.au/~tiu/papers/kt.pdf}, volume = {5607}, year = {2009}, bdsk-url-1 = {http://users.cecs.anu.edu.au/~tiu/papers/kt.pdf}} @inproceedings{GorePostTiu:08:Cut-Elim:yq, author = {Goré, Rajeev and Postniece, Linda and Tiu, Alwen}, booktitle = {Advances in Modal Logic (AiML)}, date-added = {2009-05-08 15:19:06 +0200}, date-modified = {2014-04-26 17:06:13 +0000}, editor = {Carlos Areces and Robert Goldblatt}, keywords = {deep inference}, pages = {43--66}, publisher = {College Publications}, title = {Cut-Elimination and Proof-Search for Bi-Intuitionistic Logic Using Nested Sequents}, url = {http://www.aiml.net/volumes/volume7/Gore-Postniece-Tiu.pdf}, volume = {7}, year = {2008}, bdsk-url-1 = {http://www.aiml.net/volumes/volume7/Gore-Postniece-Tiu.pdf}} @article{GoreTiu:06:Classica:uq, author = {Goré, Rajeev and Tiu, Alwen}, date-added = {2006-09-13 07:31:25 +0100}, date-modified = {2016-12-31 18:10:45 +0000}, doi = {10.1093/logcom/exm026}, journal = {Journal of Logic and Computation}, keywords = {deep inference}, number = {4}, pages = {767--794}, title = {Classical Modal Display Logic in the Calculus of Structures and Minimal Cut-free Deep Inference Calculi for {S5}}, url = {http://users.cecs.anu.edu.au/~tiu/papers/cmdl.pdf}, volume = {17}, year = {2007}, bdsk-url-1 = {http://users.cecs.anu.edu.au/~tiu/papers/cmdl.pdf}} @inproceedings{GuenStra:14:Symmetri:uq, author = {Guenot, Nicolas and Straßburger, Lutz}, booktitle = {Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic (CSL) and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)}, date-added = {2014-04-26 14:04:01 +0000}, date-modified = {2015-04-13 08:30:11 +0000}, doi = {10.1145/2603088.2603160}, editor = {Henzinger, Thomas and Miller, Dale}, keywords = {deep inference}, pages = {45:1--10}, publisher = {ACM}, title = {Symmetric Normalisation for Intuitionistic Logic}, url = {http://www.lix.polytechnique.fr/Labo/Lutz.Strassburger/papers/sjs2-final-with-appendix.pdf}, year = {2014}, bdsk-url-1 = {http://www.lix.polytechnique.fr/Labo/Lutz.Strassburger/papers/sjs2-final-with-appendix.pdf}, bdsk-url-2 = {http://dx.doi.org/10.1145/2603088.2603160}} @phdthesis{Guen:13:Nested-D:uq, author = {Guenot, Nicolas}, date-added = {2013-04-23 18:40:26 +0100}, date-modified = {2014-04-26 14:00:45 +0000}, keywords = {deep inference}, school = {École Polytechnique}, title = {Nested Deduction in Logical Foundations for Computation}, url = {http://www.itu.dk/people/ngue/pub/thesis.pdf}, year = {2013}, bdsk-url-1 = {http://www.lix.polytechnique.fr/~nguenot/th/thesis.pdf}, bdsk-url-2 = {http://www.itu.dk/people/ngue/pub/thesis.pdf}} @inproceedings{Guen:11:Nested-P:la, author = {Guenot, Nicolas}, booktitle = {13th International ACM SIGPLAN Symposium on Principles and Practices of Declarative Programming (PPDP)}, date-added = {2014-04-26 14:25:16 +0000}, date-modified = {2015-04-13 08:18:46 +0000}, doi = {10.1145/2003476.2003501}, editor = {Hanus, Michael and Schneider-Kamp, Peter}, keywords = {deep inference}, pages = {183--193}, publisher = {ACM}, series = {PPDP}, title = {Nested Proof Search as Reduction in the $\lambda$-calculus}, url = {http://www.itu.dk/people/ngue/pub/ppdp11.pdf}, year = {2011}, bdsk-url-1 = {http://www.itu.dk/people/ngue/pub/ppdp11.pdf}, bdsk-url-2 = {http://dx.doi.org/10.1145/2003476.2003501}} @inproceedings{Guen:10:Focused-:uq, author = {Guenot, Nicolas}, booktitle = {Technical Communications of the 26th International Conference on Logic Programming}, date-added = {2011-05-05 09:50:18 +0100}, date-modified = {2014-04-12 11:03:57 +0000}, doi = {10.4230/LIPIcs.ICLP.2010.84}, editor = {Manuel Hermenegildo and Torsten Schaub}, keywords = {deep inference}, pages = {84--93}, publisher = {Schloss Dagstuhl--Leibniz-Zentrum für Informatik}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, title = {Focused Proof Search for Linear Logic in the Calculus of Structures}, url = {http://drops.dagstuhl.de/opus/volltexte/2010/2586/}, volume = {7}, year = {2010}, bdsk-url-1 = {http://drops.dagstuhl.de/opus/volltexte/2010/2586/pdf/10003.GuenotNicolas.2586.pdf}, bdsk-url-2 = {http://drops.dagstuhl.de/opus/volltexte/2010/2586/}, bdsk-url-3 = {http://dx.doi.org/10.4230/LIPIcs.ICLP.2010.84}} @inproceedings{GiulHeijPaul:21:A-Deep-Q:qr, author = {Guerrieri, Giulio and Heijltjes, Willem and Paulus, Joseph W.N.}, booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL)}, date-added = {2021-02-07 11:55:44 +0000}, date-modified = {2021-02-07 11:59:42 +0000}, doi = {10.4230/LIPIcs.CSL.2021.24}, editor = {Baier, Christel and Goubault-Larrecq, Jean}, keywords = {deep inference}, pages = {24:1--24}, publisher = {Schloss Dagstuhl--Leibniz-Zentrum für Informatik}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, title = {A Deep Quantitative Type System}, url = {https://drops.dagstuhl.de/opus/volltexte/2021/13458/}, volume = {183}, year = {2021}, bdsk-url-1 = {https://drops.dagstuhl.de/opus/volltexte/2021/13458/}, bdsk-url-2 = {https://doi.org/10.4230/LIPIcs.CSL.2021.24}} @misc{Gugl:23:Deep-Inf:qf, author = {Guglielmi, Alessio}, date-added = {2007-03-03 16:59:08 +0000}, date-modified = {2023-04-12 16:50:04 +0100}, howpublished = {Web site at \url{http://alessio.guglielmi.name/res/cos}}, keywords = {deep inference}, title = {Deep Inference}, year = {2023}} @incollection{Gugl:14:Deep-Inf:fj, author = {Guglielmi, Alessio}, booktitle = {All About Proofs, Proofs for All}, date-added = {2014-12-02 07:20:51 +0000}, date-modified = {2015-01-25 13:57:50 +0000}, editor = {Delahaye, David and Woltzenlogel Paleo, Bruno}, keywords = {deep inference}, pages = {164--172}, publisher = {College Publications}, series = {Mathematical Logic and Foundations}, title = {Deep Inference}, url = {https://people.bath.ac.uk/ag248/p/DI.pdf}, volume = {55}, year = {2015}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/DI.pdf}} @misc{Gugl:14:The-Comm:yu, author = {Guglielmi, Alessio}, date-added = {2014-04-15 08:46:19 +0000}, date-modified = {2014-05-08 14:38:46 +0000}, keywords = {deep inference}, title = {The Commutative/Noncommutative Linear Logic BV}, url = {https://people.bath.ac.uk/ag248/p/CNLLBV.pdf}, year = {2014}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/CNLLBV.pdf}} @misc{Gugl:12:A-Person:yu, author = {Guglielmi, Alessio}, date-added = {2014-05-20 00:45:18 +0000}, date-modified = {2014-05-20 00:48:09 +0000}, keywords = {deep inference}, title = {A Personal Perspective on Deep Inference and Computer Science}, url = {https://people.bath.ac.uk/ag248/p/DICS.pdf}, year = {2012}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/DICS.pdf}} @article{GuglStra:02:A-Non-co:dq, author = {Guglielmi, Alessio and Straßburger, Lutz}, date-modified = {2014-04-11 00:30:07 +0000}, doi = {10.1017/S096012951100003X}, journal = {Mathematical Structures in Computer Science}, keywords = {deep inference}, number = {3}, pages = {563--584}, title = {A System of Interaction and Structure {V}: {T}he Exponentials and Splitting}, url = {http://www.lix.polytechnique.fr/~lutz/papers/NEL-splitting.pdf}, volume = {21}, year = {2011}, bdsk-url-1 = {http://www.lix.polytechnique.fr/~lutz/papers/NEL-splitting.pdf}, bdsk-url-2 = {http://dx.doi.org/10.1017/S096012951100003X}} @inproceedings{GuglGundPari::A-Proof-:fk, author = {Guglielmi, Alessio and Gundersen, Tom and Parigot, Michel}, booktitle = {21st International Conference on Rewriting Techniques and Applications (RTA)}, date-added = {2010-03-15 22:31:13 +0100}, date-modified = {2014-04-26 16:27:33 +0000}, doi = {10.4230/LIPIcs.RTA.2010.135}, editor = {Lynch, Christopher}, keywords = {deep inference}, pages = {135--150}, publisher = {Schloss Dagstuhl--Leibniz-Zentrum für Informatik}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, title = {A Proof Calculus Which Reduces Syntactic Bureaucracy}, url = {http://drops.dagstuhl.de/opus/volltexte/2010/2649}, volume = {6}, year = {2010}, bdsk-url-1 = {http://drops.dagstuhl.de/opus/volltexte/2010/2649}, bdsk-url-2 = {http://dx.doi.org/10.4230/LIPIcs.RTA.2010.135}} @inproceedings{GuglGundStra::Breaking:uq, author = {Guglielmi, Alessio and Gundersen, Tom and Straßburger, Lutz}, booktitle = {25th Annual IEEE Symposium on Logic in Computer Science (LICS)}, date-added = {2010-01-25 09:14:10 +0100}, date-modified = {2014-04-12 10:11:00 +0000}, doi = {10.1109/LICS.2010.12}, editor = {Jouannaud, Jean-Pierre}, keywords = {deep inference}, pages = {284--293}, publisher = {IEEE}, title = {Breaking Paths in Atomic Flows for Classical Logic}, url = {http://www.lix.polytechnique.fr/~lutz/papers/AFII.pdf}, year = {2010}, bdsk-url-1 = {http://www.lix.polytechnique.fr/~lutz/papers/AFII.pdf}, bdsk-url-2 = {http://dx.doi.org/10.1109/LICS.2010.12}} @misc{Gugl:09:th.pl:rz, author = {Guglielmi, Alessio}, date-added = {2009-02-25 06:54:03 +0100}, date-modified = {2014-05-01 19:18:43 +0000}, keywords = {deep inference}, note = {Prolog program, available at \url{https://people.bath.ac.uk/ag248/p/th.pl}}, title = {Th.pl}, year = {2009}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/th.pl}} @article{GuglGund:07:Normalis:lr, author = {Guglielmi, Alessio and Gundersen, Tom}, date-added = {2007-03-03 11:45:55 +0000}, date-modified = {2017-08-13 13:58:09 +0000}, doi = {10.2168/LMCS-4(1:9)2008}, journal = {Logical Methods in Computer Science}, keywords = {deep inference}, number = {1}, pages = {9:1--36}, title = {Normalisation Control in Deep Inference Via Atomic Flows}, url = {https://lmcs.episciences.org/1081/pdf}, volume = {4}, year = {2008}, bdsk-url-1 = {http://www.lmcs-online.org/ojs/viewarticle.php?id=341}, bdsk-url-2 = {http://arxiv.org/pdf/0709.1205.pdf}, bdsk-url-3 = {http://dx.doi.org/10.2168/LMCS-4(1:9)2008}} @misc{GuglGund:08:Normalis:yu, author = {Guglielmi, Alessio and Gundersen, Tom}, date-added = {2008-02-22 16:16:51 +0000}, date-modified = {2015-04-13 09:47:03 +0000}, keywords = {deep inference}, title = {Normalisation Control in Deep Inference Via Atomic Flows {II}}, url = {https://people.bath.ac.uk/ag248/p/NormContrDIAtFl2.pdf}, year = {2008}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/NormContrDIAtFl2.pdf}} @article{Gugl:06:A-System:kl, author = {Guglielmi, Alessio}, date-modified = {2014-04-10 17:06:14 +0000}, doi = {10.1145/1182613.1182614}, journal = {ACM Transactions on Computational Logic}, keywords = {deep inference}, number = {1}, pages = {1:1--64}, title = {A System of Interaction and Structure}, url = {https://people.bath.ac.uk/ag248/p/SystIntStr.pdf}, volume = {8}, year = {2007}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/SystIntStr.pdf}, bdsk-url-2 = {http://dx.doi.org/10.1145/1182613.1182614}} @misc{Gugl:07:On-the-P:fk, author = {Guglielmi, Alessio}, date-added = {2007-08-12 09:31:38 +0200}, date-modified = {2014-05-04 12:15:28 +0000}, keywords = {deep inference}, note = {Prolog program, available at https://people.bath.ac.uk/ag248/p/PrComplDI.plg}, title = {On the Proof Complexity of Deep Inference---{C}onjecture}, year = {2007}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/PrComplDI.plg}} @misc{Gugl:06:Deep-Inf:ap, author = {Guglielmi, Alessio}, date-modified = {2014-05-08 14:38:36 +0000}, keywords = {deep inference}, title = {Deep Inference and the Calculus of Structures---{P}roject Report}, url = {https://people.bath.ac.uk/ag248/p/CalcStrPR.pdf}, year = {2006}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/CalcStrPR.pdf}} @misc{Gugl:05:Butterfl:mb, author = {Guglielmi, Alessio}, date-modified = {2014-05-08 14:38:21 +0000}, keywords = {deep inference}, title = {Butterflies}, url = {https://people.bath.ac.uk/ag248/p/AG7.pdf}, year = {2005}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/AG7.pdf}} @misc{Gugl:05:Some-New:eh, author = {Guglielmi, Alessio}, date-added = {2006-01-16 10:48:24 +0000}, date-modified = {2014-04-30 13:36:41 +0000}, keywords = {deep inference}, title = {Some News on Subatomic Logic}, url = {https://people.bath.ac.uk/ag248/p/AG16.pdf}, year = {2005}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/AG16.pdf}} @inproceedings{Gugl:05:The-Prob:nu, author = {Guglielmi, Alessio}, booktitle = {Structures and Deduction}, date-added = {2006-01-16 10:47:46 +0000}, date-modified = {2006-07-13 13:12:58 +0100}, editor = {Paola Bruscoli and François Lamarche and Charles Stewart}, keywords = {deep inference}, note = {ICALP Workshop. ISSN 1430-211X}, pages = {53--68}, publisher = {Technische Universität Dresden}, title = {The Problem of Bureaucracy and Identity of Proofs from the Perspective of Deep Inference}, url = {https://people.bath.ac.uk/ag248/p/AG14.pdf}, year = {2005}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/AG14.pdf}} @misc{Gugl:04:Formalis:am, author = {Guglielmi, Alessio}, date-modified = {2014-05-08 14:37:53 +0000}, keywords = {deep inference}, title = {Formalism {A}}, url = {https://people.bath.ac.uk/ag248/p/AG11.pdf}, year = {2004}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/AG11.pdf}} @misc{Gugl:04:Formalis:ea, author = {Guglielmi, Alessio}, date-added = {2006-01-16 10:48:21 +0000}, date-modified = {2014-05-08 14:38:00 +0000}, keywords = {deep inference}, title = {Formalism {B}}, url = {https://people.bath.ac.uk/ag248/p/AG13.pdf}, year = {2004}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/AG13.pdf}} @misc{Gugl:04:Polynomi:zi, author = {Guglielmi, Alessio}, date-modified = {2014-05-08 14:38:13 +0000}, keywords = {deep inference}, title = {Polynomial Size Deep-Inference Proofs Instead of Exponential Size Shallow-Inference Proofs}, url = {https://people.bath.ac.uk/ag248/p/AG12.pdf}, year = {2004}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/AG12.pdf}} @misc{Gugl:03:Mismatch:pt, author = {Guglielmi, Alessio}, date-modified = {2014-05-08 14:37:16 +0000}, keywords = {deep inference}, title = {Mismatch}, url = {https://people.bath.ac.uk/ag248/p/AG9.pdf}, year = {2003}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/AG9.pdf}} @misc{Gugl:03:Normalis:tf, author = {Guglielmi, Alessio}, date-modified = {2014-05-08 14:37:28 +0000}, keywords = {deep inference}, title = {Normalisation Without Cut Elimination}, url = {https://people.bath.ac.uk/ag248/p/AG6.pdf}, year = {2003}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/AG6.pdf}} @misc{Gugl:03:Resoluti:ce, author = {Guglielmi, Alessio}, date-modified = {2014-05-08 14:37:40 +0000}, keywords = {deep inference}, title = {Resolution in the Calculus of Structures}, url = {https://people.bath.ac.uk/ag248/p/AG10.pdf}, year = {2003}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/AG10.pdf}} @inproceedings{GuglStra:02:A-Non-co:lq, author = {Guglielmi, Alessio and Straßburger, Lutz}, booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning (LPAR)}, date-modified = {2014-04-11 00:52:55 +0000}, doi = {10.1007/3-540-36078-6\_16}, editor = {Baaz, Matthias and Voronkov, Andrei}, keywords = {deep inference}, pages = {231--246}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {A Non-commutative Extension of {MELL}}, url = {http://www.lix.polytechnique.fr/~lutz/papers/NEL.pdf}, volume = {2514}, year = {2002}, bdsk-url-1 = {http://www.lix.polytechnique.fr/~lutz/papers/NEL.pdf}, bdsk-url-2 = {http://dx.doi.org/10.1007/3-540-36078-6%5C_16}} @misc{Gugl:02:Goodness:ti, author = {Guglielmi, Alessio}, date-modified = {2014-05-08 14:36:49 +0000}, keywords = {deep inference}, title = {Goodness, Perfection and Miracles}, url = {https://people.bath.ac.uk/ag248/p/AG1.pdf}, year = {2002}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/AG1.pdf}} @misc{Gugl:02:On-Lafon:iq, author = {Guglielmi, Alessio}, date-modified = {2014-05-08 14:36:59 +0000}, keywords = {deep inference}, title = {On {L}afont's Counterexample}, url = {https://people.bath.ac.uk/ag248/p/AG5.pdf}, year = {2002}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/AG5.pdf}} @misc{Gugl:02:Recipe:xv, author = {Guglielmi, Alessio}, date-modified = {2014-05-08 14:37:09 +0000}, keywords = {deep inference}, title = {Recipe}, url = {https://people.bath.ac.uk/ag248/p/AG2.pdf}, year = {2002}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/AG2.pdf}} @misc{Gugl:02:Subatomi:oh, author = {Guglielmi, Alessio}, date-modified = {2014-04-30 13:36:57 +0000}, keywords = {deep inference}, title = {Subatomic Logic}, url = {https://people.bath.ac.uk/ag248/p/AG8.pdf}, year = {2002}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/AG8.pdf}} @inproceedings{GuglStra:01:Non-comm:rp, author = {Guglielmi, Alessio and Straßburger, Lutz}, booktitle = {Computer Science Logic (CSL)}, date-modified = {2014-05-20 03:34:19 +0000}, doi = {10.1007/3-540-44802-0\_5}, editor = {L. Fribourg}, keywords = {deep inference}, pages = {54--68}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {Non-commutativity and {MELL} in the Calculus of Structures}, url = {https://people.bath.ac.uk/ag248/p/NoncMELLCoS.pdf}, volume = {2142}, year = {2001}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/NoncMELLCoS.pdf}, bdsk-url-2 = {http://dx.doi.org/10.1007/3-540-44802-0%5C_5}} @techreport{Gugl:99:A-Calcul:jk, author = {Guglielmi, Alessio}, date-added = {2014-05-06 07:40:59 +0000}, date-modified = {2014-05-06 07:42:55 +0000}, institution = {Technische Universität Dresden}, keywords = {deep inference}, number = {WV-99-04}, title = {A Calculus of Order and Interaction}, year = {1999}} @article{Guir:06:The-Thre:qt, author = {Guiraud, Yves}, date-modified = {2016-12-31 19:18:19 +0000}, doi = {10.1016/j.apal.2005.12.012}, journal = {Annals of Pure and Applied Logic}, keywords = {deep inference}, number = {1-2}, pages = {266--295}, title = {The Three Dimensions of Proofs}, url = {https://www.irif.fr/~guiraud/recherche/cos1.pdf}, volume = {141}, year = {2006}, bdsk-url-1 = {http://www.loria.fr/~guiraudy/recherche/cos1.pdf}} @inproceedings{Guir:05:The-Thre:ja, author = {Guiraud, Yves}, booktitle = {Structures and Deduction}, date-modified = {2006-07-13 13:12:59 +0100}, editor = {Paola Bruscoli and François Lamarche and Charles Stewart}, keywords = {deep inference}, note = {ICALP Workshop. ISSN 1430-211X}, pages = {35--52}, publisher = {Technische Universität Dresden}, title = {The Three Dimensions of Proofs}, url = {http://cs.bath.ac.uk/pb/SD05/SD05-Proc.pdf}, year = {2005}, bdsk-url-1 = {http://cs.bath.ac.uk/pb/SD05/SD05-Proc.pdf}} @inproceedings{GundHeijPari:13:A-Proof-:kx, author = {Gundersen, Tom and Heijltjes, Willem and Parigot, Michel}, booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-19)}, date-added = {2014-04-14 17:14:39 +0000}, date-modified = {2014-12-04 21:10:10 +0000}, doi = {10.1007/978-3-642-45221-5\_24}, editor = {McMillan, Ken and Middeldorp, Aart and Voronkov, Andrei}, keywords = {deep inference}, pages = {340--354}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {A Proof of Strong Normalisation of the Typed Atomic Lambda-Calculus}, url = {http://www.cs.bath.ac.uk/~wbh22/pdf/strong-normalisation-atomic-lambda-gundersen-heijltjes-parigot-2013.pdf}, volume = {8312}, year = {2013}, bdsk-url-1 = {http://www.cs.bath.ac.uk/~wbh22/docs/SN_atomic_lambda.pdf}, bdsk-url-2 = {http://dx.doi.org/10.1007/978-3-642-45221-5%5C_24}} @inproceedings{GundHeijPari:13:Atomic-L:fk, author = {Gundersen, Tom and Heijltjes, Willem and Parigot, Michel}, booktitle = {28th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)}, date-added = {2013-03-23 11:39:59 +0000}, date-modified = {2020-12-09 20:03:27 +0000}, doi = {10.1109/LICS.2013.37}, editor = {Kupferman, Orna}, keywords = {deep inference}, pages = {311--320}, publisher = {IEEE}, title = {Atomic Lambda Calculus: {A} Typed Lambda-Calculus with Explicit Sharing}, url = {http://opus.bath.ac.uk/34527/1/AL.pdf}, year = {2013}, bdsk-url-1 = {http://opus.bath.ac.uk/34527/1/AL.pdf}, bdsk-url-2 = {http://dx.doi.org/10.1109/LICS.2013.37}} @phdthesis{Gund:09:A-Genera:kx, author = {Gundersen, Tom}, date-added = {2009-08-09 11:17:28 +0200}, date-modified = {2016-06-13 06:13:51 +0000}, keywords = {deep inference}, school = {University of Bath}, title = {A General View of Normalisation Through Atomic Flows}, url = {https://tel.archives-ouvertes.fr/file/index/docid/509241/filename/thesis.pdf}, year = {2009}, bdsk-url-1 = {http://tel.archives-ouvertes.fr/docs/00/50/92/41/PDF/thesis.pdf}} @phdthesis{He:18:The-Atom:nx, author = {He, Fanny}, date-added = {2018-07-13 16:46:33 +0000}, date-modified = {2018-07-13 17:20:52 +0000}, keywords = {deep inference}, school = {University of Bath}, title = {The Atomic Lambda-Mu Calculus}, url = {https://fh341.github.io/pdf/HE-Thesis.pdf}, year = {2018}, bdsk-url-1 = {http://people.bath.ac.uk/fh341/pdf/HE-Thesis.pdf}} @mastersthesis{Hein:05:Geometri:bs, author = {Hein, Robert}, date-modified = {2006-07-13 13:12:56 +0100}, keywords = {deep inference}, school = {Technische Universität Dresden}, title = {Geometric Theories and Modal Logic in the Calculus of Structures}, url = {http://bitschnitzer.de/robert_thesis.ps.gz}, year = {2005}, bdsk-url-1 = {http://bitschnitzer.de/robert_thesis.ps.gz}} @inproceedings{HeinStew:05:Purity-T:tg, author = {Hein, Robert and Stewart, Charles}, booktitle = {Structures and Deduction}, date-modified = {2006-07-13 13:12:58 +0100}, editor = {Paola Bruscoli and François Lamarche and Charles Stewart}, keywords = {deep inference}, note = {ICALP Workshop. ISSN 1430-211X}, pages = {126--143}, publisher = {Technische Universität Dresden}, title = {Purity Through Unravelling}, url = {http://cs.bath.ac.uk/pb/SD05/SD05-Proc.pdf}, year = {2005}, bdsk-url-1 = {http://cs.bath.ac.uk/pb/SD05/SD05-Proc.pdf}} @inproceedings{Horn:19:The-Sub-:dg, author = {Horne, Ross}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD)}, date-added = {2019-11-10 20:27:47 +0000}, date-modified = {2019-11-10 20:32:11 +0000}, doi = {10.4230/LIPIcs.FSCD.2019.23}, editor = {Geuvers, Herman}, keywords = {deep inference}, pages = {23:1--16}, publisher = {Schloss Dagstuhl--Leibniz-Zentrum für Informatik}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, title = {The Sub-Additives: {A} Proof Theory for Probabilistic Choice Extending Linear Logic}, url = {http://drops.dagstuhl.de/opus/volltexte/2019/10530/pdf/LIPIcs-FSCD-2019-23.pdf}, volume = {131}, year = {2019}, bdsk-url-1 = {http://drops.dagstuhl.de/opus/volltexte/2019/10530/pdf/LIPIcs-FSCD-2019-23.pdf}, bdsk-url-2 = {https://doi.org/10.4230/LIPIcs.FSCD.2019.23}} @article{HornTiuAmanCiob:19:De-Morga:ng, author = {Horne, Ross and Tiu, Alwen and Aman, Bogdan and Ciobanu, Gabriel}, date-added = {2019-11-10 19:46:03 +0000}, date-modified = {2019-11-10 19:50:11 +0000}, doi = {10.1145/3325821}, journal = {ACM Transactions on Computational Logic}, keywords = {deep inference}, number = {4}, pages = {22:1--44}, title = {De Morgan Dual Nominal Quantifiers Modelling Private Names in Non-Commutative Logic}, volume = {20}, year = {2019}, bdsk-url-1 = {https://doi.org/10.1145/3325821}} @article{HornTiu:19:Construc:ft, author = {Horne, Ross and Tiu, Alwen}, date-added = {2019-04-04 18:33:13 +0100}, date-modified = {2019-11-10 18:04:42 +0000}, doi = {10.1017/S0960129518000452}, journal = {Mathematical Structures in Computer Science}, keywords = {deep inference}, number = {8}, pages = {1275--1308}, title = {Constructing Weak Simulations from Linear Implications for Processes with Private Names}, url = {https://satoss.uni.lu/members/ross/pdf/MSCS.pdf}, volume = {29}, year = {2019}, bdsk-url-1 = {https://doi.org/10.1017/S0960129518000452}} @article{HornMauwTiu:17:Semantic:vh, author = {Horne, Ross and Mauw, Sjouke and Tiu, Alwen}, date-added = {2019-04-04 22:23:35 +0100}, date-modified = {2019-04-04 22:27:34 +0100}, doi = {10.3233/FI-2017-1531}, journal = {Fundamenta Informaticae}, keywords = {deep inference}, number = {1-2}, pages = {57--86}, title = {Semantics for Specialising Attack Trees based on Linear Logic}, url = {http://orbilu.uni.lu/bitstream/10993/34365/1/HMT17.pdf}, volume = {153}, year = {2017}, bdsk-url-1 = {http://orbilu.uni.lu/bitstream/10993/34365/1/HMT17.pdf}, bdsk-url-2 = {https://doi.org/10.3233/FI-2017-1531}} @inproceedings{HornTiuCiob:16:Private-:ty, author = {Horne, Ross and Tiu, Alwen and Aman, Bogdan and Ciobanu, Gabriel}, booktitle = {27th International Conference on Concurrency Theory (CONCUR)}, date-added = {2016-06-30 12:45:07 +0000}, date-modified = {2019-04-04 18:23:16 +0100}, doi = {10.4230/LIPIcs.CONCUR.2016.31}, editor = {Desharnais, Josée and Jagadeesan, Radha}, keywords = {deep inference}, pages = {31:1--16}, publisher = {Schloss Dagstuhl--Leibniz-Zentrum für Informatik}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, title = {Private Names in Non-Commutative Logic}, url = {http://drops.dagstuhl.de/opus/volltexte/2016/6175/pdf/LIPIcs-CONCUR-2016-31.pdf}, volume = {59}, year = {2016}, bdsk-url-1 = {http://www.ntu.edu.sg/home/rhorne/p31-Horne.pdf}} @article{Horn:15:The-cons:ul, author = {Horne, Ross}, date-added = {2016-06-30 12:55:59 +0000}, date-modified = {2019-04-04 18:22:38 +0100}, doi = {10.7561/SACS.2015.2.245}, journal = {Scientific Annals of Computer Science}, keywords = {deep inference}, number = {2}, pages = {245--316}, title = {The Consistency and Complexity of {M}ultiplicative {A}dditive {S}ystem {V}irtual}, url = {http://orbilu.uni.lu/bitstream/10993/37434/1/sacs.pdf}, volume = {25}, year = {2015}, bdsk-url-1 = {http://www.ntu.edu.sg/home/rhorne/sacs.pdf}, bdsk-url-2 = {http://dx.doi.org/10.7561/SACS.2015.2.245}} @mastersthesis{Hors:06:The-Logi:fk, author = {Horsfall, Benjamin Robert}, date-added = {2007-09-08 07:07:08 +0100}, date-modified = {2016-06-17 12:20:49 +0000}, keywords = {deep inference}, school = {University of Melbourne}, title = {The Logic of Bunched Implications: {A} Memoir}, url = {https://minerva-access.unimelb.edu.au/bitstream/handle/11343/39480/72729_00002633_01_horsfall-mcs.pdf?sequence=1}, year = {2006}, bdsk-url-1 = {http://www.cs.mu.oz.au/~horsfall/horsfall-mcs.pdf}} @inproceedings{HughStraWu:21:Combinat:ja, author = {Hughes, Dominic J.D. and Straßburger, Lutz and Wu, Jui-Hsuan}, booktitle = {36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)}, date-added = {2022-11-02 19:39:44 +0000}, date-modified = {2022-11-02 19:39:44 +0000}, doi = {10.1109/lics52264.2021.9470579}, editor = {Libkin, Leonid}, keywords = {deep inference}, pages = {1--13}, publisher = {IEEE}, title = {Combinatorial Proofs and Decomposition Theorems for First-Order Logic}, url = {https://hal.inria.fr/hal-03369764/document}, year = {2021}, bdsk-url-1 = {https://doi.org/10.1109/lics52264.2021.9470579}} @misc{Hugh:04:Deep-Inf:fc, author = {Hughes, Dominic J.D.}, date-modified = {2014-05-08 14:39:24 +0000}, keywords = {deep inference}, title = {Deep Inference Proof Theory Equals Categorical Proof Theory Minus Coherence}, url = {http://boole.stanford.edu/~dominic/papers/di/di.pdf}, year = {2004}, bdsk-url-1 = {http://boole.stanford.edu/~dominic/papers/di/di.pdf}} @article{Japa:20:Elementa:ly, author = {Japaridze, Giorgi}, date-added = {2021-12-23 17:06:01 +0000}, date-modified = {2021-12-23 17:08:54 +0000}, doi = {10.1093/jigpal/jzaa022}, journal = {Logic Journal of the {IGPL}}, keywords = {deep inference}, number = {5}, title = {Elementary-Base Cirquent Calculus II: {C}hoice Quantifiers}, url = {https://arxiv.org/pdf/1902.07123.pdf}, volume = {29}, year = {2020}, bdsk-url-1 = {https://arxiv.org/pdf/1902.07123.pdf}, bdsk-url-2 = {https://doi.org/10.1093/jigpal/jzaa022}} @article{Japa:18:Elementa:zo, author = {Japaridze, Giorgi}, date-added = {2020-12-09 20:13:55 +0000}, date-modified = {2020-12-09 20:20:21 +0000}, journal = {Journal of Applied Logics}, keywords = {deep inference}, number = {1}, pages = {367--387}, title = {Elementary-Base Cirquent Calculus I: {P}arallel and Choice Connectives}, url = {https://arxiv.org/abs/1707.04823}, volume = {5}, year = {2018}, bdsk-url-1 = {https://arxiv.org/abs/1707.04823}} @article{Japa:07:Cirquent:fk, author = {Japaridze, Giorgi}, date-added = {2007-09-22 14:52:39 +0100}, date-modified = {2016-06-13 05:50:14 +0000}, doi = {10.1093/logcom/exn019}, journal = {Journal of Logic and Computation}, keywords = {deep inference}, number = {6}, pages = {983--1028}, title = {Cirquent Calculus Deepened}, url = {http://arxiv.org/pdf/0709.1308.pdf}, volume = {18}, year = {2008}, bdsk-url-1 = {http://arxiv.org/pdf/0709.1308}, bdsk-url-2 = {http://dx.doi.org/10.1093/logcom/exn019}} @article{Jera::On-the-C:kx, author = {Jeřábek, Emil}, date-added = {2007-12-02 20:34:04 +0000}, date-modified = {2016-06-13 06:15:36 +0000}, doi = {10.1093/logcom/exn054}, journal = {Journal of Logic and Computation}, keywords = {deep inference}, number = {2}, pages = {323--339}, title = {Proof Complexity of the Cut-Free Calculus of Structures}, url = {http://users.math.cas.cz/~jerabek/papers/cos.pdf}, volume = {19}, year = {2009}, bdsk-url-1 = {http://www.math.cas.cz/~jerabek/papers/cos.pdf}, bdsk-url-2 = {http://dx.doi.org/10.1093/logcom/exn054}} @article{Join:07:Complete:uq, author = {Joinet, Jean-Baptiste}, date-modified = {2016-06-12 10:40:58 +0000}, doi = {10.2178/jsl/1174668390}, journal = {Journal of Symbolic Logic}, keywords = {deep inference}, number = {1}, pages = {159--170}, title = {Completeness of {MLL} Proof-nets w.r.t.\ Weak Distributivity}, url = {http://www-philo.univ-paris1.fr/Joinet/NEW/PDF/PublicationsVersionOK/10-ok-WeakDistrib.pdf}, volume = {72}, year = {2007}, bdsk-url-1 = {http://www-philo.univ-paris1.fr/Joinet/joinetJSLmain.pdf}} @inproceedings{Join:05:Complete:os, author = {Joinet, Jean-Baptiste}, booktitle = {Structures and Deduction}, date-added = {2007-12-02 19:32:51 +0000}, date-modified = {2007-12-02 19:32:51 +0000}, editor = {Paola Bruscoli and François Lamarche and Charles Stewart}, keywords = {deep inference}, note = {ICALP Workshop. ISSN 1430-211X. Invited talk at WoLLIC '03 under the title `Calculus of Structures and Proof-Nets'}, pages = {81--94}, publisher = {Technische Universität Dresden}, title = {Completeness of {MLL} Proof-nets w.r.t.\ Weak Distributivity}, url = {http://cs.bath.ac.uk/pb/SD05/SD05-Proc.pdf}, year = {2005}, bdsk-url-1 = {http://cs.bath.ac.uk/pb/SD05/SD05-Proc.pdf}} @unpublished{Kahr::Labelled:ri, author = {Kahramanoğulları, Ozan}, date-modified = {2022-11-02 19:41:03 +0000}, keywords = {deep inference}, note = {Presented at the 1st World Congress on Universal Logic}, title = {Labeled Event Structure Semantics of Linear Logic Planning}, url = {https://people.bath.ac.uk/ag248/cl/ok/unilog.pdf}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/cl/ok/unilog.pdf}} @inproceedings{Kahr:17:Deep-Pro:fy, author = {Kahramanoğulları, Ozan}, booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-21)}, date-added = {2017-05-16 21:31:30 +0000}, date-modified = {2022-11-02 19:42:38 +0000}, editor = {Eiter, Thomas and Sands, David}, keywords = {deep inference}, pages = {106--124}, publisher = {EasyChair}, series = {EPiC Series in Computing}, title = {Deep Proof Search in {MELL}}, url = {https://easychair.org/publications/paper/q3S}, volume = {46}, year = {2017}, bdsk-url-1 = {http://easychair.org/publications/download/Deep_Proof_Search_in_MELL}} @inproceedings{Kahr:16:True-Con:kx, author = {Kahramanoğulları, Ozan}, booktitle = {23rd Workshop on Logic, Language, Information and Computation (WoLLIC)}, date-added = {2016-05-14 10:01:28 +0000}, date-modified = {2022-11-02 19:42:35 +0000}, doi = {10.1007/978-3-662-52921-8\_16}, editor = {Väänänen, Jouko and Hirvonen, Åsa and de Queiroz, Ruy}, keywords = {deep inference}, pages = {249--264}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {True Concurrency of Deep Inference Proofs}, url = {https://drive.google.com/file/d/0B150TbHH-gFtWVE0dGJMOVFEeTQ/view}, volume = {9803}, year = {2016}, bdsk-url-1 = {https://dl.dropboxusercontent.com/u/34033496/wollic2016.pdf}} @article{Kahr:08:Interact:ad, author = {Kahramanoğulları, Ozan}, date-added = {2008-07-01 11:53:32 +0100}, date-modified = {2022-11-02 19:42:32 +0000}, doi = {10.2168/LMCS-10(2:5)2014}, journal = {Logical Methods in Computer Science}, keywords = {deep inference}, number = {2}, pages = {5:1--49}, title = {Interaction and Depth Against Nondeterminism in Proof Search}, url = {http://arxiv.org/pdf/1403.2628.pdf}, volume = {10}, year = {2014}, bdsk-url-1 = {https://dl.dropbox.com/u/34033496/deep.pdf}} @article{Kahr:09:On-Linea:ix, author = {Kahramanoğulları, Ozan}, date-added = {2009-01-24 06:35:50 +0100}, date-modified = {2022-11-02 19:42:29 +0000}, doi = {10.1016/j.ic.2009.02.008}, journal = {Information and Computation}, keywords = {deep inference}, number = {11}, pages = {1229--1258}, publisher = {Elsevier}, title = {On Linear Logic Planning and Concurrency}, url = {http://www.sciencedirect.com/science/article/pii/S089054010900073X}, volume = {207}, year = {2009}, bdsk-url-1 = {http://www.sciencedirect.com/science/article/pii/S089054010900073X}} @unpublished{Kahr:08:Ingredie:bf, author = {Kahramanoğulları, Ozan}, date-added = {2008-07-01 11:55:42 +0100}, date-modified = {2022-11-02 19:42:26 +0000}, keywords = {deep inference}, note = {Short paper at CL\&C'08}, title = {Ingredients of a Deep Inference Theorem Prover}, url = {https://people.bath.ac.uk/ag248/cl/ok/ingredients.pdf}, year = {2008}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/cl/ok/ingredients.pdf}} @inproceedings{Kahr:07:Maude-as:lr, author = {Kahramanoğulları, Ozan}, booktitle = {Eighth International Workshop on Rule Based Programming (RULE 2007)}, date-added = {2007-06-26 09:53:26 +0100}, date-modified = {2022-11-02 19:42:23 +0000}, doi = {10.1016/j.entcs.2008.10.033}, editor = {J. Visser and V. Winter}, keywords = {deep inference}, pages = {35--50}, publisher = {Elsevier}, series = {Electronic Notes in Theoretical Computer Science}, title = {Maude as a Platform for Designing and Implementing Deep Inference Systems}, url = {https://people.bath.ac.uk/ag248/cl/ok/rule07.pdf}, volume = {219}, year = {2008}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/cl/ok/rule07.pdf}, bdsk-url-2 = {http://dx.doi.org/10.1016/j.entcs.2008.10.033}} @inproceedings{Kahr:08:On-Linea:fk, author = {Kahramanoğulları, Ozan}, booktitle = {Language and Automata Theory and Applications}, date-added = {2008-01-20 08:23:25 +0000}, date-modified = {2022-11-02 19:42:20 +0000}, doi = {10.1007/978-3-540-88282-4\_24}, editor = {Martín-Vide, Carlos and Otto, Friedrich and Fernau, Henning}, keywords = {deep inference}, pages = {250--262}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {On Linear Logic Planning and Concurrency}, url = {https://people.bath.ac.uk/ag248/cl/ok/lata.pdf}, volume = {5196}, year = {2008}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/cl/ok/lata.pdf}} @unpublished{Kahr:04:A-New-Lo:fk, author = {Kahramanoğulları, Ozan}, date-added = {2007-09-08 08:31:48 +0100}, date-modified = {2022-11-02 19:42:16 +0000}, keywords = {deep inference}, note = {Short paper at LPAR 2007}, title = {On Linear Logic Planning and Concurrency}, year = {2007}} @article{Kahr:07:System-B:fk, author = {Kahramanoğulları, Ozan}, date-added = {2007-03-24 13:01:58 +0000}, date-modified = {2022-11-02 19:42:12 +0000}, doi = {10.1016/j.apal.2007.11.005}, journal = {Annals of Pure and Applied Logic}, keywords = {deep inference}, number = {1--3}, pages = {107--121}, title = {System {BV} Is {NP}-Complete}, volume = {152}, year = {2007}, bdsk-url-1 = {http://dx.doi.org/10.1016/j.apal.2007.11.005}} @phdthesis{Kahr:06:Nondeter:fk, author = {Kahramanoğulları, Ozan}, date-added = {2007-08-13 18:00:14 +0200}, date-modified = {2022-11-02 19:42:09 +0000}, keywords = {deep inference}, school = {Technische Universität Dresden}, title = {Nondeterminism and Language Design in Deep Inference}, url = {https://people.bath.ac.uk/ag248/cl/ok/ozansthesis.pdf}, year = {2006}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/cl/ok/ozansthesis.pdf}} @inproceedings{Kahr:06:Reducing:hc, author = {Kahramanoğulları, Ozan}, booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning (LPAR)}, date-modified = {2022-11-02 19:42:05 +0000}, doi = {10.1007/11916277\_19}, editor = {Hermann, Miki and Voronkov, Andrei}, keywords = {deep inference}, pages = {272--286}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {Reducing Nondeterminism in the Calculus of Structures}, volume = {4246}, year = {2006}, bdsk-url-1 = {http://dx.doi.org/10.1007/11916277%5C_19}} @inproceedings{Kahr:06:System-B:ht, author = {Kahramanoğulları, Ozan}, booktitle = {12th Workshop on Logic, Language, Information and Computation (WoLLIC)}, date-modified = {2022-11-02 19:42:02 +0000}, doi = {10.1016/j.entcs.2005.05.026}, editor = {de Queiroz, Ruy and Macintyre, Angus and Bittencourt, Guilherme}, keywords = {deep inference}, pages = {87--99}, publisher = {Elsevier}, series = {Electronic Notes in Theoretical Computer Science}, title = {System {BV} Is {NP}-Complete}, url = {https://people.bath.ac.uk/ag248/cl/ok/BVnpc.pdf}, volume = {143}, year = {2006}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/cl/ok/BVnpc.pdf}} @inproceedings{KahrMoreReil:05:Implemen:wb, author = {Kahramanoğulları, Ozan and Moreau, Pierre-Etienne and Reilles, Antoine}, booktitle = {Structures and Deduction}, date-modified = {2022-11-02 19:41:58 +0000}, editor = {Paola Bruscoli and François Lamarche and Charles Stewart}, keywords = {deep inference}, note = {ICALP Workshop. ISSN 1430-211X}, pages = {158--172}, publisher = {Technische Universität Dresden}, title = {Implementing Deep Inference in {TOM}}, url = {https://people.bath.ac.uk/ag248/cl/ok/sd05.pdf}, year = {2005}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/cl/ok/sd05.pdf}} @inproceedings{Kahr:05:Towards-:uz, author = {Kahramanoğulları, Ozan}, booktitle = {Artificial Intelligence and Applications (AIA)}, date-modified = {2022-11-02 19:41:49 +0000}, editor = {Hamza, M.H.}, keywords = {deep inference}, pages = {197--202}, publisher = {ACTA Press}, title = {Towards Planning as Concurrency}, url = {https://people.bath.ac.uk/ag248/cl/ok/aia05.pdf}, year = {2005}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/cl/ok/aia05.pdf}} @inproceedings{Kahr:04:Implemen:ct, address = {Universit\'e Henri Poincar\'e, Nancy, France}, author = {Kahramanoğulları, Ozan}, booktitle = {ESSLLI 2004 Student Session}, date-modified = {2022-11-02 19:41:45 +0000}, keywords = {deep inference}, note = {16th European Summer School in Logic, Language and Information}, pages = {117--127}, title = {Implementing System {BV} of the Calculus of Structures in {M}aude}, url = {https://people.bath.ac.uk/ag248/cl/ok/esslli04.pdf}, year = {2004}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/cl/ok/esslli04.pdf}} @inproceedings{Kahr:04:System-B:dg, author = {Kahramanoğulları, Ozan}, booktitle = {19th International Symposium on Computer and Information Sciences (ISCIS)}, date-modified = {2022-11-02 19:41:41 +0000}, doi = {10.1007/978-3-540-30182-0\_99}, editor = {C. Aykanat and T. Dayar and I. Körpeoğlu}, keywords = {deep inference}, pages = {986--995}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {System {BV} without the Equalities for Unit}, url = {https://people.bath.ac.uk/ag248/cl/ok/bvn.pdf}, volume = {3280}, year = {2004}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/cl/ok/bvn.pdf}} @article{KuznStra:18:Maehara-:wk, author = {Kuznets, Roman and Straßburger, Lutz}, date-added = {2019-04-04 22:07:38 +0100}, date-modified = {2019-04-04 22:14:19 +0100}, doi = {10.1007/s00153-018-0636-1}, journal = {Archive for Mathematical Logic}, keywords = {deep inference}, number = {3-4}, pages = {359--385}, title = {Maehara-Style Modal Nested Calculi}, url = {https://hal.inria.fr/hal-01942240/document}, volume = {58}, year = {2018}, bdsk-url-1 = {https://hal.inria.fr/hal-01942240/document}, bdsk-url-2 = {https://doi.org/10.1007/s00153-018-0636-1}} @article{Lama::Explorin:mw, author = {Lamarche, François}, date-added = {2006-06-11 12:09:02 +0100}, date-modified = {2016-12-31 18:23:41 +0000}, journal = {Theory and Applications of Categories}, keywords = {deep inference}, number = {17}, pages = {473--535}, title = {Exploring the Gap between Linear and Classical Logic}, url = {http://www.tac.mta.ca/tac/volumes/18/17/18-17.pdf}, volume = {18}, year = {2007}, bdsk-url-1 = {http://www.loria.fr/~lamarche/papers/Gap.pdf}} @article{LamaStra:06:From-Pro:et, author = {Lamarche, François and Straßburger, Lutz}, date-modified = {2016-06-13 05:52:42 +0000}, doi = {10.2168/LMCS-2(4:3)2006}, journal = {Logical Methods in Computer Science}, keywords = {deep inference}, number = {4}, pages = {3:1--44}, title = {From Proof Nets to the Free *-Autonomous Category}, url = {https://arxiv.org/pdf/cs/0605054.pdf}, volume = {2}, year = {2006}, bdsk-url-1 = {http://arxiv.org/pdf/cs.LO/0605054}} @inproceedings{LamaStra:05:Construc:qq, author = {Lamarche, François and Straßburger, Lutz}, booktitle = {20th Annual IEEE Symposium on Logic in Computer Science (LICS)}, date-modified = {2016-12-31 18:40:56 +0000}, doi = {10.1109/LICS.2005.13}, editor = {Panangaden, Prakash}, keywords = {deep inference}, pages = {209--218}, publisher = {IEEE}, title = {Constructing Free Boolean Categories}, url = {http://www.lix.polytechnique.fr/~lutz/papers/FreeBool-long.pdf}, year = {2005}, bdsk-url-1 = {http://www.lix.polytechnique.fr/~lutz/papers/FreeBool-long.pdf}} @inproceedings{LamaStra:05:Naming-P:ov, author = {Lamarche, François and Straßburger, Lutz}, booktitle = {Typed Lambda Calculi and Applications (TLCA)}, date-modified = {2016-12-31 10:09:03 +0000}, doi = {10.1007/11417170\_19}, editor = {Paweł Urzyczyn}, keywords = {deep inference}, pages = {246--261}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {Naming Proofs in Classical Propositional Logic}, url = {http://www.lix.polytechnique.fr/~lutz/papers/namingproofsCL.pdf}, volume = {3461}, year = {2005}, bdsk-url-1 = {http://www.lix.polytechnique.fr/~lutz/papers/namingproofsCL.pdf}} @article{LellPime:19:Modulari:fb, author = {Lellmann, Björn and Pimentel, Elaine}, date-added = {2019-04-04 22:17:27 +0100}, date-modified = {2019-04-04 22:22:43 +0100}, doi = {10.1145/3288757}, journal = {ACM Transactions on Computational Logic}, keywords = {deep inference}, number = {2}, pages = {7:1--46}, title = {Modularisation of Sequent Calculi for Normal and Non-Normal Modalities}, url = {https://arxiv.org/pdf/1702.08193.pdf}, volume = {20}, year = {2019}, bdsk-url-1 = {https://arxiv.org/pdf/1702.08193.pdf}, bdsk-url-2 = {https://doi.org/10.1145/3288757}} @inproceedings{LellOlarPime:17:A-Unifor:qr, author = {Lellmann, Björn and Olarte, Carlos and Pimentel, Elaine}, booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-21)}, date-added = {2019-04-04 17:51:05 +0100}, date-modified = {2019-04-05 12:37:35 +0100}, doi = {10.29007/93qg}, editor = {Eiter, Thomas and Sands, David}, keywords = {deep inference}, pages = {435--455}, publisher = {EasyChair}, series = {EPiC Series in Computing}, title = {A Uniform Framework for Substructural Logics with Modalities}, url = {https://easychair.org/publications/paper/d5zT}, volume = {46}, year = {2017}, bdsk-url-1 = {https://easychair.org/publications/paper/d5zT}} @inproceedings{LellPime:15:Proof-Se:jt, author = {Lellmann, Björn and Pimentel, Elaine}, booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-20)}, date-added = {2016-04-13 09:32:41 +0000}, date-modified = {2016-12-31 19:13:42 +0000}, doi = {10.1007/978-3-662-48899-7\_39}, editor = {Davis, Martin and Fehnker, Ansgar and McIver, Annabelle and Voronkov, Andrei}, keywords = {deep inference}, pages = {558--574}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {Proof Search in Nested Sequent Calculi}, url = {https://www.logic.at/staff/lellmann/static/publications/2015/2015LPAR.pdf}, volume = {9450}, year = {2015}, bdsk-url-1 = {https://www.logic.at/staff/lellmann/static/publications/2015/2015LPAR.pdf}, bdsk-url-2 = {http://dx.doi.org/10.1007/978-3-662-48899-7%5C_39}} @phdthesis{Leng:06:Normalis:uq, author = {Lengrand, Stéphane}, date-added = {2007-10-06 07:11:08 +0100}, date-modified = {2007-10-06 07:15:24 +0100}, keywords = {deep inference}, school = {Université Paris VII - Denis Diderot, University of St Andrews}, title = {Normalisation \& Equivalence in Proof Theory \& Type Theory}, url = {http://www.lix.polytechnique.fr/~lengrand/Work/Reports/MyThesis.pdf}, year = {2006}, bdsk-url-1 = {http://www.lix.polytechnique.fr/~lengrand/Work/Reports/MyThesis.pdf}} @misc{LengBrun:05:Getting-:fk, author = {Lengrand, Stéphane and Brünnler, Kai}, date-added = {2007-10-06 06:46:17 +0100}, date-modified = {2014-05-08 14:39:43 +0000}, keywords = {deep inference}, title = {Getting Formalisms {A} and {B} by Proof-Terms and Typing Systems}, url = {http://www.lix.polytechnique.fr/~lengrand/Work/Reports/DI.ps}, year = {2005}, bdsk-url-1 = {http://www.lix.polytechnique.fr/~lengrand/Work/Reports/DI.ps}} @article{Lyon:20:On-the-C:rw, author = {Lyon, Tim}, date-added = {2021-02-07 11:51:22 +0000}, date-modified = {2021-02-07 11:54:10 +0000}, doi = {10.1093/logcom/exaa078}, journal = {Journal of Logic and Computation}, keywords = {deep inference}, number = {1}, pages = {213--265}, title = {On the Correspondence Between Nested Calculi and Semantic Systems for Intuitionistic Logics}, url = {https://academic.oup.com/logcom/article-pdf/31/1/213/36178019/exaa078.pdf}, volume = {31}, year = {2021}, bdsk-url-1 = {https://academic.oup.com/logcom/article-pdf/31/1/213/36178019/exaa078.pdf}, bdsk-url-2 = {https://doi.org/10.1093/logcom/exaa078}} @inproceedings{LyonTiuGoreClou:20:Syntacti:hb, author = {Lyon, Tim and Tiu, Alwen and Goré, Rajeev and Clouston, Ranald}, booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL)}, date-added = {2020-12-09 19:42:49 +0000}, date-modified = {2020-12-09 19:47:32 +0000}, doi = {10.4230/LIPIcs.CSL.2020.28}, editor = {Fernández, Maribel and Muscholl, Anca}, keywords = {deep inference}, pages = {28:1--55}, publisher = {Schloss Dagstuhl--Leibniz-Zentrum für Informatik}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, title = {Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic via Nested Sequents}, url = {https://drops.dagstuhl.de/opus/volltexte/2020/11671/}, volume = {152}, year = {2020}, bdsk-url-1 = {https://drops.dagstuhl.de/opus/volltexte/2020/11671/}, bdsk-url-2 = {https://doi.org/10.4230/LIPIcs.CSL.2020.28}} @inproceedings{Lyon:21:Nested-S:qu, author = {Lyon, Tim S.}, booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux)}, date-added = {2022-11-02 19:39:44 +0000}, date-modified = {2022-11-02 19:39:44 +0000}, doi = {10.1007/978-3-030-86059-2\_24}, editor = {Das, Anupam and Negri, Sara}, keywords = {deep inference}, pages = {409--427}, publisher = {Springer}, series = {Lecture Notes in Artificial Intelligence}, title = {Nested Sequents for Intuitionistic Modal Logics via Structural Refinement}, url = {https://easychair.org/publications/preprint_download/1Cpt}, volume = {12842}, year = {2021}, bdsk-url-1 = {https://doi.org/10.1007/978-3-030-86059-2_24}} @inproceedings{MariStra:14:Label-fr:qv, author = {Marin, Sonia and Straßburger, Lutz}, booktitle = {Advances in Modal Logic (AiML)}, date-added = {2014-06-04 11:02:03 +0000}, date-modified = {2015-04-13 09:09:40 +0000}, editor = {Goré, Rajeev and Kooi, Barteld and Kurucz, Agi}, keywords = {deep inference}, pages = {387--406}, publisher = {College Publications}, title = {Label-free Modular Systems for Classical and Intuitionistic Modal Logics}, url = {http://www.lix.polytechnique.fr/~lutz/papers/modul-modal.pdf}, volume = {10}, year = {2014}, bdsk-url-1 = {http://www.lix.polytechnique.fr/~lutz/papers/modul-modal.pdf}} @phdthesis{Mrm-:06:Categori:ff, author = {McKinley, Richard}, date-added = {2006-03-18 10:08:56 +0000}, date-modified = {2017-09-17 12:07:49 +0000}, keywords = {deep inference}, school = {University of Bath}, title = {Categorical Models of First Order Classical Proofs}, url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.60.5125&rep=rep1&type=pdf}, year = {2006}, bdsk-url-1 = {http://www.cs.bath.ac.uk/~csprim/thesis.pdf}} @inproceedings{Mrm-:05:Classica:ye, author = {McKinley, Richard}, booktitle = {Structures and Deduction}, date-modified = {2017-09-17 12:16:04 +0000}, editor = {Paola Bruscoli and François Lamarche and Charles Stewart}, keywords = {deep inference}, note = {ICALP Workshop. ISSN 1430-211X}, pages = {19--33}, publisher = {Technische Universität Dresden}, title = {Classical Categories and Deep Inference}, url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.59.3889&rep=rep1&type=pdf}, year = {2005}, bdsk-url-1 = {http://www.cs.bath.ac.uk/~csprim/csl05.pdf}} @inproceedings{NguyStra:22:BV-and-P:fo, author = {Nguyễn, Lê Thành Dũng (Tito) and Straßburger, Lutz}, booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL)}, date-added = {2022-11-02 19:39:44 +0000}, date-modified = {2022-11-05 16:01:19 +0000}, doi = {10.4230/LIPICS.CSL.2022.32}, editor = {Manea, Florin and Simpson, Alex}, keywords = {deep inference}, pages = {32:1--17}, publisher = {Schloss Dagstuhl--Leibniz-Zentrum für Informatik}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, title = {BV and Pomset Logic Are Not the Same}, url = {https://drops.dagstuhl.de/opus/volltexte/2022/15752/pdf/LIPIcs-CSL-2022-32.pdf}, volume = {216}, year = {2022}, bdsk-url-1 = {https://drops.dagstuhl.de/opus/volltexte/2022/15752/}, bdsk-url-2 = {https://doi.org/10.4230/LIPICS.CSL.2022.32}} @article{NovaStra:13:On-the-P:bs, author = {Novaković, Novak and Straßburger, Lutz}, date-added = {2014-04-26 14:44:29 +0000}, date-modified = {2015-05-01 09:02:13 +0000}, doi = {10.1145/2701424}, journal = {ACM Transactions on Computational Logic}, keywords = {deep inference}, number = {3}, pages = {19:1--20}, title = {On the Power of Substitution in the Calculus of Structures}, url = {http://www.lix.polytechnique.fr/~lutz/papers/SubstCoS.pdf}, volume = {16}, year = {2015}, bdsk-url-1 = {http://www.lix.polytechnique.fr/~lutz/papers/SubstCoS.pdf}} @inproceedings{OmidStra:22:Combinat:wb, author = {Omidvar, Giti and Straßburger, Lutz}, booktitle = {28th International Workshop on Logic, Language, Information, and Computation (WoLLIC)}, date-added = {2022-11-02 19:39:44 +0000}, date-modified = {2022-11-02 19:39:44 +0000}, doi = {10.1007/978-3-031-15298-6\_9}, editor = {Ciabattoni, Agata and Pimentel, Elaine and de Queiroz, Ruy J.G.B.}, keywords = {deep inference}, pages = {141--157}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {Combinatorial Flows as Bicolored Atomic Flows}, url = {https://www.lix.polytechnique.fr/Labo/Lutz.Strassburger/papers/Combinatorial_Flows.pdf}, volume = {13468}, year = {2022}, bdsk-url-1 = {https://doi.org/10.1007/978-3-031-15298-6_9}} @inproceedings{PimeRamaLell:19:Sequenti:jx, author = {Pimentel, Elaine and Ramanayake, Revantha and Lellmann, Björn}, booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux)}, date-added = {2019-11-10 19:51:38 +0000}, date-modified = {2019-11-10 20:00:56 +0000}, doi = {10.1007/978-3-030-29026-9\_9}, editor = {Cerrito, Serenella and Popescu, Andrei}, keywords = {deep inference}, pages = {147--165}, publisher = {Springer}, series = {Lecture Notes in Artificial Intelligence}, title = {Sequentialising Nested Systems}, url = {https://www.logic.at/staff/lellmann/static/publications/2019/2019TABLEAUXSEQ-NES.pdf}, volume = {11714}, year = {2019}, bdsk-url-1 = {https://www.logic.at/staff/lellmann/static/publications/2019/2019TABLEAUXSEQ-NES.pdf}, bdsk-url-2 = {https://doi.org/10.1007/978-3-030-29026-9%5C_9}} @phdthesis{Lind:11:Proof-Th:vn, author = {Postniece, Linda}, date-added = {2012-07-07 15:46:35 +0100}, date-modified = {2012-07-07 15:48:25 +0100}, keywords = {deep inference}, school = {The Australian National University}, title = {Proof Theory and Proof Search of Bi-Intuitionistic and Tense Logic}, url = {http://users.cecs.anu.edu.au/~linda/thesis.pdf}, year = {2011}, bdsk-url-1 = {http://users.cecs.anu.edu.au/~linda/thesis.pdf}} @inproceedings{Post:09:Deep-Inf:kx, author = {Linda Postniece}, booktitle = {16th Workshop on Logic, Language, Information and Computation (WoLLIC)}, date-added = {2009-06-12 06:25:08 +0200}, date-modified = {2016-12-31 10:12:47 +0000}, doi = {10.1007/978-3-642-02261-6\_26}, editor = {Ono, Hiroakira and Kanazawa, Makoto and de Queiroz, Ruy}, keywords = {deep inference}, pages = {320--334}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {Deep Inference in Bi-intuitionistic Logic}, url = {http://users.cecs.anu.edu.au/~linda/postniece-dbi.pdf}, volume = {5514}, year = {2009}, bdsk-url-1 = {http://users.cecs.anu.edu.au/~linda/postniece-dbi.pdf}} @article{Ralp:20:Herbrand:sz, author = {Ralph, Benjamin}, date-added = {2020-12-09 20:22:17 +0000}, date-modified = {2020-12-09 20:28:57 +0000}, doi = {10.1093/logcom/exaa052}, journal = {Journal of Logic and Computation}, keywords = {deep inference}, number = {8}, pages = {1711--1742}, title = {Herbrand Proofs and Expansion Proofs as Decomposed Proofs}, url = {https://academic.oup.com/logcom/article-pdf/30/8/1711/34673322/exaa052.pdf}, volume = {30}, year = {2020}, bdsk-url-1 = {https://academic.oup.com/logcom/article-pdf/30/8/1711/34673322/exaa052.pdf}, bdsk-url-2 = {https://doi.org/10.1093/logcom/exaa052}} @inproceedings{RalpStra:19:Towards-:ix, author = {Ralph, Benjamin and Straßburger, Lutz}, booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux)}, date-added = {2019-11-10 19:59:15 +0000}, date-modified = {2019-11-10 20:02:22 +0000}, doi = {10.1007/978-3-030-29026-9\_15}, editor = {Cerrito, Serenella and Popescu, Andrei}, keywords = {deep inference}, pages = {259--276}, publisher = {Springer}, series = {Lecture Notes in Artificial Intelligence}, title = {Towards a Combinatorial Proof Theory}, url = {https://people.bath.ac.uk/bdr25/files/CPT.pdf}, volume = {11714}, year = {2019}, bdsk-url-1 = {https://people.bath.ac.uk/bdr25/files/CPT.pdf}, bdsk-url-2 = {https://doi.org/10.1007/978-3-030-29026-9%5C_15}} @phdthesis{Ralp:19:Modular-:yq, author = {Ralph, Benjamin}, date-added = {2019-04-03 16:00:09 +0100}, date-modified = {2019-04-03 16:01:26 +0100}, keywords = {deep inference}, school = {University of Bath}, title = {Modular Normalisation of Classical Proofs}, url = {https://people.bath.ac.uk/ag248/br/phd.pdf}, year = {2019}, bdsk-url-1 = {https://people.bath.ac.uk/ag248/br/phd.pdf}} @inproceedings{Ralp:18:A-Natura:xe, author = {Ralph, Benjamin}, booktitle = {Logical Foundations of Computer Science (LFCS)}, date-added = {2017-10-21 07:28:22 +0000}, date-modified = {2019-04-03 15:34:25 +0100}, doi = {10.1007/978-3-319-72056-2\_18}, editor = {Artemov, Sergei and Nerode, Anil}, keywords = {deep inference}, pages = {289--308}, publisher = {Springer International Publishing}, series = {Lecture Notes in Computer Science}, title = {A Natural Proof System for Herbrand's Theorem}, url = {https://people.bath.ac.uk/ag248/br/prfsysht.pdf}, volume = {10703}, year = {2018}, bdsk-url-1 = {http://people.bath.ac.uk/bdr25/files/prfsysht.pdf}} @inproceedings{Reil:06:Canonica:fe, author = {Reilles, Antoine}, booktitle = {6th International Workshop on Rewriting Logic and Its Applications (WRLA 2006)}, date-added = {2006-03-28 18:48:42 +0100}, date-modified = {2016-12-31 18:34:44 +0000}, doi = {10.1016/j.entcs.2007.06.014}, keywords = {deep inference}, pages = {165--179}, publisher = {Elsevier}, series = {Electronic Notes in Theoretical Computer Science}, title = {Canonical Abstract Syntax Trees}, url = {https://arxiv.org/pdf/cs/0601019.pdf}, volume = {176}, year = {2007}, bdsk-url-1 = {http://arxiv.org/pdf/cs.PL/0601019}} @incollection{Reto:21:Pomset-L:fv, author = {Retoré, Christian}, booktitle = {Joachim Lambek: {T}he Interplay of Mathematics, Logic, and Linguistics}, date-added = {2021-12-23 14:14:42 +0000}, date-modified = {2021-12-23 14:58:26 +0000}, doi = {10.1007/978-3-030-66545-6\_9}, editor = {Casadio, Claudia and Scott, Philip J.}, keywords = {deep inference}, pages = {299--345}, publisher = {Springer}, series = {Outstanding Contributions to Logic}, title = {Pomset Logic}, volume = {20}, year = {2021}, bdsk-url-1 = {https://doi.org/10.1007/978-3-030-66545-6%5C_9}} @inproceedings{Reto:20:Flag:-A-:ig, author = {Retoré, Christian}, booktitle = {Linearity \& Trends in Linear Logic and Applications (Linearity\&TLLA)}, date-added = {2022-11-02 19:39:44 +0000}, date-modified = {2022-11-02 19:39:44 +0000}, doi = {10.4204/eptcs.353.8}, editor = {Dal Lago, Ugo and de Paiva, Valeria}, keywords = {deep inference}, pages = {157--174}, publisher = {Open Publishing Association}, series = {Electronic Proceedings in Theoretical Computer Science}, title = {Flag: {A} Self-Dual Modality for Non-Commutative Contraction and Duplication in the Category of Coherence Spaces}, url = {https://arxiv.org/pdf/2112.14961.pdf}, volume = {353}, year = {2020}, bdsk-url-1 = {https://doi.org/10.4204/eptcs.353.8}} @misc{Rove::Linear-L:fk, author = {Roversi, Luca}, date-added = {2010-11-28 16:09:08 +0000}, date-modified = {2016-06-13 06:02:44 +0000}, keywords = {deep inference}, title = {Linear Lambda Calculus with Explicit Substitutions as Proof-Search in Deep Inference}, url = {http://arxiv.org/pdf/1011.3668.pdf}, bdsk-url-1 = {http://arxiv.org/pdf/1011.3668}} @techreport{Rove:18:Subatomi:zp, author = {Roversi, Luca}, date-added = {2021-01-25 15:19:21 +0000}, date-modified = {2021-01-25 15:22:24 +0000}, institution = {Università di Torino}, keywords = {deep inference}, title = {Subatomic Systems Need Not Be Subatomic}, url = {https://arxiv.org/pdf/1804.08105.pdf}, year = {2018}, bdsk-url-1 = {https://arxiv.org/pdf/1804.08105.pdf}} @article{Rove:12:Extendin:uq, author = {Roversi, Luca}, date-added = {2013-03-07 14:14:31 +0000}, date-modified = {2016-04-13 09:08:46 +0000}, doi = {10.1093/logcom/exu033}, journal = {Journal of Logic and Computation}, keywords = {deep inference}, number = {2}, pages = {677--698}, title = {A Deep Inference System with a Self-Dual Binder Which Is Complete for Linear Lambda Calculus}, url = {http://www.di.unito.it/~rover/RESEARCH/PUBLICATIONS/2014-JLC/Roversi2014JLC.pdf}, volume = {26}, year = {2016}, bdsk-url-1 = {http://arxiv.org/pdf/1212.4483v1.pdf}, bdsk-url-2 = {http://www.di.unito.it/~rover/RESEARCH/PUBLICATIONS/2014-JLC/Roversi2014JLC.pdf}} @misc{Rove:12:Communic:kx, author = {Roversi, Luca}, date-added = {2013-03-07 14:28:39 +0000}, date-modified = {2014-05-08 14:40:14 +0000}, keywords = {deep inference}, title = {Communication, and Concurrency with Logic-Based Restriction Inside a Calculus of Structures}, url = {http://arxiv.org/pdf/1212.4669v1.pdf}, year = {2012}, bdsk-url-1 = {http://arxiv.org/pdf/1212.4669v1.pdf}} @inproceedings{Rove:11:Linear-L:kx, author = {Roversi, Luca}, booktitle = {Typed Lambda Calculi and Applications (TLCA)}, date-added = {2011-05-04 18:35:05 +0100}, date-modified = {2016-12-31 18:46:45 +0000}, doi = {10.1007/978-3-642-21691-6\_16}, editor = {Ong, Luke}, keywords = {deep inference}, pages = {184--197}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {Linear Lambda Calculus and Deep Inference}, url = {http://www.di.unito.it/~rover/RESEARCH/PUBLICATIONS/2011-TLCA/Roversi2011TLCA.pdf}, volume = {6690}, year = {2011}, bdsk-url-1 = {http://www.di.unito.it/~rover/RESEARCH/PUBLICATIONS/2011-TLCA/Roversi2011TLCA.pdf}, bdsk-url-2 = {http://dx.doi.org/10.1007/978-3-642-21691-6%5C_16}} @article{Sham:15:Nested-S:sj, author = {Shamkanov, Daniyar}, date-added = {2016-04-13 11:34:11 +0000}, date-modified = {2016-04-13 11:44:10 +0000}, doi = {10.1093/jigpal/jzv029}, journal = {Logic Journal of the {IGPL}}, keywords = {deep inference}, number = {5}, pages = {789--815}, title = {Nested Sequents for Provability Logic {GLP}}, url = {http://arxiv.org/pdf/1410.6652.pdf}, volume = {23}, year = {2015}, bdsk-url-1 = {http://arxiv.org/pdf/1410.6652.pdf}, bdsk-url-2 = {http://dx.doi.org/10.1093/jigpal/jzv029}} @inproceedings{SherHeijGundPari:20:Spinal-A:xu, author = {Sherratt, David and Heijltjes, Willem and Gundersen, Tom and Parigot, Michel}, booktitle = {Foundations of Software Science and Computation Structures (FoSSaCS)}, date-added = {2020-12-09 19:48:22 +0000}, date-modified = {2020-12-09 19:55:59 +0000}, doi = {10.1007/978-3-030-45231-5\_30}, editor = {Goubault-Larrecq, Jean and König, Barbara}, keywords = {deep inference}, pages = {582--601}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {Spinal Atomic Lambda-Calculus}, url = {http://www.cs.bath.ac.uk/~wbh22/pdf/2020-sherratt-heijltjes-gundersen-parigot.pdf}, volume = {12077}, year = {2020}, bdsk-url-1 = {http://www.cs.bath.ac.uk/~wbh22/pdf/2020-sherratt-heijltjes-gundersen-parigot.pdf}, bdsk-url-2 = {https://doi.org/10.1007/978-3-030-45231-5%5C_30}} @phdthesis{Sher:19:A-Lambda:ve, author = {Sherratt, David Rhys}, date-added = {2022-11-03 13:00:35 +0000}, date-modified = {2022-11-03 13:02:06 +0000}, keywords = {deep inference}, school = {University of Bath}, title = {A Lambda-Calculus That Achieves Full Laziness with Spine Duplication}, url = {https://purehost.bath.ac.uk/ws/portalfiles/portal/195822310/thesis_template.pdf}, year = {2019}, bdsk-url-1 = {https://purehost.bath.ac.uk/ws/portalfiles/portal/195822310/thesis_template.pdf}} @inproceedings{SimmKiss:22:Higher-O:rs, author = {Simmons, Will and Kissinger, Aleks}, booktitle = {47th International Symposium on Mathematical Foundations of Computer Science (MFCS)}, date-added = {2022-11-02 19:39:44 +0000}, date-modified = {2022-11-02 19:39:44 +0000}, doi = {10.4230/LIPIcs.MFCS.2022.80}, editor = {Szeider, Stefan and Ganian, Robert and Silva, Alexandra}, keywords = {deep inference}, pages = {80:1--14}, publisher = {Schloss Dagstuhl--Leibniz-Zentrum für Informatik}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, title = {Higher-Order Causal Theories Are Models of BV-Logic}, url = {https://drops.dagstuhl.de/opus/volltexte/2022/16878/pdf/LIPIcs-MFCS-2022-80.pdf}, volume = {241}, year = {2022}, bdsk-url-1 = {https://drops.dagstuhl.de/opus/volltexte/2022/16878/pdf/LIPIcs-MFCS-2022-80.pdf}, bdsk-url-2 = {https://doi.org/10.4230/LIPIcs.MFCS.2022.80}} @inproceedings{StewStou:05:A-System:tg, author = {Stewart, Charles and Stouppa, Phiniki}, booktitle = {Advances in Modal Logic (AiML)}, date-modified = {2014-04-26 17:06:13 +0000}, editor = {Renate Schmidt and Ian Pratt-Hartmann and Mark Reynolds and Heinrich Wansing}, keywords = {deep inference}, pages = {309--333}, publisher = {King's College Publications}, title = {A Systematic Proof Theory for Several Modal Logics}, url = {http://www.aiml.net/volumes/volume5/Stewart.ps}, volume = {5}, year = {2005}, bdsk-url-1 = {http://www.aiml.net/volumes/volume5/Stewart.ps}} @article{Stou:06:A-Deep-I:rt, author = {Stouppa, Phiniki}, date-modified = {2016-12-31 18:19:57 +0000}, doi = {10.1007/s11225-007-9028-y}, journal = {Studia Logica}, keywords = {deep inference}, number = {2}, pages = {199--214}, title = {A Deep Inference System for the Modal Logic {S5}}, url = {http://www.iam.unibe.ch/tilpub/2007/sto07.pdf}, volume = {85}, year = {2007}, bdsk-url-1 = {http://www.iam.unibe.ch/tilpub/2007/sto07.pdf}} @mastersthesis{Stou:04:The-Desi:vg, author = {Stouppa, Phiniki}, date-modified = {2008-01-28 14:42:34 +0000}, keywords = {deep inference}, school = {Technische Universität Dresden}, title = {The Design of Modal Proof Theories: The case of {S5}}, url = {http://www.wv.inf.tu-dresden.de/Publications/Diploma/diplom_stouppa.pdf}, year = {2004}, bdsk-url-1 = {http://www.wv.inf.tu-dresden.de/Publications/Diploma/diplom_stouppa.pdf}} @article{Stra:18:Deep-Inf:zf, author = {Straßburger, Lutz}, date-added = {2019-04-04 22:04:03 +0100}, date-modified = {2019-11-10 18:05:15 +0000}, doi = {10.1017/S0960129518000385}, journal = {Mathematical Structures in Computer Science}, keywords = {deep inference}, number = {8}, pages = {1030--1060}, title = {Deep Inference and Expansion Trees for Second-Order Multiplicative Linear Logic}, url = {https://hal.inria.fr/hal-01942410/document}, volume = {29}, year = {2019}, bdsk-url-1 = {https://hal.inria.fr/hal-01942410/document}, bdsk-url-2 = {https://doi.org/10.1017/S0960129518000385}} @inproceedings{Stra:17:Combinat:qf, author = {Straßburger, Lutz}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD)}, date-added = {2017-09-17 17:09:01 +0000}, date-modified = {2017-09-17 17:13:02 +0000}, doi = {10.4230/LIPIcs.FSCD.2017.31}, editor = {Miller, Dale}, keywords = {deep inference}, pages = {31:1--17}, publisher = {Schloss Dagstuhl--Leibniz-Zentrum für Informatik}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, title = {Combinatorial Flows and Their Normalisation}, url = {http://drops.dagstuhl.de/opus/volltexte/2017/7720/pdf/LIPIcs-FSCD-2017-31.pdf}, volume = {84}, year = {2017}, bdsk-url-1 = {http://drops.dagstuhl.de/opus/volltexte/2017/7720/pdf/LIPIcs-FSCD-2017-31.pdf}, bdsk-url-2 = {http://dx.doi.org/10.4230/LIPIcs.FSCD.2017.31}} @techreport{Stra:17:Combinat:zl, author = {Straßburger, Lutz}, date-added = {2017-04-02 08:27:04 +0000}, date-modified = {2017-04-02 08:41:38 +0000}, institution = {INRIA}, keywords = {deep inference}, number = {RR-9048}, title = {Combinatorial Flows and Proof Compression}, url = {https://hal.inria.fr/hal-01498468/document}, year = {2017}, bdsk-url-1 = {https://hal.inria.fr/hal-01498468/document}} @inproceedings{Stra:12:Nested-S:uq, author = {Straßburger, Lutz}, booktitle = {Foundations of Software Science and Computation Structures (FoSSaCS)}, date-added = {2012-07-07 13:24:04 +0100}, date-modified = {2014-04-26 14:58:04 +0000}, doi = {10.1007/978-3-642-37075-5\_14}, editor = {Pfenning, Frank}, keywords = {deep inference}, pages = {209--224}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {Cut Elimination in Nested Sequents for Intuitionistic Modal Logics}, url = {http://www.lix.polytechnique.fr/~lutz/papers/nested-int-mod-fossacs13.pdf}, volume = {7794}, year = {2013}, bdsk-url-1 = {http://www.lix.polytechnique.fr/~lutz/papers/nested-int-mod-fossacs13.pdf}, bdsk-url-2 = {http://dx.doi.org/10.1007/978-3-642-37075-5%5C_14}} @article{Stra:08:Extensio:kk, author = {Straßburger, Lutz}, date-added = {2008-07-01 11:58:02 +0100}, date-modified = {2014-04-12 10:44:11 +0000}, doi = {10.1016/j.apal.2012.07.004}, journal = {Annals of Pure and Applied Logic}, keywords = {deep inference}, number = {12}, pages = {1995--2007}, title = {Extension Without Cut}, url = {http://www.lix.polytechnique.fr/~lutz/papers/psppp.pdf}, volume = {163}, year = {2012}, bdsk-url-1 = {http://www.lix.polytechnique.fr/~lutz/papers/psppp.pdf}, bdsk-url-2 = {http://dx.doi.org/10.1016/j.apal.2012.07.004}} @article{StraGugl:09:A-System:vn, author = {Straßburger, Lutz and Guglielmi, Alessio}, date-added = {2009-03-30 09:16:04 +0200}, date-modified = {2016-06-13 06:04:32 +0000}, doi = {10.1145/1970398.1970399}, journal = {ACM Transactions on Computational Logic}, keywords = {deep inference}, number = {4}, pages = {23:1--39}, title = {A System of Interaction and Structure {IV}: {T}he Exponentials and Decomposition}, url = {http://arxiv.org/pdf/0903.5259.pdf}, volume = {12}, year = {2011}, bdsk-url-1 = {http://arxiv.org/pdf/0903.5259}, bdsk-url-2 = {http://dx.doi.org/10.1145/1970398.1970399}} @article{Stra:09:From-Dee:fr, author = {Straßburger, Lutz}, date-added = {2009-09-03 08:25:28 +0200}, date-modified = {2016-12-31 18:11:11 +0000}, doi = {10.1093/logcom/exp047}, journal = {Journal of Logic and Computation}, keywords = {deep inference}, number = {4}, pages = {589--624}, title = {From Deep Inference to Proof Nets Via Cut Elimination}, url = {http://www.lix.polytechnique.fr/~lutz/papers/deepnet.pdf}, volume = {21}, year = {2011}, bdsk-url-1 = {http://www.lix.polytechnique.fr/~lutz/papers/deepnet.pdf}} @unpublished{Stra:11:Towards-:fk, author = {Straßburger, Lutz}, date-added = {2011-01-17 14:26:13 +0000}, date-modified = {2011-01-17 14:27:45 +0000}, keywords = {deep inference}, note = {Habilitation Thesis}, school = {Université Paris VII - Denis Diderot}, title = {Towards a Theory of Proofs of Classical Logic}, url = {http://www.lix.polytechnique.fr/~lutz/papers/HDR.pdf}, year = {2011}, bdsk-url-1 = {http://www.lix.polytechnique.fr/~lutz/papers/HDR.pdf}} @inproceedings{Stra:10:What-Is-:fk, author = {Straßburger, Lutz}, booktitle = {Programs, Proofs, Processes---6th Conference on Computability in Europe}, date-added = {2010-07-17 18:29:43 +0200}, date-modified = {2016-12-31 10:08:21 +0000}, doi = {10.1007/978-3-642-13962-8\_45}, editor = {Ferreira, Fernando and Löwe, Benedikt and Mayordomo, Elvira and Mendes Gomes, Luís}, keywords = {deep inference}, pages = {406--416}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {What Is the Problem with Proof Nets for Classical Logic?}, url = {http://www.lix.polytechnique.fr/~lutz/papers/CiE10.pdf}, volume = {6158}, year = {2010}, bdsk-url-1 = {http://www.lix.polytechnique.fr/~lutz/papers/CiE10.pdf}} @inproceedings{Strasburger:2008qf, author = {Straßburger, Lutz}, booktitle = {Typed Lambda Calculi and Applications (TLCA)}, date-added = {2008-05-19 11:32:46 +0100}, date-modified = {2016-12-31 10:07:59 +0000}, doi = {10.1007/978-3-642-02273-9\_23}, editor = {Curien, Pierre-Louis}, keywords = {deep inference}, pages = {309--324}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {Some Observations on the Proof Theory of Second Order Propositional Multiplicative Linear Logic}, url = {http://www.lix.polytechnique.fr/~lutz/papers/ObsPT-MLL2-finalforTLCA09.pdf}, volume = {5608}, year = {2009}, bdsk-url-1 = {http://www.lix.polytechnique.fr/~lutz/papers/ObsPT-MLL2-finalforTLCA09.pdf}} @inproceedings{Stra:07:A-Charac:fk, author = {Straßburger, Lutz}, booktitle = {18th International Conference on Rewriting Techniques and Applications (RTA)}, date-modified = {2016-12-31 10:06:46 +0000}, doi = {10.1007/978-3-540-73449-9\_26}, editor = {Baader, Franz}, keywords = {deep inference}, pages = {344--358}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {A Characterisation of Medial as Rewriting Rule}, url = {http://www.lix.polytechnique.fr/~lutz/papers/CharMedial.pdf}, volume = {4533}, year = {2007}, bdsk-url-1 = {http://www.lix.polytechnique.fr/~lutz/papers/CharMedial.pdf}} @inproceedings{Stra:07:Deep-Inf:uq, author = {Straßburger, Lutz}, booktitle = {International Workshop on Hybrid Logic HyLo 2007}, date-added = {2007-08-26 12:31:10 +0100}, date-modified = {2007-08-26 12:39:44 +0100}, editor = {Jørgen Villadsen and Thomas Bolander and Torben Braüner}, keywords = {deep inference}, pages = {13--22}, title = {Deep Inference for Hybrid Logic}, url = {http://www.lix.polytechnique.fr/~lutz/papers/hybrid.pdf}, year = {2007}, bdsk-url-1 = {http://www.lix.polytechnique.fr/~lutz/papers/hybrid.pdf}} @article{Stra:06:On-the-A:jy, author = {Straßburger, Lutz}, date-modified = {2012-03-25 22:00:21 +0100}, journal = {Theory and Applications of Categories}, keywords = {deep inference}, number = {18}, pages = {536--601}, title = {On the Axiomatisation of Boolean Categories with and Without Medial}, url = {http://www.lix.polytechnique.fr/~lutz/papers/medial.pdf}, volume = {18}, year = {2007}, bdsk-url-1 = {http://www.lix.polytechnique.fr/~lutz/papers/medial.pdf}} @incollection{Stra:05:What-Is-:wl, author = {Straßburger, Lutz}, booktitle = {Logica Universalis---Towards a General Theory of Logic}, date-modified = {2008-01-15 06:56:32 +0000}, editor = {Jean-Yves Beziau}, keywords = {deep inference}, pages = {135--152}, publisher = {Birkhäuser}, title = {What Is a Logic, and What Is a Proof?}, url = {http://www.lix.polytechnique.fr/~lutz/papers/WhatLogicProof.pdf}, year = {2007}, bdsk-url-1 = {http://www.lix.polytechnique.fr/~lutz/papers/WhatLogicProof.pdf}} @techreport{Stra:06:Proof-Ne:fk, author = {Straßburger, Lutz}, date-added = {2007-10-10 11:01:54 +0100}, date-modified = {2016-06-13 06:18:49 +0000}, institution = {INRIA}, keywords = {deep inference}, number = {6013}, title = {Proof Nets and the Identity of Proofs}, url = {https://hal.inria.fr/file/index/docid/114320/filename/RR-6013.pdf}, year = {2006}, bdsk-url-1 = {http://hal.inria.fr/docs/00/11/43/20/PDF/RR-6013.pdf}} @unpublished{Stra:06:What-Cou:vh, author = {Straßburger, Lutz}, date-added = {2006-07-03 07:43:21 +0100}, date-modified = {2013-07-07 23:01:22 +0000}, keywords = {deep inference}, note = {Workshop Classical Logic and Computation colocated with ICALP 2006}, title = {What Could a Boolean Category Be?}, url = {http://www.lix.polytechnique.fr/~lutz/papers/medial-kurz.pdf}, year = {2006}, bdsk-url-1 = {http://www.lix.polytechnique.fr/~lutz/papers/medial-kurz.pdf}} @inproceedings{Stra:05:From-Dee:yb, author = {Straßburger, Lutz}, booktitle = {Structures and Deduction}, date-modified = {2009-09-03 09:01:47 +0200}, editor = {Paola Bruscoli and François Lamarche and Charles Stewart}, keywords = {deep inference}, note = {ICALP Workshop. ISSN 1430-211X}, pages = {2--18}, publisher = {Technische Universität Dresden}, title = {From Deep Inference to Proof Nets}, url = {http://www.lix.polytechnique.fr/~lutz/papers/deepnet-SD05.pdf}, year = {2005}, bdsk-url-1 = {http://www.lix.polytechnique.fr/~lutz/papers/deepnet-SD05.pdf}} @inproceedings{StraLama:04:On-Proof:ec, author = {Straßburger, Lutz and Lamarche, François}, booktitle = {Computer Science Logic (CSL)}, date-modified = {2016-12-31 10:07:12 +0000}, doi = {10.1007/978-3-540-30124-0\_14}, editor = {J. Marcinkowski and A. Tarlecki}, keywords = {deep inference}, pages = {145--159}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {On Proof Nets for Multiplicative Linear Logic with Units}, url = {http://www.lix.polytechnique.fr/~lutz/papers/multPN.pdf}, volume = {3210}, year = {2004}, bdsk-url-1 = {http://www.lix.polytechnique.fr/~lutz/papers/multPN.pdf}} @phdthesis{Stra:03:Linear-L:lp, author = {Straßburger, Lutz}, date-modified = {2006-07-13 13:12:57 +0100}, keywords = {deep inference}, school = {Technische Universität Dresden}, title = {Linear Logic and Noncommutativity in the Calculus of Structures}, url = {http://www.lix.polytechnique.fr/~lutz/papers/dissvonlutz.pdf}, year = {2003}, bdsk-url-1 = {http://www.lix.polytechnique.fr/~lutz/papers/dissvonlutz.pdf}} @article{Stra:03:MELL-in-:oy, author = {Straßburger, Lutz}, date-modified = {2016-12-31 18:20:39 +0000}, doi = {10.1016/S0304-3975(03)00240-8}, journal = {Theoretical Computer Science}, keywords = {deep inference}, pages = {213--285}, title = {{MELL} in the Calculus of Structures}, url = {http://www.lix.polytechnique.fr/~lutz/papers/els.pdf}, volume = {309}, year = {2003}, bdsk-url-1 = {http://www.lix.polytechnique.fr/~lutz/papers/els.pdf}} @inproceedings{Stra:03:System-N:mb, author = {Straßburger, Lutz}, booktitle = {10th Workshop on Logic, Language, Information and Computation (WoLLIC)}, date-added = {2007-03-29 10:00:53 +0100}, date-modified = {2016-12-31 09:53:24 +0000}, doi = {10.1016/S1571-0661(04)80853-3}, editor = {de Queiroz, Ruy and Pimentel, Elaine and Figueiredo, Lucília}, keywords = {deep inference}, pages = {166-177}, publisher = {Elsevier}, series = {Electronic Notes in Theoretical Computer Science}, title = {System {NEL} Is Undecidable}, url = {http://www.lix.polytechnique.fr/~lutz/papers/NELundec_wollic03.pdf}, volume = {84}, year = {2003}, bdsk-url-1 = {http://www.lix.polytechnique.fr/~lutz/papers/NELundec_wollic03.pdf}, bdsk-url-2 = {http://dx.doi.org/10.1016/S1571-0661(04)80853-3}} @techreport{Stra:03:The-Unde:gn, author = {Straßburger, Lutz}, date-modified = {2006-07-13 13:12:59 +0100}, institution = {Technische Universität Dresden}, keywords = {deep inference}, number = {WV-03-05}, title = {The Undecidability of System {NEL}}, url = {http://www.lix.polytechnique.fr/~lutz/papers/NELundeci.pdf}, year = {2003}, bdsk-url-1 = {http://www.lix.polytechnique.fr/~lutz/papers/NELundeci.pdf}} @techreport{Stra:02:A-Local-:ve, author = {Straßburger, Lutz}, date-modified = {2006-07-13 13:12:54 +0100}, institution = {Technische Universität Dresden}, keywords = {deep inference}, number = {WV-02-01}, title = {A Local System for Linear Logic}, url = {http://www.lix.polytechnique.fr/~lutz/papers/lls.pdf}, year = {2002}, bdsk-url-1 = {http://www.lix.polytechnique.fr/~lutz/papers/lls.pdf}} @inproceedings{Stra:02:A-Local-:ul, author = {Straßburger, Lutz}, booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning (LPAR)}, date-modified = {2016-12-31 10:07:36 +0000}, doi = {10.1007/3-540-36078-6\_26}, editor = {Baaz, Matthias and Voronkov, Andrei}, keywords = {deep inference}, pages = {388--402}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {A Local System for Linear Logic}, url = {http://www.lix.polytechnique.fr/~lutz/papers/lls-lpar.pdf}, volume = {2514}, year = {2002}, bdsk-url-1 = {http://www.lix.polytechnique.fr/~lutz/papers/lls-lpar.pdf}} @inproceedings{TiuIanoGore:12:Grammar-:uq, author = {Tiu, Alwen and Ianovski, Egor and Goré, Rajeev}, booktitle = {Advances in Modal Logic (AiML)}, date-added = {2012-07-08 16:35:55 +0100}, date-modified = {2014-04-26 17:06:13 +0000}, editor = {Bolander, Thomas and Braüner, Torben and Ghilardi, Silvio and Lawrence Moss}, keywords = {deep inference}, pages = {516--537}, publisher = {College Publications}, title = {Grammar Logics in Nested Sequent Calculus: {P}roof Theory and Decision Procedures}, url = {http://users.cecs.anu.edu.au/~tiu/papers/grammar.pdf}, volume = {9}, year = {2012}, bdsk-url-1 = {http://users.cecs.anu.edu.au/~tiu/papers/grammar.pdf}} @inproceedings{Tiu:06:A-Local-:gf, author = {Tiu, Alwen}, booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning (LPAR)}, date-modified = {2017-10-24 14:24:41 +0000}, doi = {10.1007/11916277\_17}, editor = {Hermann, Miki and Voronkov, Andrei}, keywords = {deep inference}, pages = {242--256}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {A Local System for Intuitionistic Logic}, url = {http://users.cecs.anu.edu.au/~tiu/papers/lpar06sub.pdf}, volume = {4246}, year = {2006}, bdsk-url-1 = {http://users.cecs.anu.edu.au/~tiu/localint.pdf}} @article{Tiu:06:A-System:ai, author = {Tiu, Alwen}, date-modified = {2016-06-13 06:20:05 +0000}, doi = {10.2168/LMCS-2(2:4)2006}, journal = {Logical Methods in Computer Science}, keywords = {deep inference}, number = {2}, pages = {4:1--24}, title = {A System of Interaction and Structure {II}: {T}he Need for Deep Inference}, url = {https://arxiv.org/pdf/cs/0512036.pdf}, volume = {2}, year = {2006}, bdsk-url-1 = {http://arxiv.org/pdf/cs.LO/0512036}, bdsk-url-2 = {http://arxiv.org/pdf/cs.LO/0512036.pdf}, bdsk-url-3 = {http://dx.doi.org/10.2168/LMCS-2(2:4)2006}} @techreport{Tiu:01:A1-Unifi:ij, author = {Tiu, Alwen Fernanto}, date-modified = {2017-10-24 13:46:29 +0000}, institution = {Technische Universität Dresden}, keywords = {deep inference}, number = {WV-01-08}, title = {{A1}-Unification}, url = {http://www.lix.polytechnique.fr/~tiu/a1.ps.gz}, year = {2001}, bdsk-url-1 = {http://users.cecs.anu.edu.au/~tiu/a1.ps.gz}} @techreport{Tiu:01:Combinin:qf, author = {Tiu, Alwen Fernanto}, date-modified = {2017-10-24 13:46:53 +0000}, institution = {Technische Universität Dresden}, keywords = {deep inference}, number = {WV-01-09}, title = {Combining {A1}- and {AC1}-Unification Sharing Unit}, url = {http://www.lix.polytechnique.fr/~tiu/comb4.ps.gz}, year = {2001}, bdsk-url-1 = {http://users.cecs.anu.edu.au/~tiu/comb4.ps.gz}} @techreport{Tiu:01:Properti:zk, author = {Tiu, Alwen Fernanto}, date-modified = {2017-10-24 13:47:21 +0000}, institution = {Technische Universität Dresden}, keywords = {deep inference}, number = {WV-01-06}, title = {Properties of a Logical System in the Calculus of Structures}, url = {http://www.lix.polytechnique.fr/~tiu/thesisc.pdf}, year = {2001}, bdsk-url-1 = {http://users.cecs.anu.edu.au/~tiu/thesisc.pdf}}