NRCL ? A Model Building Approach to the Bernays?Schönfinkel Fragment, Frontiers of Combining Systems (FroCoS'15), pp.69-84, 2015. ,
Lemma Learning in the Model Evolution Calculus, Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-13), pp.572-586, 2006. ,
DOI : 10.1007/11916277_39
Zum Entscheidungsproblem der mathematischen Logik, Mathematische Annalen, vol.86, issue.Heft 3/4, pp.342-372, 1928. ,
DOI : 10.1007/BF01459101
SGGS Theorem Proving: an Exposition, Workshop on Practical Aspects in Automated Reasoning (PAAR'14), EPiC 31, pp.25-38, 2014. ,
The Classical Decision Problem, 1997. ,
DOI : 10.1007/978-3-642-59207-2
The light side of interval temporal logic: the Bernays-Sch??nfinkel fragment of CDT, Annals of Mathematics and Artificial Intelligence, vol.1, issue.4, pp.1-311, 2014. ,
DOI : 10.1007/s10472-013-9337-y
On the Complexity of the Bernays? Schönfinkel Class with Datalog, Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-17), pp.187-201, 2010. ,
Automated Inference of Finite Unsatisfiability, Journal of Automated Reasoning, vol.19, issue.1, pp.111-132, 2011. ,
DOI : 10.1007/s10817-010-9216-8
The Decision Problem: Solvable Classes of Quantificational Formulas, 1979. ,
Mathematical Logic, 1994. ,
DOI : 10.1007/978-1-4757-2355-7
Resolution Decision Procedures, Handbook of Automated Reasoning, pp.1791-1849, 2001. ,
DOI : 10.1016/B978-044450813-3/50027-8
Combinations of theories for decidable fragments of firstorder logic, Frontiers of Combining Systems (FroCoS'09), pp.263-278, 2009. ,
URL : https://hal.archives-ouvertes.fr/inria-00430631
New directions in instantiation-based theorem proving, 18th Annual IEEE Symposium of Logic in Computer Science, 2003. Proceedings., pp.55-64, 2003. ,
DOI : 10.1109/LICS.2003.1210045
Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories, Computer Aided Verification (CAV'09), pp.306-320, 2009. ,
DOI : 10.1007/978-3-642-02658-4_25
The Decision Problem for the Logic of Predicates and Operations. Algebra i Logika, pp.284-308, 1969. ,
Some remarks on infinitely long formulas, Infinistic Methods, pp.167-183, 1961. ,
Superposition for Bounded Domains, Automated Reasoning and Mathematics ? Essays in Memory of William W. McCune, pp.68-100, 2013. ,
DOI : 10.1007/978-3-540-71067-7_7
From Resolution and DPLL to Solving Arithmetic Constraints, Frontiers of Combining Systems (FroCoS'13), pp.261-262, 2013. ,
DOI : 10.1007/978-3-642-40885-4_18
Non-cyclic Sorts for First-Order Satisfiability, Frontiers of Combining Systems (FroCoS'13), pp.214-228, 2013. ,
DOI : 10.1007/978-3-642-40885-4_15
Complexity results for classes of quantificational formulas, Journal of Computer and System Sciences, vol.21, issue.3, pp.317-353, 1980. ,
DOI : 10.1016/0022-0000(80)90027-6
Decidability of the monadic predicate calculus with unary function symbols, 22] L. Löwenheim. ¨ Uber Möglichkeiten im Relativkalkül. Mathematische Annalen, pp.563447-470, 1915. ,
Computing Small Clause Normal Forms, Handbook of Automated Reasoning, pp.335-367, 2001. ,
DOI : 10.1016/B978-044450813-3/50008-4
Deciding Effectively Propositional Logic Using DPLL and Substitution Sets, Journal of Automated Reasoning, vol.53, issue.6, pp.401-424, 2010. ,
DOI : 10.1007/s10817-009-9161-6
Abstract, The Journal of Symbolic Logic, vol.75, issue.03, pp.896-918, 2012. ,
DOI : 10.1016/0743-1066(95)00147-6
On a Problem of Formal Logic, Proceedings of The London Mathematical Society, pp.2-30264, 1930. ,
Ein Satz ???ber Untermengen einer endlichen Menge, Mathematische Zeitschrift, vol.27, issue.1, pp.544-548, 1928. ,
DOI : 10.1007/BF01171114
Deciding First-Order Satisfiability when Universal and Existential Variables are Separated (Extended Version) ArXiv, p.2016 ,
Towards an Automatic Analysis of Security Protocols in First-Order Logic, Automated Deduction (CADE-16), pp.314-328, 1999. ,
DOI : 10.1007/3-540-48660-7_29
Combining Theories with Shared Set Operations, Frontiers of Combining Systems (FroCoS'09), pp.366-382, 2009. ,
DOI : 10.1016/S0304-3975(01)00332-2