, We use symbols such as Q, Z, N, and R with different meaning. Depending on the current context, we use them to address the respective sets of numbers, structures, or sorts

, While the former has term length len(t 1 ) = len(4 · x + (?2)) = 5, the latter has length len(t 2 ) = len(x + x + x + x ? 1 ? 1) = 11. More generally, the rational numbers in LRA terms are formally represented by constant symbols, the integers in (abbreviated) PA terms can be conceived as being represented in a unary encoding, Notice that the formal term length of the LRA term t 1 := 4x ? 2 differs significantly from the length of the PA term t 2 := 4x ? 2

S. Arora and B. Barak, Computational Complexity -A Modern Approach, 2009.

A. Armando, M. P. Bonacina, S. Ranise, and S. Schulz, New Results on Rewrite-Based Satisfiability Procedures, ACM Transactions on Computational Logic, vol.10, issue.1, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00576862

A. Armando, C. Castellini, E. Giunchiglia, and M. Maratea, A SAT-based Decision Procedure for the Boolean Combination of Difference Constraints, Theory and Applications of Satisfiability Testing (SAT'04), 2004.

W. Ackermann, Über die Erfüllbarkeit gewisser Zählausdrücke, Mathematische Annalen, vol.100, pp.638-649, 1928.

W. Ackermann, Untersuchungenüber das Eliminationsproblem der mathematischen Logik, Mathematische Annalen, vol.110, pp.390-413, 1935.

W. Ackermann, Solvable Cases of the Decision Problem, 1954.

R. Alur and D. L. Dill, Automata For Modeling Real-Time Systems, Automata, Languages and Programming (ICALP'90), pp.322-335, 1990.

R. Alur and D. L. Dill, A Theory of Timed Automata, Theoretical Computer Science, vol.126, issue.2, pp.183-235, 1994.

C. Areces and P. Fontaine, Combining Theories: The Ackerman and Guarded Fragments, Frontiers of Combining Systems (FroCoS'11), pp.40-54, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00642529

S. Aanderaa and W. D. Goldfarb, The Finite Controllability of the Maslov Case, Journal of Symbolic Logic, vol.39, issue.3, pp.509-518, 1974.

R. Alur and T. A. Henzinger, A Really Temporal Logic, Journal of the ACM, vol.41, issue.1, pp.181-204, 1994.

S. Abramsky and J. Kontinen, Jouko Väänänen, and Heribert Vollmer, Dependence Logic, Theory and Applications, 2016.

E. Althaus, E. Kruglov, and C. Weidenbach, Superposition Modulo Linear Arithmetic SUP(LA), Frontiers of Combining Systems (FroCoS'09), pp.84-99, 2009.

G. Amendola, N. Leone, and M. Manna, Finite model reasoning over existential rules. Theory and Practice of Logic Programming, vol.17, pp.726-743, 2017.

H. Andréka, I. Németi, and J. Van-benthem, Modal Languages and Bounded Fragments of Predicate Logic, Journal of Philosophical Logic, vol.27, issue.3, pp.217-274, 1998.

A. Abadi, A. M. Rabinovich, and M. Sagiv, Decidable Fragments of Many-Sorted Logic, Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'07), pp.17-31, 2007.

A. Abadi, A. Rabinovich, and M. Sagiv, Decidable Fragments of Many-Sorted Logic, Journal of Symbolic Computation, vol.45, issue.2, pp.153-172, 2010.

G. Alagi and C. Weidenbach, NRCL -A Model Building Approach to the Bernays-Schönfinkel Fragment, Frontiers of Combining Systems (FroCoS'15), vol.9322, pp.69-84, 2015.

H. Barbosa, New techniques for instantiation and proof production in SMT solving. (Nouvelles techniques pour l'instanciation et la production des preuves dans SMT), 2017.
URL : https://hal.archives-ouvertes.fr/tel-01591108

O. Beyersdorff and J. Blinkhorn, Dependency Schemes in QBF Calculi: Semantics and Soundness, Principles and Practice of Constraint Programming (CP'16), pp.96-112, 2016.

G. S. Boolos, J. P. Burgess, and R. C. Jeffrey, Computability and Logic, 2002.

J. Baget, M. Bienvenu, M. Mugnier, and S. Rocher, Combining Existential Rules and Transitivity: Next Steps, Artificial Intelligence (IJCAI'15), pp.2720-2726, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01171846

V. Bárány, M. Benedikt, and C. Balder-ten, Rewriting Guarded Negation Queries, Mathematical Foundations of Computer Science (MFCS'13), pp.98-110, 2013.

D. Bresolin, D. D. Monica, A. Montanari, and G. Sciavicco, The light side of interval temporal logic: the Bernays-Schönfinkel fragment of CDT, Annals of Mathematics and Artificial Intelligence, vol.71, issue.1-3, pp.11-39, 2014.

P. Blackburn, Y. Maarten-de-rijke, and . Venema, Modal Logic, Cambridge Tracts in Theoretical Computer Science, vol.53, 2002.
URL : https://hal.archives-ouvertes.fr/inria-00100503

H. Behmann, Beiträge zur Algebra der Logik, insbesondere zum Entscheidungsproblem, Mathematische Annalen, vol.86, issue.3-4, pp.163-229, 1922.

M. Baaz, U. Egly, and A. Leitsch, Normal Form Transformations, Handbook of Automated Reasoning, vol.I, pp.273-333, 2001.

R. Berger, The undecidability of the domino problem, 1966.

L. Berman, The Complexitiy of Logical Theories, Theoretical Computer Science, vol.11, pp.71-77, 1980.

P. Baumgartner, A. Fuchs, C. Hans-de-nivelle, and . Tinelli, Computing finite models by reduction to function-free clause logic, Journal of Applied Logic, vol.7, issue.1, pp.58-74, 2009.

M. Baaz, C. G. Fermüller, A. Bouyer, U. Fahrenberg, K. G. Larsen et al., A Non-Elementary Speed-Up in Proof Length by Structural Clause Form Transformation, Logic in Computer Science (LICS'94), pp.213-219, 1994.

T. A. Clarke and . Henzinger, Helmut Veith, and Roderick Bloem, pp.1001-1046, 2018.

L. Bachmair and H. Ganzinger, Resolution Theorem Proving, Handbook of Automated Reasoning, vol.I, pp.19-99, 2001.

E. Börger, E. Grädel, and Y. Gurevich, The Classical Decision Problem, Perspectives in Mathematical Logic, 1997.

J. Baget, F. Garreau, M. Mugnier, and S. Rocher, Extending Acyclicity Notions for Existential Rules, European Conference on Artificial Intelligence (ECAI'14), pp.39-44, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01092757

L. Bachmair, H. Ganzinger, and U. Waldmann, Theorem Proving for Hierarchic First-Order Theories, Algebraic and Logic Programming (ALP'92), pp.420-434, 1992.

L. Bachmair, H. Ganzinger, and U. Waldmann, Superposition with Simplification as a Desision Procedure for the Monadic Class with Equality, Computational Logic and Proof Theory, Third Kurt Gödel Colloquium (KGC'93), pp.83-96, 1993.

L. Bachmair, H. Ganzinger, and U. Waldmann, Refutational Theorem Proving for Hierarchic First-Order Theories. Applicable Algebra in Engineering, Communication and Computing, vol.5, pp.193-212, 1994.

A. Biere, Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications, 2009.

M. P. Bonacina and M. Johansson, Interpolation Systems for Ground Proofs in Automated Deduction: a Survey, Journal of Automated Reasoning, vol.54, issue.4, pp.353-390, 2015.

M. P. Bonacina and M. Johansson, On Interpolation in Automated Theorem Proving, Journal of Automated Reasoning, vol.54, issue.1, pp.69-97, 2015.

C. Baier and J. Katoen, Principles of model checking, 2008.

M. Baaz and A. Leitsch, On Skolemization and Proof Complexity, Fundamenta Informaticae, vol.20, issue.4, pp.353-379, 1994.

M. Baaz and A. Leitsch, Methods of Cut-Elimination, Trends in Logic, vol.34, 2011.

J. Baget, M. Leclère, and M. Mugnier, Walking the Decidability Line for Rules with Existential Variables, Knowledge Representation and Reasoning (KR'10), 2010.
URL : https://hal.archives-ouvertes.fr/lirmm-00535780

. Blm-+-17]-patricia, F. Bouyer, N. Laroussinie, J. Markey, J. Ouaknine et al., Timed Temporal Logics, Models, Algorithms, Logics and Tools -Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday, pp.211-230, 2017.

R. E. Bryant, K. Shuvendu, S. A. Lahiri, and . Seshia, Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions, Computer Aided Verification (CAV'02), pp.78-92, 2002.

A. R. Bradley and Z. Manna, The Calculus of Computation -Decision Procedures with Applications to Verification, Texts in Theoretical Computer Science. An EATCS Series, 2007.

S. Bova and F. Mogavero, Herbrand property, finite quasi-Herbrand models, and a Chandra-Merlin theorem for quantified conjunctive queries, Logic in Computer Science (LICS'17), pp.1-12, 2017.

N. Bjørner, K. L. Mcmillan, and A. Rybalchenko, On Solving Universally Quantified Horn Clauses, Static Analysis (SAS'13), pp.105-125, 2013.

J. Baget, M. Mugnier, S. Rudolph, and M. Thomazo, Walking the Complexity Lines for Generalized Guarded Existential Rules, Artificial Intelligence (IJCAI'11), pp.712-717, 2011.
URL : https://hal.archives-ouvertes.fr/lirmm-00618081

A. R. Bradley, Z. Manna, and H. B. Sipma, What's Decidable About Arrays, Verification, Model Checking, and Abstract Interpretation (VMCAI'06), pp.427-442, 2006.

F. Baader and T. Nipkow, Term Rewriting and All That, 1998.

B. Bérard, A. Petit, V. Diekert, and P. Gastin, Characterization of the Expressive Power of Silent Transitions in Timed Automata, Fundamenta Informaticae, vol.36, issue.2-3, pp.145-182, 1998.

A. R. Bradley, Safety Analysis of Systems, 2007.

P. Bernays and M. Schönfinkel, Zum Entscheidungsproblem der mathematischen Logik, Mathematische Annalen, vol.99, issue.1, pp.342-372, 1928.

D. Berend and T. Tassa, Improved bounds on Bell numbers and on moments of sums of random variables, Probability and Mathematical Statistics, vol.30, issue.2, pp.185-205, 2010.

C. Barrett and C. Tinelli, Satisfiability Modulo Theories
URL : https://hal.archives-ouvertes.fr/hal-01095009

T. A. Clarke and . Henzinger, Helmut Veith, and Roderick Bloem, pp.305-343, 2018.

V. Bárány, L. Balder-ten-cate, and . Segoufin, Guarded negation, Automata, Languages and Programming (ICALP'11), Part II, pp.356-367, 2011.

V. Bárány, Balder ten Cate, and Luc Segoufin. Guarded Negation, Journal of the ACM, vol.62, issue.3, p.22, 2015.

M. Benedikt, Balder ten Cate, and Michael Vanden Boom. Effective Interpolation and Preservation in Guarded Logics, ACM Transactions on Computational Logic, vol.17, issue.2, pp.1-8, 2016.

J. and R. Büchi, Weak second-order arithmetic and finite automata, Logik und Grundlagen der Mathematik, vol.6, pp.66-92, 1960.

J. and R. Büchi, On a decision method in restricted second order arithmetic, Proceedings of the 1960 International Congress on Logic, pp.1-11, 1962.

P. Baumgartner and U. Waldmann, Hierarchic Superposition: Completeness without Compactness, Fifth International Conference on Mathematical Aspects of Computer and Information Sciences (MACIS'13), pp.8-12, 2013.
URL : https://hal.archives-ouvertes.fr/hal-01087872

P. Baumgartner and U. Waldmann, Hierarchic superposition with weak abstraction, Automated Deduction (CADE-24), vol.7898, pp.39-57, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00931919

C. Calude, Information and Randomness : An Algorithmic Perspective. Springer, second, revised and extended edition, 2002.

S. Cotton, E. Asarin, O. Maler, and P. Niebert, Some Progress in Satisfiability Checking for Difference Logic, Formal Modelling and Analysis of Timed Systems and Formal Techniques in Real-Time and Fault-Tolerant Systems (FORMATS/FTRTFT'04), pp.263-276, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00157566

M. Cdg-+-08]-h.-comon, R. Dauchet, C. Gilleron, F. Löding, D. Jacquemard et al., Tree Automata Techniques and Applications, 2008.

P. Chocron, P. Fontaine, and C. Ringeissen, A Gentle Non-Disjoint Combination of Satisfiability Procedures, Automated Reasoning (IJCAR'14), pp.122-136, 2014.
URL : https://hal.archives-ouvertes.fr/hal-00985135

P. Chocron, P. Fontaine, and C. Ringeissen, A Polite Non-Disjoint Combination Method: Theories with Bridging Functions Revisited, Automated Deduction (CADE-25), pp.419-433, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01157898

A. Calì, G. Gottlob, and A. Pieris, Advanced Processing for Ontological Queries, Proceedings of VLDB, vol.3, pp.554-565, 2010.

A. Calì, G. Gottlob, and A. Pieris, Query Answering under Nonguarded Rules in Datalog+/?, Web Reasoning and Rule Systems (RR'10), pp.1-17, 2010.

K. J. Compton and C. W. Henson, A Uniform Method for Proving Lower Bounds on the Computational Complexity of Logical Theories, Annals of Pure and Applied Logic, vol.48, issue.1, pp.1-79, 1990.

A. Church, Correction to A Note on the Entscheidungsproblem, Journal of Symbolic Logic, vol.1, issue.3, pp.101-102, 1936.

A. Church, A Note on the Entscheidungsproblem, Journal of Symbolic Logic, vol.1, issue.1, pp.40-41, 1936.

A. Church, An Unsolvable Problem of Elementary Number Theory, Journal of Symbolic Logic, vol.1, issue.2, pp.73-74, 1936.

E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem, Handbook of Model Checking, 2018.

H. Comon and Y. Jurski, Multiple Counters Automata, Safety Analysis and Presburger Arithmetic, Computer Aided Verification (CAV'98), pp.268-279, 1998.

H. Comon and Y. Jurski, Timed automata and the theory of real numbers, Concurrency Theory (CONCUR'99), pp.242-257, 1999.

C. Chung, C. , and H. Keisler, Model Theory, Studies in Logic and the Foundations of Mathematics, vol.73, 1990.

S. Conchon and S. Krstic, Strategies for combining decision procedures, Theoretical Computer Science, vol.354, issue.2, pp.187-210, 2006.

K. Ashok, H. R. Chandra, J. A. Lewis, and . Makowsky, Embedded Implicational Dependencies and their Inference Problem, Symposium on Theory of Computing (STOC'81), pp.342-354, 1981.

J. Cox and K. Mcaloon, Decision procedures for constraint-based extensions of Datalog, Constraint Logic Programming, pp.17-32, 1993.

S. Cotton and O. Maler, Fast and Flexible Difference Constraint Propagation for DPLL(T), Theory and Applications of Satisfiability Testing (SAT'06), pp.170-183, 2006.

J. Cox, K. Mcaloon, and C. Tretkoff, Computational Complexity and Constraint Logic Programming Languages, Annals of Mathematics and Artificial Intelligence, vol.5, issue.2-4, pp.163-189, 1992.

W. Conradie, On the strength and scope of DLS, Journal of Applied Non-Classical Logics, vol.16, issue.3-4, pp.279-296, 2006.

A. Stephen and . Cook, The Complexity of Theorem-Proving Procedures, Theory of Computing (STOC'71), pp.151-158, 1971.

D. C. Cooper, Theorem Proving in Arithmetic without Multiplication, Machine Intelligence, vol.7, pp.91-99, 1972.

S. and B. Cooper, Computability Theory, 2004.

W. Craig, Linear Reasoning. A New Form of the Herbrand-Gentzen Theorem, Journal of Symbolic Logic, vol.22, issue.3, p.1957

W. Craig, Three Uses of the Herbrand-Gentzen Theorem in Relating Model Theory and Proof Theory, Journal of Symbolic Logic, vol.22, issue.3, p.1957

H. Thomas, C. Cormen, R. L. Stein, C. E. Rivest, and . Leiserson, Introduction to Algorithms, 2001.

W. Charatonik and P. Witkowski, On the Complexity of the Bernays-Schönfinkel Class with Datalog, Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-17), vol.6397, pp.187-201, 2010.

A. Dawar, Finite models and finitely many variables, Logic, Algebra and Computer Science, vol.46, pp.93-117, 1999.

B. George, B. C. Dantzig, and . Eaves, Fourier-Motzkin Elimination and Its Dual, Journal of Combinatorial Theory, Series A, vol.14, issue.3, pp.288-297, 1973.

L. Doyen, G. Frehse, G. J. Pappas, and A. Platzer, Verification of Hybrid Systems, Handbook of Model Checking, pp.1047-1110, 2018.

B. Dreben and W. D. Goldfarb, The Decision Problem: Solvable Classes of Quantificational Formulas, 1979.

A. Dawar, M. Grohe, S. Kreutzer, and N. Schweikardt, Model Theory Makes Formulas Large, Automata, Languages and Programming (ICALP'07), pp.913-924, 2007.

A. Dawar, M. Grohe, S. Kreutzer, and N. Schweikardt, Model Theory Makes Formulas Large, 2007.

G. Rodney, D. R. Downey, and . Hirschfeldt, Algorithmic Randomness and Complexity, 2010.

L. L. Dines, Systems of Linear Inequalities, vol.20, pp.191-199, 1919.

B. Dreben, A. Kahr, and H. Wang, Classification of AEA Formulas by Letter Atoms, Bulletin of the American Mathematical Society, vol.68, issue.5, pp.528-532, 1962.

L. Denenberg and H. R. Lewis, The Complexity of the Satisfiability Problem for Krom Formulas, Theoretical Computer Science, vol.30, pp.319-341, 1984.

L. Denenberg and H. R. Lewis, Logical Syntax and Computational Complexity, Computation and Proof Theory. Proceedings of the Logic Colloquium '83, pp.101-115, 1984.

L. Mendonça-de-moura and N. Bjørner, Satisfiability Modulo Theories: Introduction and Applications, Communications of the ACM, vol.54, issue.9, pp.69-77, 2011.

N. Hans-de, A Resolution Decision Procedure for the Guarded Fragment, Automated Deduction (CADE-15), pp.191-204, 1998.

M. Hans-de-nivelle and . De-rijke, Deciding the guarded fragments by resolution, Journal of Symbolic Computation, vol.35, issue.1, pp.21-58, 2003.

I. Hans-de-nivelle and . Pratt-hartmann, A Resolution-Based Decision Procedure for the Two-Variable Fragment with Equality, Automated Reasoning (IJCAR'01), pp.211-225, 2001.

D. Detlefs, G. Nelson, and J. B. Saxe, Simplify: a theorem prover for program checking, Journal of the ACM, vol.52, issue.3, pp.365-473, 2005.

A. Dolzmann, Algorithmic strategies for applicable real quantifier elimination, 2000.

J. Peter and . Downey, Undecidability of Presburger Arithmetic with a Single Monadic Predicate Letter, 1972.

B. Dreben, Solvable Surányi subclasses: an introduction to the Herbrand theory, vol.31, pp.32-47, 1962.

H. Ebbinghaus and J. Flum, Finite model theory. Second Edition. Perspectives in Mathematical Logic, 1999.

H. Ebbinghaus, J. Flum, and W. Thomas, Mathematical Logic, 1994.

U. Egly, On the Value of Antiprenexing, Logic Programming and Automated Reasoning (LPAR'94), pp.69-83, 1994.

E. Ekk-+-11]-andreas-eggers, S. Kruglov, K. Kupferschmid, T. Scheibler, C. Teige et al., Superposition Modulo Non-linear Arithmetic, Frontiers of Combining Systems (FroCoS'11), pp.119-134, 2011.

Z. Ekk-+-12]-moshe-emmer, K. Khasidashvili, C. Korovin, A. Sticksel, and . Voronkov, EPR-Based Bounded Model Checking at Word Level, Automated Reasoning (IJCAR'12), pp.210-224, 2012.

M. Emmer, Z. Khasidashvili, K. Korovin, and A. Voronkov, Encoding industrial hardware verification problems into effectively propositional logic, Formal Methods in Computer-Aided Design (FMCAD'10), pp.137-144, 2010.

B. Herbert and . Enderton, A mathematical introduction to logic, 1972.

B. Herbert and . Enderton, A mathematical introduction to logic, 2001.

T. Frühwirth and S. Abdennadher, Essentials of Constraint Programming

. Springer, , 2003.

J. Flum and M. Grohe, Parameterized Complexity Theory. Texts in Theoretical Computer Science. An EATCS Series, 2006.

A. Fietzke, Labelled Superposition, 2013.

M. Fitting, First-Order Logic and Automated Theorem Proving, Second Edition. Graduate Texts in Computer Science, 1996.

C. Flanagan, R. Joshi, and J. B. Saxe, An Explicating Theorem Prover for Quantified Formulas, 2004.

G. Christian, A. Fermüller, U. Leitsch, T. Hustadt, and . Tammet, Resolution Decision Procedures, Handbook of Automated Reasoning, vol.II, pp.1791-1849, 2001.

G. Christian, A. Fermüller, T. Leitsch, N. K. Tammet, and . Zamov, Resolution Methods for the Decision Problem, LNCS, vol.679, 1993.

B. Finkbeiner, C. Müller, H. Seidl, and E. Zalinescu, Verifying Security Policies in Multi-agent Workflows with Loops, Computer and Communications Security (CCS'17), pp.633-645, 2017.

P. Fontaine, Combinations of Theories and the Bernays-Schönfinkel-Ramsey Class, Verification Workshop in connection with CADE-21 (VERIFY'07), 2007.

P. Fontaine, Combinations of Theories for Decidable Fragments of First-Order Logic, Frontiers of Combining Systems (FroCoS'09), vol.5749, pp.263-278
URL : https://hal.archives-ouvertes.fr/inria-00430631

. Springer, , 2009.

J. Fourier, Nouveau Bulletin des Sciences par la Société philomathique de Paris, Oeuvres de Fourier, vol.II, pp.317-319, 1826.

J. Michael, M. O. Fischer, and . Rabin, Super-Exponential Complexity of Presburger Arithmetic, SIAM-AMS Symposium in Applied Mathematics, pp.27-41, 1974.

J. Ferrante and C. Rackoff, A Decision Procedure for the First Order Theory of Real Addition with Order, SIAM Journal of Computing, vol.4, issue.1, pp.69-76, 1975.

J. Ferrante and C. W. Rackoff, The computational complexity of logical theories, 1979.

G. Christian, G. Fermüller, and . Salzer, Ordered Paramodulation and Resolution as Decision Procedure, Logic Programming and Automated Reasoning (LPAR'93), pp.122-133, 1993.

T. W. Frühwirth, E. Y. Shapiro, M. Y. Vardi, and E. Yardeni, Logic Programs as Types for Logic Programs, Logic in Computer Science (LICS'91), pp.300-309, 1991.

M. Fürer, Alternation and the Ackermann Case of the Decision Problem

L. Mathématique, , vol.27, pp.137-162, 1981.

M. Fürer, The computational complexity of the unconstrained limited domino problem (with implications for logical decision problems), Logic and Machines: Decision Problems and Complexity, Proceedings of the Symposium "Rekursive Kombinatorik, pp.312-319, 1983.

A. Fietzke and C. Weidenbach, Superposition as a Decision Procedure for Timed Automata, Mathematics in Computer Science, vol.6, issue.4, pp.409-425, 2012.

H. Gaifman, On Local and Non-Local Properties, Proceedings of the Herbrand Symposium, Logic Colloquium '81, pp.105-135, 1982.

H. Ganzinger, . Shostak, and . Light, Automated Deduction (CADE-18), pp.332-346, 2002.

Y. Ge, C. W. Barrett, and C. Tinelli, Solving quantified verification conditions using satisfiability modulo theories, Ann. Math. Artif. Intell, vol.55, issue.1-2, pp.101-122, 2009.

Y. Ge and L. Mendonça-de-moura, Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories, Computer Aided Verification (CAV'09), vol.5643, pp.306-320, 2009.

H. Ganzinger and . Hans-de-nivelle, A Superposition Decision Procedure for the Guarded Fragment with Equality, Logic in Computer Science (LICS'99), pp.295-303, 1999.

G. Gentzen, Untersuchungenüber das logische Schließen, I. Mathematische Zeitschrift, vol.39, issue.1, pp.176-210, 1935.

G. Gentzen, Untersuchungenüber das logische Schließen, II. Mathematische Zeitschrift, vol.39, issue.1, pp.405-431, 1935.

S. Ghilardi and A. Gianola, Modularity results for interpolation, amalgamation and superamalgamation, Annals in Pure and Applied Logic, vol.169, issue.8, pp.731-754, 2018.

W. D. Goldfarb, Y. Gurevich, and S. Shelah, A Decidable Subclass of the Minimal Gödel Class with Identity, Journal of Symbolic Logic, vol.49, issue.4, pp.1253-1261, 1984.

. Ghk-+-13]-bernardo-cuenca, I. Grau, M. Horrocks, C. Krötzsch, D. Kupke et al., Acyclicity Notions for Existential Rules and Their Application to Query Answering in Ontologies, Journal of Artificial Intelligence Research, vol.47, pp.741-808, 2013.

. Ghn-+-04]-harald, G. Ganzinger, R. Hagen, A. Nieuwenhuis, C. Oliveras et al., DPLL(T): Fast Decision Procedures, Computer Aided Verification (CAV'04), pp.175-188, 2004.

L. Georgieva, U. Hustadt, and R. A. Schmidt, Hyperresolution for Guarded Formulae, Proceedings of the Seventh Workshop on Automated Reasoning, Bridging the Gap between Theory and Practice, 2000.

L. Georgieva, U. Hustadt, and R. A. Schmidt, A New Clausal Class Decidable by Hyperresolution, Automated Deduction (CADE-18), pp.260-274, 2002.

L. Georgieva, U. Hustadt, and R. A. Schmidt, Hyperresolution for guarded formulae, Journal of Symbolic Computation, vol.36, issue.1-2, pp.163-192, 2003.

H. Ganzinger, T. Hillenbrand, and U. Waldmann, Superposition Modulo a Shostak Theory, Finite Model Theory and Its Applications, pp.182-196, 2003.

E. Grädel, G. Phokion, M. Y. Kolaitis, and . Vardi, On the decision problem for two-variable first-order logic, Bulletin of Symbolic Logic, vol.3, issue.1, pp.53-69, 1997.

E. Grädel, J. Kontinen, J. Väänänen, and H. Vollmer, Logics for Dependence and Independence (Dagstuhl Seminar 15261), Dagstuhl Reports, vol.5, issue.6, pp.70-85, 2016.

P. Gács and L. Lovász, Khachiyan's algorithm for linear programming, Mathematical Programming Study, issue.14, pp.61-68, 1981.

S. Ghilardi, E. Nicolini, and D. Zucchelli, A comprehensive combination framework, ACM Transactions on Computational Logic, vol.9, issue.2, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00576602

E. Grädel and M. Otto, On Logics with Two Variables, Theoretical Computer Science, vol.224, issue.1-2, pp.73-113, 1999.

K. Gödel, ;. John, W. Dawson, J. Stephen, C. Kleene et al., English translation in Solomon Feferman, Ein Spezialfall des Entscheidungsproblems der theoretischen Logik. Ergebnisse eines mathematischen Kolloquiums, vol.I, pp.230-233, 1929.

K. Gödel, ;. John, W. Dawson, J. Stephen, C. Kleene et al., Reprinted in Solomon Feferman, Zum Entscheidungsproblem des logischen Funktionenkalküls. Monatshefte für Mathematik und Physik, vol.40, pp.306-326, 1929.

R. Goldberg, On the Solvability of a Subclass of the Suranyi Reduction Class, Journal of Symbolic Logic, vol.28, issue.3, pp.237-244, 1963.

W. D. Goldfarb, The Unsolvability of the Godel Class with Identity, Journal of Symbolic Logic, vol.49, issue.4, pp.1237-1252, 1984.

O. Goldreich, Computational Complexity -A Conceptual Perspective, 2008.

J. Goubault, A BDD-Based Simplification and Skolemization Procedure, Logic Journal of the IGPL, vol.3, issue.6, pp.827-855, 1995.

J. Goubault-larrecq, Deciding H 1 by resolution, Information Processing Letters, vol.95, issue.3, pp.401-408, 2005.

E. Grädel, On solvable cases of Hilbert's 'Entscheidungsproblem'. Habilitationsschrift, 1990.

E. Grädel, Satisfiability of Formulae with One ? is Decidable in Exponential Time, Archive for Mathematical Logic, vol.29, pp.265-276, 1990.

E. Grädel, Invited Talk: Decision procedures for guarded logics, Automated Deduction (CADE-16), pp.31-51, 1999.

E. Grädel, On the Restraining Power of Guards, Journal of Symbolic Logic, vol.64, pp.1719-1742, 1999.

M. Grohe, Finite variable logics in descriptive complexity theory, Bulletin of Symbolic Logic, vol.4, issue.4, pp.345-398, 1998.

R. L. Graham, B. L. Rothschild, and J. H. Spencer, , 1990.

S. Garfunkel, H. James, and . Schmerl, The undecidability of theories of groupoids with an extra predicate, Proceedings of the, vol.42, pp.286-289, 1974.

Y. Gurevich and S. Shelah, Random Models and the Gödel Case of the Decision Problem, Journal of Symbolic Logic, vol.48, issue.4, pp.1120-1124, 1983.

D. Gabbay, R. Schmidt, and A. Sza-las, Second-Order Quantifier Elimination: Foundations, Computational Aspects and Applications, 2008.

Y. Gurevich, The Decision Problem for the Logic of Predicates and Operations. Algebra i Logika, vol.8, pp.284-308, 1969.

Y. Gurevich, Formulas with one ?. In Selected Questions in Algebra and Logic; in memory of A. Malcev, Russian. A German translation is available at TIB Universität Hannover, pp.97-110, 1973.

Y. Gurevich, The Decision Problem for Standard Classes, Journal of Symbolic Logic, vol.41, issue.2, pp.460-464, 1976.

D. Hilbert and W. Ackermann, Grundzüge der theoretischen Logik, 1928.

C. Haase, A Survival Guide to Presburger Arithmetic, SIGLOG News, vol.5, issue.3, pp.67-82, 2018.

J. Y. Halpern, Presburger Arithmetic with Unary Predicates is ? 1

, Complete. Journal of Symbolic Logic, vol.56, issue.2, pp.637-642, 1991.

J. Hartmanis, The Structural Complexity Column: The Collapsing Hierarchies, Bulletin of the European Association for Theoretical Computer Science (EATCS), issue.33, pp.26-39, 1987.

L. Henkin, Some remarks on infinitely long formulas, Infinistic Methods, pp.167-183, 1961.

J. Herbrand, Recherches sur la théorie de la démonstration, English translation in Jacques Herbrand, Logical Writings, 1930.

A. Herzig, A new decidable fragment of first order logic, Abstracts of the Third Logical Biennial, Summer School & Conference in Honour of S. C. Kleene, 1990.

T. Hillenbrand, Superposition and Decision Procedures Back and Forth, 2008.

J. Hintikka, Distributive Normal Forms in First-Order Logic, Formal Systems and Recursive Functions, vol.40, pp.48-91, 1965.

, Jaakko Hintikka. Logic, Language-Games and Information: Kantian Themes in the Philosophy of Logic, 1973.

P. Habermehl, R. Iosif, and T. Vojnar, What Else Is Decidable about Integer Arrays?, Foundations of Software Science and Computational Structures (FOSSACS'08), pp.474-489, 2008.
URL : https://hal.archives-ouvertes.fr/hal-01418914

E. Hoogland and M. Marx, Interpolation in Guarded Fragments, 1999.

E. Hoogland and M. Marx, Interpolation and Definability in Guarded Fragments, Studia Logica, vol.70, issue.3, pp.373-409, 2002.

E. Hoogland, M. Marx, and M. Otto, Beth Definability for the Guarded Fragment, Logic Programming and Automated Reasoning (LPAR'99), pp.273-285, 1999.

J. E. Hopcroft, R. Motwani, and J. D. Ullman, Introduction to Automata Theory, Languages, and Computation, 2001.

T. A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine, Symbolic Model Checking for Real-Time Systems. Information and Computation, vol.111, pp.193-244, 1994.

W. Hodges, Model theory, 1993.

I. M. Hodkinson, Loosely Guarded Fragment of First-Order Logic has the Finite Model Property, Studia Logica, vol.70, issue.2, pp.205-240, 2002.

U. Hustadt, A. Ozaki, and C. Dixon, Theorem Proving for Metric Temporal Logic over the Naturals, Automated Deduction (CADE-26), pp.326-343, 2017.

E. Hoogland, Definability and Interpolation: Model-theoretic investigations, 2001.

D. Harel, A. Pnueli, and J. Stavi, Propositional dynamic logic of nonregular programs, Journal of Computer and System Sciences, vol.26, issue.2, pp.222-243, 1983.

U. Hustadt and R. A. Schmidt, Maslov's Class K Revisited, Automated Deduction (CADE-16), pp.172-186, 1999.

Y. Hamadi and L. Sais, Handbook of Parallel Constraint Reasoning

. Springer, , 2018.

J. Hoffart, F. M. Suchanek, K. Berberich, and G. Weikum, YAGO2: A spatially and temporally enhanced knowledge base from Wikipedia, Artificial Intelligence, vol.194, pp.28-61, 2013.

U. Hustadt, R. A. Schmidt, and L. Georgieva, A survey of decidable firstorder fragments and description logics, Journal on Relational Methods in Computer Science, vol.1, pp.251-276, 2004.

J. E. Hopcroft and J. D. Ullman, Introduction to Automata Theory, Languages, and Computation, 1979.

G. Huang, Constructing Craig Interpolation Formulas, Computing and Combinatorics (COCOON'95), pp.181-190, 1995.

U. Hustadt, Resolution-Based Decision Procedures for Subclasses of First-Order Logic, 1999.

M. Horbach, M. Voigt, and C. Weidenbach, On the Combination of the Bernays-Schönfinkel-Ramsey Fragment with Simple Linear Integer Arithmetic, Automated Deduction (CADE'17), pp.77-94, 2017.

M. Horbach, M. Voigt, and C. Weidenbach, The Universal Fragment of Presburger Arithmetic with Unary Uninterpreted Predicates is Undecidable, ArXiv preprint, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01592177

T. Hillenbrand and C. Weidenbach, Superposition for Bounded Domains, Automated Reasoning and Mathematics -Essays in Memory of William W

A. Mccune-;-shachar-itzhaky, N. Banerjee, A. Immerman, M. Nanevski, A. Sagiv-;-shachar-itzhaky et al., Aleksandar Nanevski, and Mooly Sagiv. Modular reasoning about heap paths via effectively propositional formulas, Shachar Itzhaky, Nikolaj Bjørner, Thomas W. Reps, Mooly Sagiv, and Aditya V, vol.7788, pp.385-396, 2013.

. Thakur, Property-Directed Shape Analysis, Computer Aided Verification (CAV'14), pp.35-51, 2014.

N. Immerman, Nondeterministic Space is Closed Under Complementation, SIAM Journal on Computing, vol.17, issue.5, pp.935-938, 1988.

D. Neil, W. T. Jones, and . Laaser, Complete Problems for Deterministic Polynomial Time, Theoretical Computer Science, vol.3, pp.105-117, 1977.

N. D. Jones, Y. E. Lien, and W. T. Laaser, New problems complete for nondeterministic log space, Mathematical systems theory, vol.10, issue.1, pp.1-17, 1976.

F. Jacquemard, C. Meyer, and C. Weidenbach, Unification in Extensions of Shallow Equational Theories, Rewriting Techniques and Applications (RTA'98), pp.76-90, 1998.
URL : https://hal.archives-ouvertes.fr/inria-00098740

H. William and . Joyner, Resolution Strategies as Decision Procedures, Journal of the ACM, vol.23, issue.3, pp.398-417, 1976.

F. Jacquemard, M. Rusinowitch, and L. Vigneron, Tree Automata with Equality Constraints Modulo Equational Theories, Automated Reasoning (IJCAR'06), pp.557-571, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00329693

L. Kalmár, Über die Erfüllbarkeit derjenigen Zählausdrücke, welche in der Normalform zwei benachbarte Allzeichen enthalten, Mathematische Annalen, vol.108, pp.466-484, 1933.

N. Karmarkar, A new polynomial-time algorithm for linear programming, Combinatorica, vol.4, issue.4, pp.373-395, 1984.

S. Kasif, Property-Directed Inference of Universal Invariants or Proving Their Absence, Shachar Itzhaky, Noam Rinetzky, and Sharon Shoham, pp.583-602, 1986.

L. Gendrichowitsch-khachiyan, Polynomial algorithms in linear programming, USSR Computational Mathematics and Mathematical Physics, vol.20, issue.1, pp.53-72, 1980.

E. Kieronski and A. Kuusisto, Complexity and Expressivity of Uniform One-Dimensional Fragment with Equality, Mathematical Foundations of Computer Science (MFCS'14), pp.365-376, 2014.

M. Micha-l-krynicki and . Mostowski, Henkin Quantifiers, Quantifiers: Logics, Models and Computation, pp.193-263, 1995.

K. Korovin, Inst-Gen -A Modular Approach to Instantiation-Based Automated Reasoning, Programming Logics -Essays in Memory of Harald Ganzinger, pp.239-270, 2013.

K. Korovin, Non-cyclic Sorts for First-Order Satisfiability, Frontiers of Combining Systems (FroCoS'13), vol.8152, pp.214-228, 2013.

M. Ko?ta, New Concepts for Real Quantifier Elimination by Virtual Substitution, 2016.

E. Kiero?ski, I. Pratt-hartmann, and L. Tendera, Two-variable logics with counting and semantic constraints, SIGLOG News, vol.5, issue.3, pp.22-43, 2018.

V. Kuncak, R. Piskac, P. Suter, and T. Wies, Building a Calculus of Data Structures, Verification, Model Checking, and Abstract Interpretation (VMCAI'10), pp.26-44, 2010.

M. Krötzsch and S. Rudolph, Extending Decidable Existential Rules by Joining Acyclicity and Guardedness, Artificial Intelligence (IJCAI'11), pp.963-968, 2011.

R. Melven and . Krom, The Decision Problem for Segregated Formulas in First-Order Logic, Mathematica Scandinavica, vol.21, pp.233-240, 1967.

P. Koopmann, S. Rudolph, R. A. Schmidt, and C. Wernhard, Proceedings of the Workshop on Second-Order Quantifier Elimination and Related Topics (SOQE 2017), volume 2013 of CEUR Workshop Proceedings. CEUR-WS.org, 2017.

E. Kruglov, Superposition Modulo Theory, 2013.

K. Korovin and C. Sticksel, iProver-Eq: An Instantiation-Based Theorem Prover with Equality, Automated Reasoning (IJCAR'10), pp.196-202, 2010.

D. Kroening and O. Strichman, Decision Procedures. Texts in Theoretical Computer Science, An EATCS Series, 2016.

D. G. Kuehner, A note on the relation between resolution and Maslov's inverse method, Machine Intelligence, vol.6, pp.73-76, 1971.

G. Phokion, M. Y. Kolaitis, and . Vardi, 0-1 Laws and Decision Problems for Fragments of Second-Order Logic. Information and Computation, vol.87, pp.301-337, 1990.

L. Kovács and A. Voronkov, First-Order Interpolation and Interpolating Proof Systems, Logic for Programming, Artificial Intelligence and Reasoning (LPAR'17), pp.49-64, 2017.

E. Kruglov and C. Weidenbach, Superposition Decides the First-Order Logic Fragment Over Ground Theories, Mathematics in Computer Science, vol.6, issue.4, pp.427-456, 2012.

A. Leitsch, Deciding Clause Classes by Semantic Clash Resolution. Fundamenta Informaticae, vol.18, pp.163-182, 1993.

A. Leitsch, The Resolution Calculus. Texts in theoretical computer science, An EATCS Series, 1997.

A. Leitsch, Resolution and the Decision Problem, Logic and Foundations of Mathematics: Selected Contributed Papers of the Tenth International Congress of Logic, pp.249-269, 1995.

L. A. Levin, Universal Sequential Search Problems. Problemy peredachi informatsii, vol.9, pp.115-116, 1973.

H. R. Lewis, Complexity of Solvable Cases of the Decision Problem for the Predicate Calculus, Foundations of Computer Science (FOCS'78), pp.35-47, 1978.

H. R. Lewis, Unsolvable Classes of Quantificational Formulas, 1979.

H. R. Lewis, Complexity Results for Classes of Quantificational Formulas, Journal of Computer and System Sciences, vol.21, issue.3, pp.317-353, 1980.

H. R. Lewis, A Logic of Concrete Time Intervals (Extended Abstract), Logic in Computer Science (LICS'90), pp.380-389, 1990.

L. Libkin, Elements of Finite Model Theory. Texts in Theoretical Computer Science, An EATCS Series, 2004.

V. A. Lifshits, Some Reduction Classes and Undecidable Theories, Studies in Constructive Mathematics and Mathematical Logic, vol.4, pp.24-25, 1969.

V. Lifschitz, What Is the Inverse Method, Journal of Automated Reasoning, vol.5, issue.1, pp.1-23, 1989.

N. Leone, M. Manna, G. Terracina, and P. Veltri, Efficiently Computable Datalog? Programs, Knowledge Representation and Reasoning (KR'12), 2012.

H. Martin and . Löb, Decidability of the monadic predicate calculus with unary function symbols, Journal of Symbolic Logic, vol.32, p.563, 1967.

F. Lonsing, Dependency Schemes and Search-Based QBF Solving: Theory and Practice, 2012.

J. Lo?, On the extending of models (I). Fundamenta mathematicae, vol.42, pp.38-54, 1955.

L. Löwenheim, Über Möglichkeiten im Relativkalkül, Mathematische Annalen, vol.76, pp.447-470, 1915.

R. Loos and . Volker-weispfenning, Applying Linear Quantifier Elimination, The Computer Journal, vol.36, issue.5, pp.450-462, 1993.

M. Lamotte, -. Schubert, and C. Weidenbach, BDI: A New Decidable Firstorder Clause Class, Logic for Programming, Artificial Intelligence and Reasoning (LPAR-19), vol.26, pp.62-74, 2013.

M. Lamotte, -. Schubert, and C. Weidenbach, BDI: a new decidable clause class, Journal of Logic and Computation, vol.27, issue.2, pp.441-468, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01098084

R. C. Lyndon, An interpolation theorem in the predicate calculus, Pacific Journal of Mathematics, vol.9, issue.1, pp.129-142, 1959.

M. Mahfoudh, Sur la Vérification de la Satisfaction pour la Logique des Différences, 2003.

M. Marx, Tolerance Logic, Journal of Logic, Language and Information, vol.10, issue.3, pp.353-374, 2001.

S. Yu and . Maslov, An Inverse Method of Establishing Deducibilities in the Classical Predicate Calculus, Doklady Akademii Nauk SSSR, vol.159, pp.1420-1424, 1964.

S. Yu and . Maslov, The Inverse Method for Establishing Deducibility for Logical Calculi (in Russian), English translation in Proceedings of the Steklov Institute of Mathematics, vol.98, pp.25-95, 1968.

A. R. Meyer, The Inherent Computational Complexity of Theories of Ordered Sets, Proceedings of the International Congress of Mathematicians, pp.477-482, 1974.

M. L. Minsky, Computation: finite and infinite machines, 1967.

M. Mahfoudh and P. Niebert, Eugene Asarin, and Oded Maler. A Satisfiability Checker for Difference Logic, Theory and Applications of Satisfiability Testing (SAT'02), pp.222-230, 2002.

S. Y. Maslov and V. P. Orevkov, Decidable classes reducing to a one-quantifier class, Russian. English translation in Proceedings of the Steklov Institute of Mathematics, vol.121, pp.61-72, 1972.

M. Mortimer, On Languages with Two Variables, Mathematical Logic Quarterly, vol.21, issue.1, pp.135-140, 1975.

T. S. Motzkin, Beiträge zur Theorie der Linearen Ungleichungen, 1936.

F. Mogavero and G. Perelli, Binding Forms in First-Order Logic, Computer Science Logic (CSL'15), pp.648-665, 2015.

M. Mugnier, Ontological Query Answering with Existential Rules, Web Reasoning and Rule Systems (RR'11), pp.2-23, 2011.
URL : https://hal.archives-ouvertes.fr/lirmm-00618296

Z. Manna and C. G. Zarba, Combining Decision Procedures. In Formal Methods at the Crossroads. From Panacea to Foundational Support, 10th Anniversary Colloquium of UNU/IIST, the International Institute for Software Technology of The United Nations University, pp.381-422, 2002.

T. Nelson, D. J. Dougherty, K. Fisler, and S. Krishnamurthi, Toward a More Complete Alloy, Abstract State Machines, Alloy, B, VDM, and Z (ABZ'12), pp.136-149, 2012.

G. Nelson, Combining satisfiability procedures by equality-sharing, Contemporary Mathematics, vol.29, pp.201-211, 1984.

, Marius Bozga, Oded Maler, and Navendu Jain. Verification of Timed Automata via Satisfiability Checking, Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT'02), pp.225-244, 1996.

F. Nielson, H. Hanne-riis-nielson, and . Seidl, Normalizable Horn Clauses, Strongly Recognizable Relations, and Spi, Static Analysis (SAS'02), pp.20-35, 2002.

G. Nelson and D. C. Oppen, Simplification by Cooperating Decision Procedures, ACM Transactions on Programming Languages and Systems, vol.1, issue.2, pp.245-257, 1979.

R. Nieuwenhuis and A. Oliveras, DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference Logic, Computer Aided Verification (CAV'05), pp.321-334, 2005.

A. Noah, Predicate-functors and the limits of decidability in logic, Notre Dame Journal of Formal Logic, vol.21, issue.4, pp.701-707, 1980.

A. Nonnengart and C. Weidenbach, Computing Small Clause Normal Forms, Handbook of Automated Reasoning, vol.I, pp.335-367, 2001.

P. Odifreddi, Classical Recursion Theory, Studies in Logic and the Foundations of Mathematics, vol.125, 1992.

D. C. Oppen, Complexity, Convexity and Combinations of Theories. Theoretical Computer Science, vol.12, pp.291-302, 1980.

M. Otto, Bounded Variable Logics and Counting: A Study in Finite Models, Lecture Notes in Logic, vol.9, 1997.

M. Otto, An interpolation theorem, Bulletin of Symbolic Logic, vol.6, issue.4, pp.447-462, 2000.

J. Ouaknine and J. Worrell, Some Recent Results in Metric Temporal Logic, Formal Modeling and Analysis of Timed Systems (FORMATS'08), pp.1-13, 2008.

C. H. Papadimitriou, Computational complexity, 1994.

R. Piskac, L. Mendonça-de-moura, and N. Bjørner, Deciding Effectively Propositional Logic Using DPLL and Substitution Sets, Journal of Automated Reasoning, vol.44, issue.4, pp.401-424, 2010.

D. A. Plaisted, Complete Problems in the First-Order Predicate Calculus, Journal of Computer and System Sciences, vol.29, issue.1, pp.8-35, 1984.

O. Padon, K. L. Mcmillan, A. Panda, M. Sagiv, and S. Shoham, Ivy: safety verification by interactive generalization, Programming Language Design and Implementation (PLDI'16), pp.614-630, 2016.

A. Policriti and E. Omodeo, The Bernays-Schönfinkel-Ramsey class for set theory: decidability, Journal of Symbolic Logic, vol.77, pp.896-918, 2012.

R. Vaughan and . Pratt, Two Easy Theories Whose Combination is Hard, 1977.

M. Presburger, Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt, Sprawozdanie z I Kongresu matematyków krajów s lowia?skich, pp.92-101, 1929.

I. Pratt-hartmann, W. Szwast, and L. Tendera, Quine's Fluted Fragment is Non-Elementary, Computer Science Logic (CSL'16), vol.39, pp.1-39, 2016.

C. William and . Purdy, Decidability of Fluted Logic with Identity, Notre Dame Journal of Formal Logic, vol.37, issue.1, pp.84-104, 1996.

C. William and . Purdy, Fluted Formulas and the Limits of Decidability, Journal of Symbolic Logic, vol.61, issue.2, pp.608-620, 1996.

C. William and . Purdy, Quine's 'Limits of Decision', Journal of Symbolic Logic, vol.64, issue.4, pp.1439-1466, 1999.

C. William and . Purdy, Complexity and Nicety of Fluted Logic, Studia Logica, vol.71, issue.2, pp.177-198, 2002.

H. Putnam, Decidability and Essential Undecidability, Journal of Symbolic Logic, vol.22, issue.1, pp.39-54, 1957.

J. A. , N. Pérez, and A. Voronkov, Encodings of Bounded LTL Model Checking in Effectively Propositional Logic, Automated Deduction (CADE-21), pp.346-361, 2007.

J. A. , N. Pérez, and A. Voronkov, Encodings of Problems in Effectively Propositional Logic, Theory and Applications of Satisfiability Testing (SAT'07), p.3, 2007.

J. A. , N. Pérez, and A. Voronkov, Proof Systems for Effectively Propositional Logic, Automated Reasoning (IJCAR'08), pp.426-440, 2008.

J. A. , N. Pérez, and A. Voronkov, Planning with Effectively Propositional Logic, Programming Logics -Essays in Memory of Harald Ganzinger, pp.302-316, 2013.

K. Quaas, M. Shirmohammadi, and J. Worrell, Revisiting reachability in timed automata, Logic in Computer Science (LICS'17), pp.1-12, 2017.

W. Van-orman-quine, An extended version appeared in W, 14th International Congress of Philosophy, vol.III, pp.57-62, 1969.

W. Van-orman-quine, The Ways of Paradox and other essays. Revised and enlarged edition, 1976.

M. O. Rabin, Decidability of Second-Order Theories and Automata on Infinite Trees, Transactions of the American Mathematical Society, vol.141, pp.1-35, 1969.

C. W. Rackoff, The complexity of theories of the monadic predicate calculus, IRIA Report, vol.136, 1975.

R. Frank-plumpton, On a Problem of Formal Logic, Proceedings of The London Mathematical Society, 1930.

V. Rantala and . Constituents, Jaakko Hintikka, pp.43-76, 1987.

A. Reynolds, H. Barbosa, and P. Fontaine, Revisiting Enumerative Instantiation, Tools and Algorithms for the Construction and Analysis of Systems (TACAS'18), pp.112-131, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01877055

S. Ruggieri, P. Eirinakis, K. Subramani, and P. J. Wojciechowski, On the complexity of quantified linear systems, Theoretical Computer Science, vol.518, pp.128-134, 2014.

A. Reynolds, R. Iosif, and C. Serban, Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic, Verification, Model Checking, and Abstract Interpretation (VMCAI'17), pp.462-482, 2017.

A. Reynolds and V. Kuncak, Induction for SMT Solvers, Verification, Model Checking, and Abstract Interpretation (VMCAI'15), pp.80-98, 2015.

A. Reynolds, T. King, and V. Kuncak, Solving quantified linear arithmetic by counterexample-guided instantiation, Formal Methods in System Design, vol.51, issue.3, pp.500-532, 2017.

J. Robinson, Definability and Decision Problems in Arithmetic, Journal of Symbolic Logic, vol.14, issue.2, pp.98-114, 1949.

H. Rogers, This is a paperback reprint of the 1967 original with the same author, 1987.

S. Ranise, C. Ringeissen, and D. Tran, Nelson-Oppen, Shostak and the Extended Canonizer: A Family Picture with a Newborn, Theoretical Aspects of Computing (ICTAC'04), Revised Selected Papers, pp.372-386, 2004.
URL : https://hal.archives-ouvertes.fr/inria-00099985

S. Ranise, C. Ringeissen, and C. G. Zarba, Combining Data Structures with Nonstably Infinite Theories Using Many-Sorted Logic, Frontiers of Combining Systems (FroCoS'05), pp.48-64, 2005.
URL : https://hal.archives-ouvertes.fr/inria-00070335

H. Rueß and N. Shankar, Deconstructing Shostak, Logic in Computer Science (LICS'01), pp.19-28, 2001.

T. Rebele, F. M. Suchanek, J. Hoffart, J. Biega, E. Kuzey et al., YAGO: A Multilingual Knowledge Base from Wikipedia, Wordnet, and Geonames, The Semantic Web (ISWC'16), pp.177-185, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01369125

A. Reynolds, C. Tinelli, and L. Mendonça-de-moura, Finding conflicting instances of quantified formulas in SMT, Formal Methods in Computer-Aided Design (FMCAD'14), pp.195-202, 2014.

A. John-alan-robinson and . Voronkov, Handbook of Automated Reasoning. I & II, 2001.

M. Samer, Variable Dependencies of Quantified CSPs, Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'08), pp.512-527, 2008.

J. Walter and . Savitch, Relationships between nondeterministic and deterministic tape complexities, Journal of Computer and System Sciences, vol.4, issue.2, pp.177-192, 1970.

A. Schlichtkrull, J. C. Blanchette, D. Traytel, and U. Waldmann, Formalizing Bachmair and Ganzinger's Ordered Resolution Prover, Automated Reasoning (IJCAR'18), pp.89-107, 2018.

A. Sankaran and S. Chakraborty, On Semantic Generalizations of the Bernays-Schönfinkel-Ramsey Class with Finite or Co-finite Spectra, 2010.

K. Schütte, Über die Erfüllbarkeit einer Klasse von logischen Formeln, vol.110, pp.161-194, 1934.

K. Schütte, Untersuchungen zum Entscheidungsproblem der mathematischen Logik, Mathematische Annalen, vol.109, issue.4, pp.572-603, 1934.

A. Schrijver, Theory of linear and integer programming. Wiley-Interscience series in discrete mathematics and optimization, 1999.

, Logic for Computer Scientists, 2008.

S. Schmitz, Complexity Hierarchies beyond Elementary. ACM Transactions on Computation Theory, vol.8, issue.1, pp.1-3, 2016.

D. Scott, A decision method for validity of sentences in two variables, Journal of Symbolic Logic, vol.27, p.477, 1962.

L. Segoufin, A survey on guarded negation, SIGLOG News, vol.4, issue.3, pp.12-26, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01589314

R. A. Schmidt and U. Hustadt, A Resolution Decision Procedure for Fluted Logic, Automated Deduction (CADE-17), pp.433-448, 2000.

S. Shelah, The Monadic Theory of Order, Annals of Mathematics, vol.102, issue.3, pp.379-419, 1975.

S. Shelah, Decidability of a portion of the predicate calculus, Israel Journal on Mathematics, vol.28, pp.32-44, 1977.

R. E. Shostak, Deciding Combinations of Theories, Journal of the ACM, vol.31, issue.1, pp.1-12, 1984.

T. Skolem, Untersuchungenüber die Axiome des Klassenkalküls undüber Produktations-und Summationsprobleme welche gewisse Klassen von Aussagen betreffen, Videnskapsselskapets Skrifter I. Mat.-Nat. Klasse, issue.3, p.1919

, Thoralf Skolem. Ein Satzüber Zählausdrücke. ACTA Scientarium Mathematicarum, vol.7, pp.193-199, 1935.

F. M. Suchanek, G. Kasneci, and G. Weikum, YAGO: A Large Ontology from Wikipedia and WordNet, Journal of Web Semantics, vol.6, issue.3, pp.203-217, 2008.

J. Schulte-mönting, Interpolation formulae for predicates and terms which carry their own history, Archive for Mathematical Logic, vol.17, issue.3-4, pp.159-169, 1975.

R. M. Smullyan, First-Order Logic, 1995.

R. Irving-soare, Recursively Enumerable Sets and Degrees, 1987.

R. Irving-soare, Turing Computability Theory and Applications. Theory and Applications of Computability, In cooperation with the association Computability in Europe, 2016.

V. Sofronie-stokkermans, On Combinations of Local Theory Extensions, Programming Logics -Essays in Memory of Harald Ganzinger, pp.392-413, 2013.

V. Sofronie-stokkermans, Hierarchical Reasoning in Local Theory Extensions and Applications, Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'14), pp.34-41, 2014.

O. Stanislav and . Speranski, Collapsing probabilistic hierarchies. I. Algebra and Logic, vol.52, pp.159-171, 2013.

O. Stanislav and . Speranski, A note on definability in fragments of arithmetic with free unary predicates. Archive for Mathematical Logic, vol.52, pp.507-516, 2013.

N. Shankar and H. Rueß, Combining Shostak Theories, Rewriting Techniques and Applications (RTA'02), pp.1-18, 2002.

H. Seidl and A. Reuß, Extending H 1 -clauses with disequalities, Information Processing Letters, vol.111, issue.20, pp.1007-1013, 2011.

H. Seidl and A. Reuß, Extending H 1 -Clauses with Path Disequalities, Foundations of Software Science and Computational Structures (FOSSACS'12), pp.165-179, 2012.

G. Sutcliffe and C. B. Suttner, The state of CASC, AI Communications, vol.19, issue.1, pp.35-48, 2006.

M. Samer and S. Szeider, Backdoor Sets of Quantified Boolean Formulas, Journal of Automated Reasoning, vol.42, issue.1, pp.77-97, 2009.

O. Strichman, A. Sanjit, R. E. Seshia, and . Bryant, Deciding Separation Formulas with SAT, Computer Aided Verification (CAV'02), pp.209-222, 2002.

R. A. Schmidt and D. Tishkovsky, A General Tableau Method for Deciding Description Logics, Modal Logics and Related First-Order Fragments, Automated Reasoning (IJCAR'08), pp.194-209, 2008.

R. Stansifer, Presburger's Article on Integer Arithmetic: Remarks and Translation, 1984.

, Luc Segoufin and Balder ten Cate. Unary negation, Logical Methods in Computer Science, vol.9, issue.3, 2013.

T. Sturm, A Survey of Some Methods for Real Quantifier Elimination, Decision, and Satisfiability and Their Applications, Mathematics in Computer Science, vol.11, issue.3-4, pp.483-502, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01648690

T. Sturm, Thirty Years of Virtual Substitution: Foundations, Techniques, Applications, Symbolic and Algebraic Computation (ISSAC'18), pp.11-16, 2018.

J. Surányi, Reduktionstheorie des Entscheidungsproblems im Prädikatenkalkül der ersten Stufe. Verlag der Ungarischen Akademie der Wissenschaften, 1959.

G. Sutcliffe, The 9th IJCAR Automated Theorem Proving System Competition -CASC-J9. AI Communications, vol.31, pp.495-507, 2018.

H. Seidl, . Kumar-neeraj, and . Verma, Cryptographic Protocol Verification Using Tractable Classes of Horn Clauses, Program Analysis and Compilation, Theory and Practice, Essays Dedicated to Reinhard Wilhelm on the Occasion of His 60th Birthday, pp.97-119, 2006.

H. Seidl, . Kumar-neeraj, and . Verma, Flat and one-variable clauses: Complexity of verifying cryptographic protocols with single blind copying, ACM Transactions on Computational Logic, vol.9, issue.4, 2008.

T. Sturm, M. Voigt, and C. Weidenbach, Deciding First-Order Satisfiability when Universal and Existential Variables are Separated, IEEE/ACM, 2016. An extended version is available at the arXiv preprint server (arXiv.org) under the signature, pp.86-95
URL : https://hal.archives-ouvertes.fr/hal-01389744

M. Suda, C. Weidenbach, and P. Wischnewski, On the Saturation of YAGO, Automated Reasoning (IJCAR'10), pp.441-456, 2010.

R. Szelepcsényi, The Method of Forced Enumeration for Nondeterministic Automata, Acta Informatica, vol.26, issue.3, pp.279-284, 1988.

T. Tammet, Resolution methods for decision problems and finite-model building, 1991.

T. Tammet, Using Resolution for Extending KL-ONE-type Languages, Information and Knowledge Management (CIKM'95), pp.326-332, 1995.

A. Tarski, Contributions to the theory of models, vol.XVI, pp.572-581, 1954.

A. Tarski, A Decision Method for Elementary Algebra and Geometry, 1948.

A. Tarski, A Decision Method for Elementary Algebra and Geometry, Quantifier Elimination and Cylindrical Algebraic Decomposition, pp.24-84, 1998.

A. Teucke, An Approximation and Refinement Approach to First-Order Automated Reasoning, 2017.

C. Tinelli and M. T. Harandi, A New Correctness Proof of the Nelson-Oppen Combination Procedure, Frontiers of Combining Systems (FroCoS'96), pp.103-119, 1996.

C. Tinelli and C. Ringeissen, Unions of non-disjoint theories and combinations of satisfiability procedures, Theoretical Computer Science, vol.290, issue.1, pp.291-353, 2003.
URL : https://hal.archives-ouvertes.fr/inria-00099668

B. A. Trakhtenbrot, A Survey of Russian Approaches to Perebor (Brute-Force Search) Algorithms, IEEE Annals of the History of Computing, vol.6, issue.4, pp.384-400, 1984.

D. Tran, C. Ringeissen, S. Ranise, and H. Kirchner, Combination of convex theories: Modularity, deduction completeness, and explanation, Journal of Symbolic Computation, vol.45, issue.2, pp.261-286, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00331479

A. S. Troelstra and H. Schwichtenberg, Basic Proof Theory, Cambridge Tracts in Theoretical Computer Science, vol.43, 1996.

M. Talupur, N. Sinha, O. Strichman, and A. Pnueli, Range Allocation for Separation Logic, Computer Aided Verification (CAV'04), pp.148-161, 2004.

A. Mathison and T. , On Computable Numbers, with an Application to the Entscheidungsproblem, Proceedings of the, pp.230-265, 1936.

A. Mathison and T. , On Computable Numbers, with an Application to the Entscheidungsproblem. A Correction, Proceedings of the, pp.544-546, 1938.

A. Teucke and C. Weidenbach, First-Order Logic Theorem Proving and Model Building via Approximation and Instantiation, Frontiers of Combining Systems (FroCoS'15), pp.85-100, 2015.

A. Teucke and C. Weidenbach, Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints, Automated Deduction (CADE-26), pp.202-219, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01657026

C. Tinelli and C. G. Zarba, Combining Nonstably Infinite Theories, Journal of Automated Reasoning, vol.34, issue.3, pp.209-238, 2005.

A. Jouko and . Väänänen, Dependence Logic -A New Approach to Independence Friendly Logic, vol.70, 2007.

J. Van-benthem, Dynamic bits and pieces, 1997.

D. Van-dalen, Logic and Structure, 2013.

M. Veanes, Computational Complexity of Basic Decision Problems of Finite Tree Automata, 1997.

M. Veanes, On Simultaneous Rigid E-Unification, 1997.

. Jean-van-heijenoort, From Frege to Gödel -A Source Book in Mathematical Logic, pp.1879-1931, 2002.

M. Voigt, The Bernays-Schönfinkel-Ramsey Fragment with Bounded Difference Constraints over the Reals is Decidable, Frontiers of Combining Systems (Fro-CoS'17), pp.244-261, 2017.

M. Voigt, A Fine-Grained Hierarchy of Hard Problems in the Separated Fragment, IEEE/ACM, 2017. An extended version is available at the arXiv preprint server (arXiv.org) under the signature, pp.1-12
URL : https://hal.archives-ouvertes.fr/hal-01592172

M. Voigt, On Generalizing Decidable Standard Prefix Classes of First-Order Logic, ArXiv preprint, 2017.

M. Voigt, Towards Elimination of Second-Order Quantifiers in the Separated Fragment, Proceedings of the Workshop on Second-Order Quantifier Elimination and Related Topics (SOQE 2017), pp.67-81, 2017.

M. Voigt and C. Weidenbach, Bernays-Schönfinkel-Ramsey with Simple Bounds is NEXPTIME-complete, 2015.

. Volker-weispfenning, The Complexity of Linear Problems in Fields, Journal of Symbolic Computation, vol.5, issue.1/2, pp.3-27, 1988.

. Volker-weispfenning, Quantifier Elimination for Real Algebra -the Quadratic Case and Beyond. Applicable Algebra in Engineering, vol.8, pp.85-101, 1997.

C. Weidenbach, Automated Deduction -A Basis for Applications, Applied Logic Series, vol.I, pp.291-320, 1998.

C. Weidenbach, Towards an Automatic Analysis of Security Protocols in First-Order Logic, Automated Deduction (CADE-16), vol.1632, pp.314-328

. Springer, , 1999.

C. Wernhard, Heinrich Behmann's Contributions to Second-Order Quantifier Elimination from the View of Computational Logic, 2015.

C. Wernhard, Second-Order Quantifier Elimination on Relational Monadic Formulas -A Basic Method and Some Less Expected Applications, Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX'15), pp.253-269, 2015.

C. Wang, A. Gupta, and M. K. Ganai, Predicate Learning and Selective Theory Deduction for a Difference Logic Solver, Design Automation Conference (DAC'06), pp.235-240, 2006.

H. and P. Williams, Fourier's Method of Linear Programming and Its Dual, The American Mathematical Monthly, vol.93, issue.9, pp.681-695, 1986.

M. Wirsing, Das Entscheidungsproblem der Prädikatenlogik 1. Stufe mit Identität und Funktionszeichen in Herbrandformeln, 1976.

M. Wirsing, Das Entscheidungsproblem der Klasse von Formeln, die höchstens zwei Primformeln enthalten, Manuscripta Mathematica, vol.22, pp.13-25, 1977.

M. Wirsing, Kleine unentscheidbare Klassen der Prädikatenlogik mit Identität und Funktionszeichen. Archiv für mathematische Logik und Grundlagenforschung, vol.19, pp.97-109, 1978.

P. Wischnewski, Efficient Reasoning Procedures for Complex First-Order Theories, 2012.

T. Wies, R. Piskac, and V. Kuncak, Combining Theories with Shared Set Operations, Frontiers of Combining Systems (FroCoS'09), vol.5749, pp.366-382, 2009.

N. K. Zamov, On a Connection Between the Resolution Method and the Inverse Method, Fundamentals of Computation Theory (FCT'87), pp.501-505, 1987.