main.bib

% Encoding: UTF-8

@book{hastie01statisticallearning,
  added-at = {2008-05-16T16:17:42.000+0200},
  address = {New York, NY, USA},
  author = {Hastie, Trevor and Tibshirani, Robert and Friedman, Jerome},
  biburl = {https://www.bibsonomy.org/bibtex/2f58afc5c9793fcc8ad8389824e57984c/sb3000},
  interhash = {d585aea274f2b9b228fc1629bc273644},
  intrahash = {f58afc5c9793fcc8ad8389824e57984c},
  keywords = {ml statistics},
  publisher = {Springer New York Inc.},
  series = {Springer Series in Statistics},
  timestamp = {2008-05-16T16:17:43.000+0200},
  title = {The Elements of Statistical Learning},
  year = 2009,
  doi = {10.1007/b94608},
  isbn = {978-0-387-84857-0},
  issn = {0172-7397},
}

@inproceedings{DBLP:conf/cade/WeidenbachDFKSW09,
  author    = {Christoph Weidenbach and
               Dilyana Dimova and
               Arnaud Fietzke and
               Rohit Kumar and
               Martin Suda and
               Patrick Wischnewski},
  editor    = {Renate A. Schmidt},
  title     = {{SPASS} Version 3.5},
  booktitle = {Automated Deduction - CADE-22},
  series    = {Lecture Notes in Computer Science},
  number    = {5663},
  pages     = {140--145},
  year      = {2009},
  doi       = {10.1007/978-3-642-02959-2_10},
  timestamp = {Tue, 14 May 2019 10:00:39 +0200},
  biburl    = {https://dblp.org/rec/conf/cade/WeidenbachDFKSW09.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{KaliszykU13b,
  author    = {Cezary Kaliszyk and
               Josef Urban},
  title     = {{MizAR 40 for Mizar 40}},
  journal   = {Journal of Automated Reasoning},
  volume    = {55},
  number    = {3},
  pages     = {245--256},
  year      = {2015},
  doi       = {10.1007/s10817-015-9330-8},
  timestamp = {Tue, 29 Sep 2015 09:03:48 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/jar/KaliszykU15a},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@article{DBLP:journals/jsc/RiazanovV03,
  author    = {Alexandre Riazanov and
               Andrei Voronkov},
  title     = {Limited resource strategy in resolution theorem proving},
  journal   = {Journal of Symbolic Computation},
  volume    = {36},
  number    = {1--2},
  pages     = {101--115},
  year      = {2003},
  doi       = {10.1016/S0747-7171(03)00040-3},
  timestamp = {Wed, 17 May 2017 14:25:48 +0200},
  biburl    = {https://dblp.org/rec/journals/jsc/RiazanovV03.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{Overbeek:1974:NCA:321812.321814,
 author = {Overbeek, Ross A.},
 title = {A New Class of Automated Theorem-Proving Algorithms},
 journal = {J. ACM},
 issue_date = {April 1974},
 volume = {21},
 number = {2},
 month = apr,
 year = {1974},
 issn = {0004-5411},
 pages = {191--200},
 numpages = {10},
 url = {http://doi.acm.org/10.1145/321812.321814},
 doi = {10.1145/321812.321814},
 acmid = {321814},
 publisher = {ACM},
 address = {New York, NY, USA},
}

@incollection{DBLP:books/el/RV01/NonnengartW01,
  author    = {Andreas Nonnengart and
               Christoph Weidenbach},
  editor    = {John Alan Robinson and
               Andrei Voronkov},
  title     = {Computing Small Clause Normal Forms},
  booktitle = {Handbook of Automated Reasoning (in 2 volumes)},
  pages     = {335--367},
  publisher = {Elsevier and {MIT} Press},
  year      = {2001},
  url       = {https://doi.org/10.1016/b978-044450813-3/50008-4},
  doi       = {10.1016/b978-044450813-3/50008-4},
  timestamp = {Thu, 25 Jul 2019 12:26:00 +0200},
  biburl    = {https://dblp.org/rec/books/el/RV01/NonnengartW01.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@MISC{E-manual,
  author =   {Stephan Schulz},
  title =   {{E 2.4 User Manual}},
  url = {http://wwwlehre.dhbw-stuttgart.de/~sschulz/WORK/E_DOWNLOAD/V_2.4/eprover.pdf},
  urldate = {May 2020},
  year =   2019,
}

@article{DBLP:journals/logcom/BachmairG94,
  author    = {Leo Bachmair and
               Harald Ganzinger},
  title     = {Rewrite-Based Equational Theorem Proving with Selection and Simplification},
  journal   = {Journal of Logic and Computation},
  volume    = {4},
  number    = {3},
  pages     = {217--247},
  year      = {1994},
  doi       = {10.1093/logcom/4.3.217},
  timestamp = {Wed, 17 May 2017 14:25:56 +0200},
  biburl    = {https://dblp.org/rec/journals/logcom/BachmairG94.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@InProceedings{SCV:CADE-2019,
  author =       {Stephan Schulz and Simon Cruanes and Petar Vukmirovi{\'c}},
  title =        {Faster, Higher, Stronger: {E} 2.3},
  year =         {2019},
  booktitle =    {Automated Deduction - CADE 27},
  editor =       {Pacal Fontaine},
  number =       {11716},
  series =       {Lecture Notes in Computer Science},
  pages =        {495--507},
  publisher =    {Springer},
  doi       = {10.1007/978-3-030-29436-6_29},
}


@article{DBLP:journals/jar/KuhlweinU15,
  author    = {Daniel K{\"{u}}hlwein and
               Josef Urban},
  title     = {{MaLeS:} {A} Framework for Automatic Tuning of Automated Theorem Provers},
  journal   = {J. Autom. Reasoning},
  volume    = {55},
  number    = {2},
  pages     = {91--116},
  year      = {2015},
  url       = {https://doi.org/10.1007/s10817-015-9329-1},
  doi       = {10.1007/s10817-015-9329-1},
  timestamp = {Sun, 02 Jun 2019 21:00:08 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/jar/KuhlweinU15},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/cade/KovacsMV11,
  author    = {Laura Kov{\'{a}}cs and
               Georg Moser and
               Andrei Voronkov},
  editor    = {Nikolaj Bj{\o}rner and
               Viorica Sofronie{-}Stokkermans},
  title     = {On Transfinite {K}nuth-{B}endix Orders},
  booktitle = {Automated Deduction -- {CADE-23}},
  series    = {Lecture Notes in Computer Science},
  number    = {6803},
  pages     = {384--399},
  publisher = {Springer Berlin Heidelberg},
  address   = {Berlin, Heidelberg},
  year      = {2011},
  doi       = {10.1007/978-3-642-22438-6_29},
  isbn      = {978-3-642-22438-6},
  timestamp = {Tue, 14 May 2019 10:00:39 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cade/KovacsMV11},
  bibsource = {dblp computer science bibliography, https://dblp.org},
}

@inproceedings{DBLP:conf/sat/SelsamB19,
  author    = {Daniel Selsam and
               Nikolaj Bj{\o}rner},
  title     = {Guiding High-Performance {SAT} Solvers with Unsat-Core Predictions},
  booktitle = {Theory and Applications of Satisfiability Testing - {SAT} 2019 - 22nd
               International Conference, {SAT} 2019, Lisbon, Portugal, July 9-12,
               2019, Proceedings},
  pages     = {336--353},
  year      = {2019},
  crossref  = {DBLP:conf/sat/2019},
  url       = {https://doi.org/10.1007/978-3-030-24258-9_24},
  doi       = {10.1007/978-3-030-24258-9_24},
  timestamp = {Mon, 01 Jul 2019 14:18:25 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/sat/SelsamB19},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/nips/WangTWD17,
  author    = {Mingzhe Wang and
               Yihe Tang and
               Jian Wang and
               Jia Deng},
  title     = {Premise Selection for Theorem Proving by Deep Graph Embedding},
  booktitle = {Advances in Neural Information Processing Systems 30: Annual Conference
               on Neural Information Processing Systems 2017, 4-9 December 2017,
               Long Beach, CA, {USA}},
  pages     = {2786--2796},
  year      = {2017},
  crossref  = {DBLP:conf/nips/2017},
  url       = {http://papers.nips.cc/paper/6871-premise-selection-for-theorem-proving-by-deep-graph-embedding},
  timestamp = {Tue, 23 Jul 2019 12:44:35 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/nips/WangTWD17},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/sat/2019,
  editor    = {Mikol{\'{a}}s Janota and
               In{\^{e}}s Lynce},
  title     = {Theory and Applications of Satisfiability Testing - {SAT} 2019 - 22nd
               International Conference, {SAT} 2019, Lisbon, Portugal, July 9-12,
               2019, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {11628},
  publisher = {Springer},
  year      = {2019},
  url       = {https://doi.org/10.1007/978-3-030-24258-9},
  doi       = {10.1007/978-3-030-24258-9},
  isbn      = {978-3-030-24257-2},
  timestamp = {Mon, 01 Jul 2019 14:16:33 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/sat/2019},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/corr/abs-1905-10006,
  author    = {Aditya Paliwal and
               Sarah M. Loos and
               Markus N. Rabe and
               Kshitij Bansal and
               Christian Szegedy},
  title     = {Graph Representations for Higher-Order Logic and Theorem Proving},
  journal   = {CoRR},
  volume    = {abs/1905.10006},
  year      = {2019},
  url       = {http://arxiv.org/abs/1905.10006},
  archivePrefix = {arXiv},
  eprint    = {1905.10006},
  timestamp = {Wed, 29 May 2019 11:27:50 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/corr/abs-1905-10006},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{olk2019property,
    title={Property Invariant Embedding for Automated Reasoning},
    author={Miroslav Olšák and Cezary Kaliszyk and Josef Urban},
    journal   = {CoRR},
    year={2019},
    eprint={1911.12073},
    archivePrefix={arXiv},
    primaryClass={cs.AI}
}
@proceedings{DBLP:conf/nips/2017,
  editor    = {Isabelle Guyon and
               Ulrike von Luxburg and
               Samy Bengio and
               Hanna M. Wallach and
               Rob Fergus and
               S. V. N. Vishwanathan and
               Roman Garnett},
  title     = {Advances in Neural Information Processing Systems 30: Annual Conference
               on Neural Information Processing Systems 2017, 4-9 December 2017,
               Long Beach, CA, {USA}},
  year      = {2017},
  timestamp = {Mon, 27 Nov 2017 12:38:16 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/nips/2017},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@incollection{Robinson1983,
author="Robinson, G.
and Wos, Larry",
editor="Siekmann, J{\"o}rg H.
and Wrightson, Graham",
title="Paramodulation and Theorem-Proving in First-Order Theories with Equality",
bookTitle="Automation of Reasoning: 2: Classical Papers on Computational Logic 1967--1970",
year="1983",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="298--313",
abstract="A term is an individual constant or variable or an n-adic function letter followed by n terms. An atomic formula is an n-adic predicate letter followed by n terms. A literal is an atomic formula or the negation thereof. A clause is a set of literals and is thought of as representing the universally-quantified disjunction of its members. It will sometimes be notationally convenient1 to distinguish between the empty clause □, viewed as a clause, and `other' empty sets such as the empty set of clauses, even though all these empty sets are the same set-theoretic object {\o}. A ground clause (term, literal) is one with no variables. A clause C' (literal, term) is an instance of another clause C (literal, term) if there is a uniform replacement of the variables in C by terms that transform C into C'.",
isbn="978-3-642-81955-1",
doi="10.1007/978-3-642-81955-1_19",
}

@article{DBLP:journals/jsc/PlaistedG86,
  author    = {David A. Plaisted and
               Steven Greenbaum},
  title     = {A Structure-Preserving Clause Form Translation},
  journal   = {J. Symb. Comput.},
  volume    = {2},
  number    = {3},
  pages     = {293--304},
  year      = {1986},
  url       = {http://dx.doi.org/10.1016/S0747-7171(86)80028-1},
  doi       = {10.1016/S0747-7171(86)80028-1},
  timestamp = {Tue, 20 Sep 2011 11:17:56 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/jsc/PlaistedG86},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@incollection{DBLP:books/el/RV01/NieuwenhuisR01,
  author    = {Robert Nieuwenhuis and
               Albert Rubio},
  editor    = {John Alan Robinson and
               Andrei Voronkov},
  title     = {Paramodulation-Based Theorem Proving},
  booktitle = {Handbook of Automated Reasoning (in 2 volumes)},
  pages     = {371--443},
  publisher = {Elsevier and {MIT} Press},
  year      = {2001},
  doi       = {10.1016/b978-044450813-3/50009-6},
  timestamp = {Thu, 25 Jul 2019 12:26:00 +0200},
  biburl    = {https://dblp.org/rec/books/el/RV01/NieuwenhuisR01.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{RegerSuda2017,
  author       = {Giles Reger and Martin Suda},
  title        = {Measuring progress to predict success: {Can} a good proof strategy be evolved?},
  year         = {2017},
  booktitle    = {AITP 2017},
  pages        = {20--21},
  url          = {http://aitp-conference.org/2017/aitp17-proceedings.pdf},
}

@Article{Cohen2011,
  author        = {William W. Cohen and Robert E. Schapire and Yoram Singer},
  title         = {Learning to Order Things},
  journal       = {Journal Of Artificial Intelligence Research},
  volume        = {10},
  pages         = {243--270},
  year          = {1999},
  archiveprefix = {arXiv},
  bibsource     = {dblp computer science bibliography, https://dblp.org},
  biburl        = {https://dblp.org/rec/bib/journals/corr/abs-1105-5464},
  eprint        = {1105.5464},
  doi           = {10.1613/jair.587},
}

@Article{Liu2009,
  author        = {Liu, Tie-Yan},
  title         = {Learning to Rank for Information Retrieval},
  journal       = {Found. Trends Inf. Retr.},
  year          = {2009},
  volume        = {3},
  number        = {3},
  pages         = {225--331},
  month         = mar,
  issn          = {1554-0669},
  __markedentry = {[filip:6]},
  acmid         = {1618304},
  address       = {Hanover, MA, USA},
  doi           = {10.1561/1500000016},
  issue_date    = {March 2009},
  numpages      = {107},
  owner         = {filip},
  publisher     = {Now Publishers Inc.},
  timestamp     = {2019-11-28},
  url           = {http://dx.doi.org/10.1561/1500000016},
}

@Article{Sut17,
  author    = {Sutcliffe, Geoff},
  title     = {The {TPTP} Problem Library and Associated Infrastructure. {From} {CNF} to {TH0}, {TPTP} v6.4.0},
  journal   = {Journal of Automated Reasoning},
  year      = {2017},
  volume    = {59},
  number    = {4},
  pages     = {483--502},
  doi       = {10.1007/s10817-017-9407-7},
}

@InProceedings{Kovacs2013,
  author    = {Kov{\'a}cs, Laura and Voronkov, Andrei},
  title     = {First-Order Theorem Proving and {Vampire}},
  booktitle = {Computer Aided Verification},
  year      = {2013},
  editor    = {Sharygina, Natasha and Veith, Helmut},
  pages     = {1--35},
  address   = {Berlin, Heidelberg},
  publisher = {Springer Berlin Heidelberg},
  abstract  = {In this paper we give a short introduction in first-order theorem proving and the use of the theorem prover Vampire. We discuss the superposition calculus and explain the key concepts of saturation and redundancy elimination, present saturation algorithms and preprocessing, and demonstrate how these concepts are implemented in Vampire. Further, we also cover more recent topics and features of Vampire designed for advanced applications, including satisfiability checking, theory reasoning, interpolation, consequence elimination, and program analysis.},
  isbn      = {978-3-642-39799-8},
  owner     = {filip},
  timestamp = {2019-12-02},
  url_document = {http://www.vprover.org/cav2013.pdf},
  doi       = {10.1007/978-3-642-39799-8_1},
}

@InProceedings{Schulz2013,
  author    = {Stephan Schulz},
  title     = {{System Description: E~1.8}},
  booktitle = {Proc.\ of the 19th LPAR, Stellenbosch},
  year      = {2013},
  editor    = {Ken McMillan and Aart Middeldorp and Andrei Voronkov},
  volume    = {8312},
  series    = {LNCS},
  publisher = {Springer},
  annote    = {StS},
  optpages  = {735-743},
  owner     = {filip},
  timestamp = {2019-12-02},
}

@Unpublished{Kamin1980,
  author    = {Samuel N. Kamin and Jacques L{\'e}vy},
  title     = {Two generalizations of the recursive path ordering},
  year      = {1980},
  owner     = {filip},
  timestamp = {2019-12-02},
  note      = {Unpublished letter to Nachum Dershowitz},
  url       = {http://www.cs.tau.ac.il/~nachumd/term/kamin-levy80spo.pdf},
}

@incollection{Knuth1983,
  pages         = {342--376},
  title         = {Simple Word Problems in Universal Algebras},
  publisher     = {Springer Berlin Heidelberg},
  year          = {1983},
  author        = {Knuth, Donald Ervin and Bendix, Peter B.},
  editor        = {Siekmann, J{\"o}rg H. and Wrightson, Graham},
  address       = {Berlin, Heidelberg},
  isbn          = {978-3-642-81955-1},
  abstract      = {An algorithm is described which is capable of solving certain word problems: i.e. of deciding whether or not two words composed of variables and operators can be proved equal as a consequence of a given set of identities satisfied by the operators. Although the general word problem is well known to be unsolvable, this algorithm provides results in many interesting cases. For example in elementary group theory if we are given the binary operator {\textperiodcentered}, the unary operator −, and the nullary operator e, the algorithm is capable of deducing from the three identities a {\textperiodcentered} (b {\textperiodcentered} c) = (a {\textperiodcentered} b) {\textperiodcentered} c, a {\textperiodcentered} a− = e, a {\textperiodcentered} e = a, the laws a− {\textperiodcentered} a = e, e {\textperiodcentered} a = a, a− −= a, etc.; and furthermore it can show that a {\textperiodcentered} b = b {\textperiodcentered} a−is not a consequence of the given axioms.},
  booktitle     = {Automation of Reasoning: 2: Classical Papers on Computational Logic 1967--1970},
  doi           = {10.1007/978-3-642-81955-1_23},
  owner         = {filip},
  timestamp     = {2019-12-02},
}

@article{Wu2019,
   title={A Comprehensive Survey on Graph Neural Networks},
   ISSN={2162-2388},
   DOI={10.1109/tnnls.2020.2978386},
   journal={IEEE Transactions on Neural Networks and Learning Systems},
   publisher={Institute of Electrical and Electronics Engineers (IEEE)},
   author={Wu, Zonghan and Pan, Shirui and Chen, Fengwen and Long, Guodong and Zhang, Chengqi and Yu, Philip S.},
   year={2020},
   pages={1–21}
}

@incollection{Tseitin1983,
  pages     = {466--483},
  title     = {On the Complexity of Derivation in Propositional Calculus},
  publisher = {Springer Berlin Heidelberg},
  year      = {1983},
  author    = {Tseitin, G. S.},
  editor    = {Siekmann, J{\"o}rg H. and Wrightson, Graham},
  address   = {Berlin, Heidelberg},
  isbn      = {978-3-642-81955-1},
  abstract  = {The question of the minimum complexity of derivation of a given formula in classical propositional calculus is considered in this article and it is proved that estimates of complexity may vary considerably among the various forms of propositional calculus. The forms of propositional calculus used in the present article are somewhat unusual, {\textdagger} but the results obtained for them can, in principle, be extended to the usual forms of propositional calculus.},
  booktitle = {Automation of Reasoning: 2: Classical Papers on Computational Logic 1967--1970},
  doi       = {10.1007/978-3-642-81955-1_28},
  owner     = {filip},
  timestamp = {2019-12-03},
}

@InProceedings{Reger2016,
  author    = {Giles Reger and Martin Suda and Andrei Voronkov},
  title     = {New Techniques in Clausal Form Generation},
  booktitle = {GCAI 2016. 2nd Global Conference on Artificial Intelligence},
  year      = {2016},
  editor    = {Christoph Benzm\"uller and Geoff Sutcliffe and Raul Rojas},
  volume    = {41},
  series    = {EPiC Series in Computing},
  pages     = {11--23},
  publisher = {EasyChair},
  bibsource = {EasyChair, https://easychair.org},
  doi       = {10.29007/dzfz},
  issn      = {2398-7340},
  owner     = {filip},
  timestamp = {2019-12-03},
}

@Article{Graves2013,
  author        = {Alex Graves},
  title         = {Generating Sequences With Recurrent Neural Networks},
  journal       = {CoRR},
  year          = {2013},
  volume        = {abs/1308.0850},
  archiveprefix = {arXiv},
  bibsource     = {dblp computer science bibliography, https://dblp.org},
  biburl        = {https://dblp.org/rec/bib/journals/corr/Graves13},
  eprint        = {1308.0850},
  owner         = {filip},
  timestamp     = {2019-12-04},
  url           = {http://arxiv.org/abs/1308.0850},
}

@book{Iverson1962,
address = {New York, NY, USA},
author = {Iverson, Kenneth E.},
isbn = {978-0-471-43014-8},
publisher = {John Wiley \& Sons, Inc.},
title = {{A Programming Language}},
url = {https://dl.acm.org/doi/book/10.5555/1098666},
url_document = {http://www.softwarepreservation.org/projects/apl/Books/APROGRAMMING LANGUAGE},
year = {1962}
}

@Article{scikit-learn,
  author  = {Pedregosa, F. and Varoquaux, G. and Gramfort, A. and Michel, V. and Thirion, B. and Grisel, O. and Blondel, M. and Prettenhofer, P. and Weiss, R. and Dubourg, V. and Vanderplas, J. and Passos, A. and Cournapeau, D. and Brucher, M. and Perrot, M. and Duchesnay, E.},
  journal = {Journal of Machine Learning Research},
  title   = {Scikit-learn: Machine Learning in {P}ython},
  year    = {2011},
  pages   = {2825--2830},
  volume  = {12},
  url     = {https://scikit-learn.org/}
}

@Article{Tibshirani1996,
  author    = {Robert Tibshirani},
  journal   = {Journal of the Royal Statistical Society. Series B (Methodological)},
  title     = {Regression Shrinkage and Selection via the {Lasso}},
  year      = {1996},
  issn      = {00359246},
  number    = {1},
  pages     = {267--288},
  volume    = {58},
  abstract  = {We propose a new method for estimation in linear models. The `lasso' minimizes the residual sum of squares subject to the sum of the absolute value of the coefficients being less than a constant. Because of the nature of this constraint it tends to produce some coefficients that are exactly 0 and hence gives interpretable models. Our simulation studies suggest that the lasso enjoys some of the favourable properties of both subset selection and ridge regression. It produces interpretable models like subset selection and exhibits the stability of ridge regression. There is also an interesting relationship with recent work in adaptive function estimation by Donoho and Johnstone. The lasso idea is quite general and can be applied in a variety of statistical models: extensions to generalized regression models and tree-based models are briefly described.},
  publisher = {[Royal Statistical Society, Wiley]},
  url       = {http://www.jstor.org/stable/2346178},
}

@Comment{jabref-meta: databaseType:bibtex;}