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