@article(andreoli92jlc,
 author       = {Jean{-}Marc Andreoli},
 year         = {1992},
 title        = {Logic Programming with Focusing Proofs in Linear Logic},
 journal      = {J. Log. Comput.},
 volume       = {2},
 number       = {3},
 pages        = {297--347},
 doi          = {10.1093/logcom/2.3.297},
)
@techreport(FILL,
 author       = {Torben Bra{\"{u}}ner and Valeria de Paiva},
 year         = {1996},
 title        = {Cut-Elimination for Full Intuitionistic Linear Logic},
 type         = {Technical Report},
 institution  = {BRICS Report Series},
)
@techreport(petri-LL,
 author       = {Iliano Cervesato},
 year         = {1994},
 title        = {Petri Nets as Multiset Rewriting Systems in a Linear Framework},
 type         = {Technical Report},
 institution  = {Dipartimento di Informatica. Universit\'{a} di Torino},
)
@inproceedings(DBLP:conf/agp/Cervesato95,
 author       = {Iliano Cervesato},
 year         = {1995},
 title        = {Petri Nets and Linear Logic: a Case Study for Logic Programming},
 editor       = {Mar{\'{\i}}a Alpuente and Maria I. Sessa},
 booktitle    = {1995 Joint Conference on Declarative Programming, GULP-PRODE'95, Marina di Vietri, Italy, September 11-14, 1995},
 pages        = {313--320},
)
@article(DBLP:journals/tcs/CervesatoHP00,
 author       = {Iliano Cervesato and Joshua S. Hodas and Frank Pfenning},
 year         = {2000},
 title        = {Efficient resource management for linear logic proof search},
 journal      = {Theor. Comput. Sci.},
 volume       = {232},
 number       = {1-2},
 pages        = {133--163},
 doi          = {10.1016/S0304-3975(99)00173-5},
)
@article(cervesato02ic,
 author       = {Iliano Cervesato and Frank Pfenning},
 year         = {2002},
 title        = {{A Linear Logical Framework}},
 journal      = {Information \& Computation},
 volume       = {179},
 number       = {1},
 pages        = {19--75},
 doi          = {10.1006/inco.2001.2951},
)
@inproceedings(DBLP:conf/cade/ChaudhuriP05,
 author       = {Kaustuv Chaudhuri and Frank Pfenning},
 year         = {2005},
 title        = {A Focusing Inverse Method Theorem Prover for First-Order Linear Logic},
 editor       = {Robert Nieuwenhuis},
 booktitle    = {Automated Deduction - CADE-20},
 series       = {LNCS},
 volume       = {3632},
 publisher    = {Springer},
 pages        = {69--83},
 doi          = {10.1007/11532231\_6},
)
@inproceedings(ChaudhuriR15,
 author       = {Kaustuv Chaudhuri and Giselle Reis},
 year         = {2015},
 title        = {An Adequate Compositional Encoding of Bigraph Structure in Linear Logic with Subexponentials},
 booktitle    = {LPAR-20},
 pages        = {146--161},
 doi          = {10.1007/978-3-662-48899-7\_11},
)
@article(DanosJS95,
 author       = {Vincent Danos and Jean{-}Baptiste Joinet and Harold Schellinx},
 year         = {1995},
 title        = {On the linear decoration of intuitionistic derivations},
 journal      = {Arch. Math. Log.},
 volume       = {33},
 number       = {6},
 pages        = {387--412},
 doi          = {10.1007/BF02390456},
)
@inproceedings(DBLP:conf/lfcs/GalmicheP94,
 author       = {Didier Galmiche and Guy Perrier},
 year         = {1994},
 title        = {Foundations of Proof Search Strategies Design in Linear Logic},
 editor       = {Anil Nerode and Yuri V. Matiyasevich},
 booktitle    = {Proc. of LFCS'94},
 series       = {LNCS},
 volume       = {813},
 publisher    = {Springer},
 pages        = {101--113},
 doi          = {10.1007/3-540-58140-5\_11},
)
@article(girard87tcs,
 author       = {Jean-Yves Girard},
 year         = {1987},
 title        = {Linear Logic},
 journal      = {Theoretical Computer Science},
 volume       = {50},
 pages        = {1--102},
 doi          = {10.1016/0304-3975(87)90045-4},
)
@book(klccne1952im,
 author       = {S. Kleene},
 year         = {1952},
 title        = {{Introduction to Metamathematics}},
 publisher    = {Van Nostrand, New York},
)
@inproceedings(Laurent18,
 author       = {Olivier Laurent},
 year         = {2018},
 title        = {Around Classical and Intuitionistic Linear Logics},
 editor       = {Anuj Dawar and Erich Gr{\"{a}}del},
 booktitle    = {Proceedings of {LICS}},
 publisher    = {{ACM}},
 pages        = {629--638},
 doi          = {10.1145/3209108.3209132},
)
@article(LiangM09,
 author       = {Chuck Liang and Dale Miller},
 year         = {2009},
 title        = {Focusing and polarization in linear, intuitionistic, and classical logics},
 journal      = {Theor. Comput. Sci.},
 volume       = {410},
 number       = {46},
 pages        = {4747--4768},
 doi          = {10.1016/j.tcs.2009.07.041},
)
@article(DBLP:journals/apal/LincolnMSS92,
 author       = {Patrick Lincoln and John C. Mitchell and Andre Scedrov and Natarajan Shankar},
 year         = {1992},
 title        = {Decision Problems for Propositional Linear Logic},
 journal      = {Annals of Pure and Applied Logic},
 volume       = {56},
 number       = {1-3},
 pages        = {239--311},
 doi          = {10.1016/0168-0072(92)90075-B},
)
@inproceedings(DBLP:conf/lpar/LopezP99,
 author       = {Pablo L{\'{o}}pez and Ernesto Pimentel},
 year         = {1999},
 title        = {Resource Management in Linear Logic Search Revisited},
 editor       = {Harald Ganzinger and David A. McAllester and Andrei Voronkov},
 booktitle    = {LPAR'99},
 series       = {LNCS},
 volume       = {1705},
 publisher    = {Springer},
 pages        = {304--319},
 doi          = {10.1007/3-540-48242-3\_19},
)
@inproceedings(DBLP:conf/ctcs/Marti-OlietM89,
 author       = {Mart{\'{\i}}{-}Oliet, Narciso and Jos{\'{e}} Meseguer},
 year         = {1989},
 title        = {From Petri Nets to Linear Logic},
 editor       = {David H. Pitt and David E. Rydeheard and Peter Dybjer and Andrew M. Pitts and Axel Poign{\'{e}}},
 booktitle    = {Category Theory and Computer Science},
 series       = {LNCS},
 volume       = {389},
 publisher    = {Springer},
 pages        = {313--340},
 doi          = {10.1007/BFb0018359},
)
@article(DBLP:journals/jlp/Meseguer12,
 author       = {Jos{\'{e}} Meseguer},
 year         = {2012},
 title        = {Twenty years of rewriting logic},
 journal      = {J. Log. Algebr. Program.},
 volume       = {81},
 number       = {7-8},
 pages        = {721--781},
 doi          = {10.1016/j.jlap.2012.06.003},
)
@article(MillerP13,
 author       = {Dale Miller and Elaine Pimentel},
 year         = {2013},
 title        = {A formal framework for specifying sequent calculus proof systems},
 journal      = {Theor. Comput. Sci.},
 volume       = {474},
 pages        = {98--116},
 doi          = {10.1016/j.tcs.2012.12.008},
)
@article(DBLP:journals/jolli/Mints93,
 author       = {Grigori Mints},
 year         = {1993},
 title        = {Resolution calculus for the first order linear logic},
 journal      = {Journal of Logic, Language and Information},
 volume       = {2},
 number       = {1},
 pages        = {59--83},
 doi          = {10.1007/BF01051768},
)
@article(Nigam2010,
 author       = {Vivek Nigam and Dale Miller},
 year         = {2010},
 title        = {{A Framework for Proof Systems}},
 journal      = {Journal of Automated Reasoning},
 volume       = {45},
 number       = {2},
 pages        = {157--188},
 doi          = {10.1007/s10817-010-9182-1},
)
@article(OlarteP17,
 author       = {Carlos Olarte and Elaine Pimentel},
 year         = {2017},
 title        = {On concurrent behaviors and focusing in linear logic},
 journal      = {Theor. Comput. Sci.},
 volume       = {685},
 pages        = {46--64},
 doi          = {10.1016/j.tcs.2016.08.026},
)
@inproceedings(qmltp2,
 author       = {Thomas Raths and Jens Otten},
 year         = {2012},
 title        = {The QMLTP problem library for first-order modal logics},
 booktitle    = {International Joint Conference on Automated Reasoning},
 pages        = {454--461},
 doi          = {10.1007/978-3-642-31365-3\_35},
)
@article(iltp,
 author       = {Thomas Raths and Jens Otten and Christoph Kreitz},
 year         = {2007},
 title        = {The ILTP problem library for intuitionistic logic},
 journal      = {Journal of Automated Reasoning},
 volume       = {38},
 number       = {1-3},
 pages        = {261--271},
 doi          = {10.1007/s10817-006-9060-z},
)
@book(DBLP:books/sp/Reisig85a,
 author       = {Wolfgang Reisig},
 year         = {1985},
 title        = {Petri Nets: An Introduction},
 series       = {{EATCS} Monographs on Theoretical Computer Science},
 volume       = {4},
 publisher    = {Springer},
 doi          = {10.1007/978-3-642-69968-9},
)
@article(Schellinx91,
 author       = {Harold Schellinx},
 year         = {1991},
 title        = {Some Syntactical Observations on Linear Logic},
 journal      = {J. Log. Comput.},
 volume       = {1},
 number       = {4},
 pages        = {537--559},
 doi          = {10.1093/logcom/1.4.537},
)
@article(Sut17,
 author       = {G. Sutcliffe},
 year         = {2017},
 title        = {{The TPTP Problem Library and Associated Infrastructure. From CNF to TH0, TPTP v6.4.0}},
 journal      = {Journal of Automated Reasoning},
 volume       = {59},
 number       = {4},
 pages        = {483--502},
 doi          = {10.1007/s10817-017-9407-7},
)
@article(DBLP:journals/jar/Tammet94,
 author       = {Tanel Tammet},
 year         = {1994},
 title        = {Proof Sytrategies in Linear Logic},
 journal      = {J. Autom. Reasoning},
 volume       = {12},
 number       = {3},
 pages        = {273--304},
 doi          = {10.1007/BF00885763},
)
@inproceedings(DBLP:conf/kgc/Tammet97,
 author       = {Tanel Tammet},
 year         = {1997},
 title        = {Resolution, Inverse Method and the Sequent Calculus},
 editor       = {Georg Gottlob and Alexander Leitsch and Daniele Mundici},
 booktitle    = {KGC'97},
 series       = {LNCS},
 volume       = {1289},
 publisher    = {Springer},
 pages        = {65--83},
 doi          = {10.1007/3-540-63385-5\_33},
)
@book(troelstra92csli,
 author       = {Anne S. Troelstra},
 year         = {1992},
 title        = {Lectures on Linear Logic},
 publisher    = {CSLI Lecture Notes 29, Center for the Study of Language and Information},
 address      = {Stanford, California},
)
@inproceedings(qmltp1,
 author       = {Max Wisniewski and Alexander Steen and Christoph Benzm{\"{u}}ller},
 year         = {2016},
 title        = {{TPTP} and Beyond: Representation of Quantified Non-Classical Logics},
 editor       = {Christoph Benzm{\"{u}}ller and Jens Otten},
 booktitle    = {Proceedings of {ARQNL@IJCAR}},
 series       = {{CEUR} Workshop Proceedings},
 volume       = {1770},
 publisher    = {CEUR-WS.org},
 pages        = {51--65},
)