@article(ANB98,
 author       = {H. Andr\'{e}ka and I. N\'{e}meti and J. van Benthem},
 year         = {1998},
 title        = {Modal logics and bounded fragments of predicate logic},
 journal      = {JPL},
 volume       = {27},
 number       = {3},
 pages        = {217--274},
 doi          = {10.1023/A:1004275029985},
)
@article(AG00,
 author       = {T. Arts and J. Giesl},
 year         = {2000},
 title        = {Termination of term rewriting using dependency pairs},
 journal      = {Theoretical Computer Science},
 volume       = {236},
 number       = {1},
 pages        = {133--178},
 doi          = {10.1016/S0304-3975(99)00207-8},
)
@article(AEM15,
 author       = {M. Avanzini and N. Eguchi and G. Moser},
 year         = {2015},
 title        = {A new order-theoretic characterisation of the polytime computable functions},
 journal      = {Theoretical Computer Science},
 volume       = {585},
 pages        = {3--24},
 doi          = {10.1016/j.tcs.2015.03.003},
)
@article(AM13,
 author       = {M. Avanzini and G. Moser},
 year         = {2013},
 title        = {Polynomial Path Orders},
 journal      = {Log.\ Meth.\ Comput.\ Sci.},
 volume       = {9},
 number       = {4},
 doi          = {10.2168/LMCS-9(4:9)2013},
)
@book(BN98,
 author       = {F. Baader and T. Nipkow},
 year         = {1998},
 title        = {Term Rewriting and All That},
 publisher    = {Cambridge University Press},
 doi          = {10.1017/CBO9781139172752},
)
@article(BellantoniCook:1992,
 author       = {S. Bellantoni and S. Cook},
 year         = {1992},
 title        = {A new recursion-theoretic characterization of the polytime functions},
 journal      = {Comput. Complex.},
 volume       = {2},
 number       = {2},
 pages        = {97--110},
 doi          = {10.1145/129712.129740},
)
@article(Ben-Amram:2011,
 author       = {Ben-Amram, A.},
 year         = {2011},
 title        = {Monotonicity Constraints for Termination in the Integer Domain},
 journal      = {Log.\ Meth.\ Comput.\ Sci.},
 volume       = {7},
 number       = {3},
 doi          = {10.2168/LMCS-7(3:4)2011},
)
@inproceedings(BP:2016,
 author       = {Ben{-}Amram, A. and A. Pineles},
 year         = {2016},
 title        = {Flowchart Programs, Regular Expressions, and Decidability of Polynomial Growth-Rate},
 booktitle    = {Proc.\ 4th VPT},
 series       = {EPTCS},
 volume       = {216},
 pages        = {24--49},
 doi          = {10.4204/EPTCS.216.2},
)
@article(BHP14,
 author       = {J. P. Bridge and S. Holden and L. Paulson},
 year         = {2014},
 title        = {Machine Learning for First-Order Theorem Proving},
 journal      = {JAR},
 volume       = {53},
 number       = {2},
 pages        = {141--172},
 doi          = {10.1007/s10817-014-9301-5},
)
@inproceedings(CJSU19,
 author       = {K. Chvalovsk\'y and Jakub\r{u}v, J. and M. Suda and J. Urban},
 year         = {2019},
 title        = {{ENIGMA-NG:} Efficient Neural and Gradient-Boosted Inference Guidance for {E}},
 booktitle    = {Proc.\ 27th CADE},
 series       = {LNCS},
 volume       = {11716},
 pages        = {197--215},
 doi          = {10.1007/978-3-030-29436-6\_12},
)
@inproceedings(CDZ:2017,
 author       = {T. Colcombet and L. Daviaud and F. Zuleger},
 year         = {2017},
 title        = {Automata and Program Analysis},
 booktitle    = {Proc.\ 21st FCT},
 series       = {LNCS},
 volume       = {10472},
 pages        = {3--10},
 doi          = {10.1007/978-3-662-55751-8\_1},
)
@inproceedings(DT90,
 author       = {M. Dauchet and S. Tison},
 year         = {1990},
 title        = {The Theory of Ground Rewrite Systems is Decidable},
 booktitle    = {Proc.\ 5thIEEE Symposium on Logic in Computer Science},
 pages        = {242--248},
 doi          = {10.1109/LICS.1990.113750},
)
@article(DPVZ17,
 author       = {Y. Demyanova and T. Pani and H. Veith and F. Zuleger},
 year         = {2017},
 title        = {Empirical Software Metrics for Benchmarking of Verification Tools},
 journal      = {Form. Methods Syst. Des.},
 volume       = {50},
 number       = {2-3},
 pages        = {289--316},
 doi          = {10.1007/s10703-016-0264-5},
)
@inproceedings(JU17,
 author       = {Jakub\r{u}v, J. and J. Urban},
 year         = {2017},
 title        = {{ENIGMA:} Efficient Learning-Based Inference Guiding Machine},
 booktitle    = {Proc.\ CICM 2017},
 series       = {LNCS},
 volume       = {10383},
 pages        = {292--302},
 doi          = {10.1007/978-3-319-62075-6\_20},
)
@article(JU18,
 author       = {Jakub\r{u}v, J. and J. Urban},
 year         = {2018},
 title        = {Hierarchical invention of theorem proving strategies},
 journal      = {{AI} Commun.},
 volume       = {31},
 number       = {3},
 pages        = {237--250},
 doi          = {10.3233/AIC-180761},
)
@inproceedings(KU15,
 author       = {C. Kaliszyk and J. Urban},
 year         = {2015},
 title        = {{FEMaLeCoP}: Fairly Efficient Machine Learning Connection Prover},
 booktitle    = {Proc.\ LPAR 2015},
 series       = {LNCS},
 volume       = {9450},
 pages        = {88--96},
 doi          = {10.1007/978-3-662-48899-7\_7},
)
@inproceedings(Ko13,
 author       = {K. Korovin},
 year         = {2013},
 title        = {Non-cyclic Sorts for First-Order Satisfiability},
 booktitle    = {Proc.\ FroCoS 2013},
 series       = {LNCS},
 volume       = {8152},
 pages        = {214--228},
 doi          = {10.1007/978-3-642-40885-4\_15},
)
@inproceedings(KSU13,
 author       = {D. K{\"u}hlwein and S. Schulz and J. Urban},
 year         = {2013},
 title        = {{E-MaLeS} 1.1},
 booktitle    = {Proc.\ 24th CADE},
 series       = {LNCS},
 volume       = {7898},
 pages        = {407--413},
 doi          = {10.1007/978-3-642-38574-2},
)
@incollection(Leivant:1994,
 author       = {D. Leivant},
 year         = {1994},
 title        = {Ramified recurrence and computatinal complexity {I}: {W}ord recurrence and poly-time},
 editor       = {P. Clote and J. Remmel},
 booktitle    = {Feasible Mathematics {II}},
 publisher    = {Birkh{\"a}user},
 pages        = {320--343},
 doi          = {10.1007/978-1-4612-2566-9\_11},
)
@article(Le80,
 author       = {H. R. Lewis},
 year         = {1980},
 title        = {Complexity results for classes of quantificational formulas},
 journal      = {JCSS},
 volume       = {21},
 number       = {3},
 pages        = {317--353},
 doi          = {10.1016/0022-0000(80)90027-6},
)
@inproceedings(LISK17,
 author       = {S. M. Loos and G. Irving and C. Szegedy and C. Kaliszyk},
 year         = {2017},
 title        = {Deep Network Guided Proof Search},
 booktitle    = {Proc. 21st LPAR},
 pages        = {85--105},
 doi          = {10.29007/8mwc},
)
@inproceedings(Sch01,
 author       = {S. Schulz},
 year         = {2001},
 title        = {Learning Search Control Knowledge for Equational Theorem Proving},
 booktitle    = {Proc.\ KI 2001},
 series       = {LNCS},
 volume       = {2174},
 pages        = {320--334},
 doi          = {10.1007/3-540-45422-5\_23},
)
@article(Si88,
 author       = {H. Simmons},
 year         = {1988},
 title        = {The realm of primitive recursion},
 journal      = {Archive for Mathematical Logic},
 volume       = {27},
 number       = {2},
 pages        = {177--188},
 doi          = {10.1007/BF01620765},
)
@article(TPTP,
 author       = {G. Sutcliffe},
 year         = {2009},
 title        = {{The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts}},
 journal      = {JAR},
 volume       = {43},
 number       = {4},
 pages        = {337--362},
 doi          = {10.1007/s10817-009-9143-8},
)