, 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
Computational Complexity -A Modern Approach, 2009. ,
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 SAT-based Decision Procedure for the Boolean Combination of Difference Constraints, Theory and Applications of Satisfiability Testing (SAT'04), 2004. ,
Über die Erfüllbarkeit gewisser Zählausdrücke, Mathematische Annalen, vol.100, pp.638-649, 1928. ,
Untersuchungenüber das Eliminationsproblem der mathematischen Logik, Mathematische Annalen, vol.110, pp.390-413, 1935. ,
Solvable Cases of the Decision Problem, 1954. ,
Automata For Modeling Real-Time Systems, Automata, Languages and Programming (ICALP'90), pp.322-335, 1990. ,
A Theory of Timed Automata, Theoretical Computer Science, vol.126, issue.2, pp.183-235, 1994. ,
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
The Finite Controllability of the Maslov Case, Journal of Symbolic Logic, vol.39, issue.3, pp.509-518, 1974. ,
A Really Temporal Logic, Journal of the ACM, vol.41, issue.1, pp.181-204, 1994. ,
Jouko Väänänen, and Heribert Vollmer, Dependence Logic, Theory and Applications, 2016. ,
Superposition Modulo Linear Arithmetic SUP(LA), Frontiers of Combining Systems (FroCoS'09), pp.84-99, 2009. ,
Finite model reasoning over existential rules. Theory and Practice of Logic Programming, vol.17, pp.726-743, 2017. ,
Modal Languages and Bounded Fragments of Predicate Logic, Journal of Philosophical Logic, vol.27, issue.3, pp.217-274, 1998. ,
Decidable Fragments of Many-Sorted Logic, Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'07), pp.17-31, 2007. ,
Decidable Fragments of Many-Sorted Logic, Journal of Symbolic Computation, vol.45, issue.2, pp.153-172, 2010. ,
NRCL -A Model Building Approach to the Bernays-Schönfinkel Fragment, Frontiers of Combining Systems (FroCoS'15), vol.9322, pp.69-84, 2015. ,
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
Dependency Schemes in QBF Calculi: Semantics and Soundness, Principles and Practice of Constraint Programming (CP'16), pp.96-112, 2016. ,
Computability and Logic, 2002. ,
Combining Existential Rules and Transitivity: Next Steps, Artificial Intelligence (IJCAI'15), pp.2720-2726, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01171846
Rewriting Guarded Negation Queries, Mathematical Foundations of Computer Science (MFCS'13), pp.98-110, 2013. ,
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. ,
Modal Logic, Cambridge Tracts in Theoretical Computer Science, vol.53, 2002. ,
URL : https://hal.archives-ouvertes.fr/inria-00100503
Beiträge zur Algebra der Logik, insbesondere zum Entscheidungsproblem, Mathematische Annalen, vol.86, issue.3-4, pp.163-229, 1922. ,
Normal Form Transformations, Handbook of Automated Reasoning, vol.I, pp.273-333, 2001. ,
The undecidability of the domino problem, 1966. ,
The Complexitiy of Logical Theories, Theoretical Computer Science, vol.11, pp.71-77, 1980. ,
Computing finite models by reduction to function-free clause logic, Journal of Applied Logic, vol.7, issue.1, pp.58-74, 2009. ,
A Non-Elementary Speed-Up in Proof Length by Structural Clause Form Transformation, Logic in Computer Science (LICS'94), pp.213-219, 1994. ,
, Helmut Veith, and Roderick Bloem, pp.1001-1046, 2018.
Resolution Theorem Proving, Handbook of Automated Reasoning, vol.I, pp.19-99, 2001. ,
The Classical Decision Problem, Perspectives in Mathematical Logic, 1997. ,
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
Theorem Proving for Hierarchic First-Order Theories, Algebraic and Logic Programming (ALP'92), pp.420-434, 1992. ,
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. ,
Refutational Theorem Proving for Hierarchic First-Order Theories. Applicable Algebra in Engineering, Communication and Computing, vol.5, pp.193-212, 1994. ,
Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications, 2009. ,
Interpolation Systems for Ground Proofs in Automated Deduction: a Survey, Journal of Automated Reasoning, vol.54, issue.4, pp.353-390, 2015. ,
On Interpolation in Automated Theorem Proving, Journal of Automated Reasoning, vol.54, issue.1, pp.69-97, 2015. ,
Principles of model checking, 2008. ,
On Skolemization and Proof Complexity, Fundamenta Informaticae, vol.20, issue.4, pp.353-379, 1994. ,
Methods of Cut-Elimination, Trends in Logic, vol.34, 2011. ,
Walking the Decidability Line for Rules with Existential Variables, Knowledge Representation and Reasoning (KR'10), 2010. ,
URL : https://hal.archives-ouvertes.fr/lirmm-00535780
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. ,
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. ,
The Calculus of Computation -Decision Procedures with Applications to Verification, Texts in Theoretical Computer Science. An EATCS Series, 2007. ,
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. ,
On Solving Universally Quantified Horn Clauses, Static Analysis (SAS'13), pp.105-125, 2013. ,
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
What's Decidable About Arrays, Verification, Model Checking, and Abstract Interpretation (VMCAI'06), pp.427-442, 2006. ,
Term Rewriting and All That, 1998. ,
Characterization of the Expressive Power of Silent Transitions in Timed Automata, Fundamenta Informaticae, vol.36, issue.2-3, pp.145-182, 1998. ,
Safety Analysis of Systems, 2007. ,
Zum Entscheidungsproblem der mathematischen Logik, Mathematische Annalen, vol.99, issue.1, pp.342-372, 1928. ,
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. ,
Satisfiability Modulo Theories ,
URL : https://hal.archives-ouvertes.fr/hal-01095009
, Helmut Veith, and Roderick Bloem, pp.305-343, 2018.
Guarded negation, Automata, Languages and Programming (ICALP'11), Part II, pp.356-367, 2011. ,
Balder ten Cate, and Luc Segoufin. Guarded Negation, Journal of the ACM, vol.62, issue.3, p.22, 2015. ,
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. ,
Weak second-order arithmetic and finite automata, Logik und Grundlagen der Mathematik, vol.6, pp.66-92, 1960. ,
On a decision method in restricted second order arithmetic, Proceedings of the 1960 International Congress on Logic, pp.1-11, 1962. ,
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
Hierarchic superposition with weak abstraction, Automated Deduction (CADE-24), vol.7898, pp.39-57, 2013. ,
URL : https://hal.archives-ouvertes.fr/hal-00931919
Information and Randomness : An Algorithmic Perspective. Springer, second, revised and extended edition, 2002. ,
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
Tree Automata Techniques and Applications, 2008. ,
A Gentle Non-Disjoint Combination of Satisfiability Procedures, Automated Reasoning (IJCAR'14), pp.122-136, 2014. ,
URL : https://hal.archives-ouvertes.fr/hal-00985135
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
Advanced Processing for Ontological Queries, Proceedings of VLDB, vol.3, pp.554-565, 2010. ,
Query Answering under Nonguarded Rules in Datalog+/?, Web Reasoning and Rule Systems (RR'10), pp.1-17, 2010. ,
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. ,
Correction to A Note on the Entscheidungsproblem, Journal of Symbolic Logic, vol.1, issue.3, pp.101-102, 1936. ,
A Note on the Entscheidungsproblem, Journal of Symbolic Logic, vol.1, issue.1, pp.40-41, 1936. ,
An Unsolvable Problem of Elementary Number Theory, Journal of Symbolic Logic, vol.1, issue.2, pp.73-74, 1936. ,
Handbook of Model Checking, 2018. ,
Multiple Counters Automata, Safety Analysis and Presburger Arithmetic, Computer Aided Verification (CAV'98), pp.268-279, 1998. ,
Timed automata and the theory of real numbers, Concurrency Theory (CONCUR'99), pp.242-257, 1999. ,
Model Theory, Studies in Logic and the Foundations of Mathematics, vol.73, 1990. ,
Strategies for combining decision procedures, Theoretical Computer Science, vol.354, issue.2, pp.187-210, 2006. ,
Embedded Implicational Dependencies and their Inference Problem, Symposium on Theory of Computing (STOC'81), pp.342-354, 1981. ,
Decision procedures for constraint-based extensions of Datalog, Constraint Logic Programming, pp.17-32, 1993. ,
Fast and Flexible Difference Constraint Propagation for DPLL(T), Theory and Applications of Satisfiability Testing (SAT'06), pp.170-183, 2006. ,
Computational Complexity and Constraint Logic Programming Languages, Annals of Mathematics and Artificial Intelligence, vol.5, issue.2-4, pp.163-189, 1992. ,
On the strength and scope of DLS, Journal of Applied Non-Classical Logics, vol.16, issue.3-4, pp.279-296, 2006. ,
The Complexity of Theorem-Proving Procedures, Theory of Computing (STOC'71), pp.151-158, 1971. ,
Theorem Proving in Arithmetic without Multiplication, Machine Intelligence, vol.7, pp.91-99, 1972. ,
Computability Theory, 2004. ,
Linear Reasoning. A New Form of the Herbrand-Gentzen Theorem, Journal of Symbolic Logic, vol.22, issue.3, p.1957 ,
Three Uses of the Herbrand-Gentzen Theorem in Relating Model Theory and Proof Theory, Journal of Symbolic Logic, vol.22, issue.3, p.1957 ,
Introduction to Algorithms, 2001. ,
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. ,
Finite models and finitely many variables, Logic, Algebra and Computer Science, vol.46, pp.93-117, 1999. ,
Fourier-Motzkin Elimination and Its Dual, Journal of Combinatorial Theory, Series A, vol.14, issue.3, pp.288-297, 1973. ,
Verification of Hybrid Systems, Handbook of Model Checking, pp.1047-1110, 2018. ,
The Decision Problem: Solvable Classes of Quantificational Formulas, 1979. ,
Model Theory Makes Formulas Large, Automata, Languages and Programming (ICALP'07), pp.913-924, 2007. ,
Model Theory Makes Formulas Large, 2007. ,
Algorithmic Randomness and Complexity, 2010. ,
, Systems of Linear Inequalities, vol.20, pp.191-199, 1919.
Classification of AEA Formulas by Letter Atoms, Bulletin of the American Mathematical Society, vol.68, issue.5, pp.528-532, 1962. ,
The Complexity of the Satisfiability Problem for Krom Formulas, Theoretical Computer Science, vol.30, pp.319-341, 1984. ,
Logical Syntax and Computational Complexity, Computation and Proof Theory. Proceedings of the Logic Colloquium '83, pp.101-115, 1984. ,
Satisfiability Modulo Theories: Introduction and Applications, Communications of the ACM, vol.54, issue.9, pp.69-77, 2011. ,
A Resolution Decision Procedure for the Guarded Fragment, Automated Deduction (CADE-15), pp.191-204, 1998. ,
Deciding the guarded fragments by resolution, Journal of Symbolic Computation, vol.35, issue.1, pp.21-58, 2003. ,
A Resolution-Based Decision Procedure for the Two-Variable Fragment with Equality, Automated Reasoning (IJCAR'01), pp.211-225, 2001. ,
Simplify: a theorem prover for program checking, Journal of the ACM, vol.52, issue.3, pp.365-473, 2005. ,
Algorithmic strategies for applicable real quantifier elimination, 2000. ,
Undecidability of Presburger Arithmetic with a Single Monadic Predicate Letter, 1972. ,
Solvable Surányi subclasses: an introduction to the Herbrand theory, vol.31, pp.32-47, 1962. ,
Finite model theory. Second Edition. Perspectives in Mathematical Logic, 1999. ,
Mathematical Logic, 1994. ,
On the Value of Antiprenexing, Logic Programming and Automated Reasoning (LPAR'94), pp.69-83, 1994. ,
Superposition Modulo Non-linear Arithmetic, Frontiers of Combining Systems (FroCoS'11), pp.119-134, 2011. ,
EPR-Based Bounded Model Checking at Word Level, Automated Reasoning (IJCAR'12), pp.210-224, 2012. ,
Encoding industrial hardware verification problems into effectively propositional logic, Formal Methods in Computer-Aided Design (FMCAD'10), pp.137-144, 2010. ,
A mathematical introduction to logic, 1972. ,
A mathematical introduction to logic, 2001. ,
Essentials of Constraint Programming ,
, , 2003.
, Parameterized Complexity Theory. Texts in Theoretical Computer Science. An EATCS Series, 2006.
Labelled Superposition, 2013. ,
First-Order Logic and Automated Theorem Proving, Second Edition. Graduate Texts in Computer Science, 1996. ,
An Explicating Theorem Prover for Quantified Formulas, 2004. ,
Resolution Decision Procedures, Handbook of Automated Reasoning, vol.II, pp.1791-1849, 2001. ,
Resolution Methods for the Decision Problem, LNCS, vol.679, 1993. ,
Verifying Security Policies in Multi-agent Workflows with Loops, Computer and Communications Security (CCS'17), pp.633-645, 2017. ,
Combinations of Theories and the Bernays-Schönfinkel-Ramsey Class, Verification Workshop in connection with CADE-21 (VERIFY'07), 2007. ,
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
, , 2009.
Nouveau Bulletin des Sciences par la Société philomathique de Paris, Oeuvres de Fourier, vol.II, pp.317-319, 1826. ,
Super-Exponential Complexity of Presburger Arithmetic, SIAM-AMS Symposium in Applied Mathematics, pp.27-41, 1974. ,
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. ,
The computational complexity of logical theories, 1979. ,
Ordered Paramodulation and Resolution as Decision Procedure, Logic Programming and Automated Reasoning (LPAR'93), pp.122-133, 1993. ,
Logic Programs as Types for Logic Programs, Logic in Computer Science (LICS'91), pp.300-309, 1991. ,
Alternation and the Ackermann Case of the Decision Problem ,
, , vol.27, pp.137-162, 1981.
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. ,
Superposition as a Decision Procedure for Timed Automata, Mathematics in Computer Science, vol.6, issue.4, pp.409-425, 2012. ,
On Local and Non-Local Properties, Proceedings of the Herbrand Symposium, Logic Colloquium '81, pp.105-135, 1982. ,
, Automated Deduction (CADE-18), pp.332-346, 2002.
Solving quantified verification conditions using satisfiability modulo theories, Ann. Math. Artif. Intell, vol.55, issue.1-2, pp.101-122, 2009. ,
Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories, Computer Aided Verification (CAV'09), vol.5643, pp.306-320, 2009. ,
A Superposition Decision Procedure for the Guarded Fragment with Equality, Logic in Computer Science (LICS'99), pp.295-303, 1999. ,
Untersuchungenüber das logische Schließen, I. Mathematische Zeitschrift, vol.39, issue.1, pp.176-210, 1935. ,
Untersuchungenüber das logische Schließen, II. Mathematische Zeitschrift, vol.39, issue.1, pp.405-431, 1935. ,
Modularity results for interpolation, amalgamation and superamalgamation, Annals in Pure and Applied Logic, vol.169, issue.8, pp.731-754, 2018. ,
A Decidable Subclass of the Minimal Gödel Class with Identity, Journal of Symbolic Logic, vol.49, issue.4, pp.1253-1261, 1984. ,
Acyclicity Notions for Existential Rules and Their Application to Query Answering in Ontologies, Journal of Artificial Intelligence Research, vol.47, pp.741-808, 2013. ,
DPLL(T): Fast Decision Procedures, Computer Aided Verification (CAV'04), pp.175-188, 2004. ,
Hyperresolution for Guarded Formulae, Proceedings of the Seventh Workshop on Automated Reasoning, Bridging the Gap between Theory and Practice, 2000. ,
A New Clausal Class Decidable by Hyperresolution, Automated Deduction (CADE-18), pp.260-274, 2002. ,
Hyperresolution for guarded formulae, Journal of Symbolic Computation, vol.36, issue.1-2, pp.163-192, 2003. ,
Superposition Modulo a Shostak Theory, Finite Model Theory and Its Applications, pp.182-196, 2003. ,
On the decision problem for two-variable first-order logic, Bulletin of Symbolic Logic, vol.3, issue.1, pp.53-69, 1997. ,
Logics for Dependence and Independence (Dagstuhl Seminar 15261), Dagstuhl Reports, vol.5, issue.6, pp.70-85, 2016. ,
Khachiyan's algorithm for linear programming, Mathematical Programming Study, issue.14, pp.61-68, 1981. ,
A comprehensive combination framework, ACM Transactions on Computational Logic, vol.9, issue.2, 2008. ,
URL : https://hal.archives-ouvertes.fr/inria-00576602
On Logics with Two Variables, Theoretical Computer Science, vol.224, issue.1-2, pp.73-113, 1999. ,
English translation in Solomon Feferman, Ein Spezialfall des Entscheidungsproblems der theoretischen Logik. Ergebnisse eines mathematischen Kolloquiums, vol.I, pp.230-233, 1929. ,
Reprinted in Solomon Feferman, Zum Entscheidungsproblem des logischen Funktionenkalküls. Monatshefte für Mathematik und Physik, vol.40, pp.306-326, 1929. ,
On the Solvability of a Subclass of the Suranyi Reduction Class, Journal of Symbolic Logic, vol.28, issue.3, pp.237-244, 1963. ,
The Unsolvability of the Godel Class with Identity, Journal of Symbolic Logic, vol.49, issue.4, pp.1237-1252, 1984. ,
Computational Complexity -A Conceptual Perspective, 2008. ,
A BDD-Based Simplification and Skolemization Procedure, Logic Journal of the IGPL, vol.3, issue.6, pp.827-855, 1995. ,
Deciding H 1 by resolution, Information Processing Letters, vol.95, issue.3, pp.401-408, 2005. ,
On solvable cases of Hilbert's 'Entscheidungsproblem'. Habilitationsschrift, 1990. ,
Satisfiability of Formulae with One ? is Decidable in Exponential Time, Archive for Mathematical Logic, vol.29, pp.265-276, 1990. ,
Invited Talk: Decision procedures for guarded logics, Automated Deduction (CADE-16), pp.31-51, 1999. ,
On the Restraining Power of Guards, Journal of Symbolic Logic, vol.64, pp.1719-1742, 1999. ,
Finite variable logics in descriptive complexity theory, Bulletin of Symbolic Logic, vol.4, issue.4, pp.345-398, 1998. ,
, , 1990.
The undecidability of theories of groupoids with an extra predicate, Proceedings of the, vol.42, pp.286-289, 1974. ,
Random Models and the Gödel Case of the Decision Problem, Journal of Symbolic Logic, vol.48, issue.4, pp.1120-1124, 1983. ,
Second-Order Quantifier Elimination: Foundations, Computational Aspects and Applications, 2008. ,
The Decision Problem for the Logic of Predicates and Operations. Algebra i Logika, vol.8, pp.284-308, 1969. ,
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. ,
The Decision Problem for Standard Classes, Journal of Symbolic Logic, vol.41, issue.2, pp.460-464, 1976. ,
Grundzüge der theoretischen Logik, 1928. ,
A Survival Guide to Presburger Arithmetic, SIGLOG News, vol.5, issue.3, pp.67-82, 2018. ,
Presburger Arithmetic with Unary Predicates is ? 1 ,
, Complete. Journal of Symbolic Logic, vol.56, issue.2, pp.637-642, 1991.
The Structural Complexity Column: The Collapsing Hierarchies, Bulletin of the European Association for Theoretical Computer Science (EATCS), issue.33, pp.26-39, 1987. ,
Some remarks on infinitely long formulas, Infinistic Methods, pp.167-183, 1961. ,
Recherches sur la théorie de la démonstration, English translation in Jacques Herbrand, Logical Writings, 1930. ,
A new decidable fragment of first order logic, Abstracts of the Third Logical Biennial, Summer School & Conference in Honour of S. C. Kleene, 1990. ,
Superposition and Decision Procedures Back and Forth, 2008. ,
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.
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
Interpolation in Guarded Fragments, 1999. ,
Interpolation and Definability in Guarded Fragments, Studia Logica, vol.70, issue.3, pp.373-409, 2002. ,
Beth Definability for the Guarded Fragment, Logic Programming and Automated Reasoning (LPAR'99), pp.273-285, 1999. ,
Introduction to Automata Theory, Languages, and Computation, 2001. ,
Symbolic Model Checking for Real-Time Systems. Information and Computation, vol.111, pp.193-244, 1994. ,
Model theory, 1993. ,
Loosely Guarded Fragment of First-Order Logic has the Finite Model Property, Studia Logica, vol.70, issue.2, pp.205-240, 2002. ,
Theorem Proving for Metric Temporal Logic over the Naturals, Automated Deduction (CADE-26), pp.326-343, 2017. ,
Definability and Interpolation: Model-theoretic investigations, 2001. ,
Propositional dynamic logic of nonregular programs, Journal of Computer and System Sciences, vol.26, issue.2, pp.222-243, 1983. ,
Maslov's Class K Revisited, Automated Deduction (CADE-16), pp.172-186, 1999. ,
Handbook of Parallel Constraint Reasoning ,
, , 2018.
YAGO2: A spatially and temporally enhanced knowledge base from Wikipedia, Artificial Intelligence, vol.194, pp.28-61, 2013. ,
A survey of decidable firstorder fragments and description logics, Journal on Relational Methods in Computer Science, vol.1, pp.251-276, 2004. ,
Introduction to Automata Theory, Languages, and Computation, 1979. ,
Constructing Craig Interpolation Formulas, Computing and Combinatorics (COCOON'95), pp.181-190, 1995. ,
Resolution-Based Decision Procedures for Subclasses of First-Order Logic, 1999. ,
On the Combination of the Bernays-Schönfinkel-Ramsey Fragment with Simple Linear Integer Arithmetic, Automated Deduction (CADE'17), pp.77-94, 2017. ,
The Universal Fragment of Presburger Arithmetic with Unary Uninterpreted Predicates is Undecidable, ArXiv preprint, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01592177
Superposition for Bounded Domains, Automated Reasoning and Mathematics -Essays in Memory of William W ,
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. ,
Property-Directed Shape Analysis, Computer Aided Verification (CAV'14), pp.35-51, 2014. ,
Nondeterministic Space is Closed Under Complementation, SIAM Journal on Computing, vol.17, issue.5, pp.935-938, 1988. ,
Complete Problems for Deterministic Polynomial Time, Theoretical Computer Science, vol.3, pp.105-117, 1977. ,
New problems complete for nondeterministic log space, Mathematical systems theory, vol.10, issue.1, pp.1-17, 1976. ,
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
Resolution Strategies as Decision Procedures, Journal of the ACM, vol.23, issue.3, pp.398-417, 1976. ,
Tree Automata with Equality Constraints Modulo Equational Theories, Automated Reasoning (IJCAR'06), pp.557-571, 2006. ,
URL : https://hal.archives-ouvertes.fr/inria-00329693
Über die Erfüllbarkeit derjenigen Zählausdrücke, welche in der Normalform zwei benachbarte Allzeichen enthalten, Mathematische Annalen, vol.108, pp.466-484, 1933. ,
A new polynomial-time algorithm for linear programming, Combinatorica, vol.4, issue.4, pp.373-395, 1984. ,
Property-Directed Inference of Universal Invariants or Proving Their Absence, Shachar Itzhaky, Noam Rinetzky, and Sharon Shoham, pp.583-602, 1986. ,
Polynomial algorithms in linear programming, USSR Computational Mathematics and Mathematical Physics, vol.20, issue.1, pp.53-72, 1980. ,
Complexity and Expressivity of Uniform One-Dimensional Fragment with Equality, Mathematical Foundations of Computer Science (MFCS'14), pp.365-376, 2014. ,
Henkin Quantifiers, Quantifiers: Logics, Models and Computation, pp.193-263, 1995. ,
Inst-Gen -A Modular Approach to Instantiation-Based Automated Reasoning, Programming Logics -Essays in Memory of Harald Ganzinger, pp.239-270, 2013. ,
Non-cyclic Sorts for First-Order Satisfiability, Frontiers of Combining Systems (FroCoS'13), vol.8152, pp.214-228, 2013. ,
New Concepts for Real Quantifier Elimination by Virtual Substitution, 2016. ,
Two-variable logics with counting and semantic constraints, SIGLOG News, vol.5, issue.3, pp.22-43, 2018. ,
Building a Calculus of Data Structures, Verification, Model Checking, and Abstract Interpretation (VMCAI'10), pp.26-44, 2010. ,
Extending Decidable Existential Rules by Joining Acyclicity and Guardedness, Artificial Intelligence (IJCAI'11), pp.963-968, 2011. ,
The Decision Problem for Segregated Formulas in First-Order Logic, Mathematica Scandinavica, vol.21, pp.233-240, 1967. ,
, Proceedings of the Workshop on Second-Order Quantifier Elimination and Related Topics (SOQE 2017), volume 2013 of CEUR Workshop Proceedings. CEUR-WS.org, 2017.
Superposition Modulo Theory, 2013. ,
iProver-Eq: An Instantiation-Based Theorem Prover with Equality, Automated Reasoning (IJCAR'10), pp.196-202, 2010. ,
Decision Procedures. Texts in Theoretical Computer Science, An EATCS Series, 2016. ,
A note on the relation between resolution and Maslov's inverse method, Machine Intelligence, vol.6, pp.73-76, 1971. ,
0-1 Laws and Decision Problems for Fragments of Second-Order Logic. Information and Computation, vol.87, pp.301-337, 1990. ,
First-Order Interpolation and Interpolating Proof Systems, Logic for Programming, Artificial Intelligence and Reasoning (LPAR'17), pp.49-64, 2017. ,
Superposition Decides the First-Order Logic Fragment Over Ground Theories, Mathematics in Computer Science, vol.6, issue.4, pp.427-456, 2012. ,
Deciding Clause Classes by Semantic Clash Resolution. Fundamenta Informaticae, vol.18, pp.163-182, 1993. ,
The Resolution Calculus. Texts in theoretical computer science, An EATCS Series, 1997. ,
Resolution and the Decision Problem, Logic and Foundations of Mathematics: Selected Contributed Papers of the Tenth International Congress of Logic, pp.249-269, 1995. ,
Universal Sequential Search Problems. Problemy peredachi informatsii, vol.9, pp.115-116, 1973. ,
Complexity of Solvable Cases of the Decision Problem for the Predicate Calculus, Foundations of Computer Science (FOCS'78), pp.35-47, 1978. ,
Unsolvable Classes of Quantificational Formulas, 1979. ,
Complexity Results for Classes of Quantificational Formulas, Journal of Computer and System Sciences, vol.21, issue.3, pp.317-353, 1980. ,
A Logic of Concrete Time Intervals (Extended Abstract), Logic in Computer Science (LICS'90), pp.380-389, 1990. ,
Elements of Finite Model Theory. Texts in Theoretical Computer Science, An EATCS Series, 2004. ,
Some Reduction Classes and Undecidable Theories, Studies in Constructive Mathematics and Mathematical Logic, vol.4, pp.24-25, 1969. ,
What Is the Inverse Method, Journal of Automated Reasoning, vol.5, issue.1, pp.1-23, 1989. ,
Efficiently Computable Datalog? Programs, Knowledge Representation and Reasoning (KR'12), 2012. ,
Decidability of the monadic predicate calculus with unary function symbols, Journal of Symbolic Logic, vol.32, p.563, 1967. ,
Dependency Schemes and Search-Based QBF Solving: Theory and Practice, 2012. ,
On the extending of models (I). Fundamenta mathematicae, vol.42, pp.38-54, 1955. ,
Über Möglichkeiten im Relativkalkül, Mathematische Annalen, vol.76, pp.447-470, 1915. ,
Applying Linear Quantifier Elimination, The Computer Journal, vol.36, issue.5, pp.450-462, 1993. ,
BDI: A New Decidable Firstorder Clause Class, Logic for Programming, Artificial Intelligence and Reasoning (LPAR-19), vol.26, pp.62-74, 2013. ,
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
An interpolation theorem in the predicate calculus, Pacific Journal of Mathematics, vol.9, issue.1, pp.129-142, 1959. ,
Sur la Vérification de la Satisfaction pour la Logique des Différences, 2003. ,
Tolerance Logic, Journal of Logic, Language and Information, vol.10, issue.3, pp.353-374, 2001. ,
An Inverse Method of Establishing Deducibilities in the Classical Predicate Calculus, Doklady Akademii Nauk SSSR, vol.159, pp.1420-1424, 1964. ,
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. ,
The Inherent Computational Complexity of Theories of Ordered Sets, Proceedings of the International Congress of Mathematicians, pp.477-482, 1974. ,
Computation: finite and infinite machines, 1967. ,
Eugene Asarin, and Oded Maler. A Satisfiability Checker for Difference Logic, Theory and Applications of Satisfiability Testing (SAT'02), pp.222-230, 2002. ,
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. ,
On Languages with Two Variables, Mathematical Logic Quarterly, vol.21, issue.1, pp.135-140, 1975. ,
Beiträge zur Theorie der Linearen Ungleichungen, 1936. ,
Binding Forms in First-Order Logic, Computer Science Logic (CSL'15), pp.648-665, 2015. ,
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
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. ,
Toward a More Complete Alloy, Abstract State Machines, Alloy, B, VDM, and Z (ABZ'12), pp.136-149, 2012. ,
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.
Normalizable Horn Clauses, Strongly Recognizable Relations, and Spi, Static Analysis (SAS'02), pp.20-35, 2002. ,
Simplification by Cooperating Decision Procedures, ACM Transactions on Programming Languages and Systems, vol.1, issue.2, pp.245-257, 1979. ,
DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference Logic, Computer Aided Verification (CAV'05), pp.321-334, 2005. ,
Predicate-functors and the limits of decidability in logic, Notre Dame Journal of Formal Logic, vol.21, issue.4, pp.701-707, 1980. ,
Computing Small Clause Normal Forms, Handbook of Automated Reasoning, vol.I, pp.335-367, 2001. ,
Classical Recursion Theory, Studies in Logic and the Foundations of Mathematics, vol.125, 1992. ,
, Complexity, Convexity and Combinations of Theories. Theoretical Computer Science, vol.12, pp.291-302, 1980.
Bounded Variable Logics and Counting: A Study in Finite Models, Lecture Notes in Logic, vol.9, 1997. ,
An interpolation theorem, Bulletin of Symbolic Logic, vol.6, issue.4, pp.447-462, 2000. ,
Some Recent Results in Metric Temporal Logic, Formal Modeling and Analysis of Timed Systems (FORMATS'08), pp.1-13, 2008. ,
Computational complexity, 1994. ,
Deciding Effectively Propositional Logic Using DPLL and Substitution Sets, Journal of Automated Reasoning, vol.44, issue.4, pp.401-424, 2010. ,
Complete Problems in the First-Order Predicate Calculus, Journal of Computer and System Sciences, vol.29, issue.1, pp.8-35, 1984. ,
Ivy: safety verification by interactive generalization, Programming Language Design and Implementation (PLDI'16), pp.614-630, 2016. ,
The Bernays-Schönfinkel-Ramsey class for set theory: decidability, Journal of Symbolic Logic, vol.77, pp.896-918, 2012. ,
Two Easy Theories Whose Combination is Hard, 1977. ,
Ü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. ,
Quine's Fluted Fragment is Non-Elementary, Computer Science Logic (CSL'16), vol.39, pp.1-39, 2016. ,
Decidability of Fluted Logic with Identity, Notre Dame Journal of Formal Logic, vol.37, issue.1, pp.84-104, 1996. ,
Fluted Formulas and the Limits of Decidability, Journal of Symbolic Logic, vol.61, issue.2, pp.608-620, 1996. ,
Quine's 'Limits of Decision', Journal of Symbolic Logic, vol.64, issue.4, pp.1439-1466, 1999. ,
Complexity and Nicety of Fluted Logic, Studia Logica, vol.71, issue.2, pp.177-198, 2002. ,
Decidability and Essential Undecidability, Journal of Symbolic Logic, vol.22, issue.1, pp.39-54, 1957. ,
Encodings of Bounded LTL Model Checking in Effectively Propositional Logic, Automated Deduction (CADE-21), pp.346-361, 2007. ,
Encodings of Problems in Effectively Propositional Logic, Theory and Applications of Satisfiability Testing (SAT'07), p.3, 2007. ,
Proof Systems for Effectively Propositional Logic, Automated Reasoning (IJCAR'08), pp.426-440, 2008. ,
Planning with Effectively Propositional Logic, Programming Logics -Essays in Memory of Harald Ganzinger, pp.302-316, 2013. ,
Revisiting reachability in timed automata, Logic in Computer Science (LICS'17), pp.1-12, 2017. ,
An extended version appeared in W, 14th International Congress of Philosophy, vol.III, pp.57-62, 1969. ,
The Ways of Paradox and other essays. Revised and enlarged edition, 1976. ,
Decidability of Second-Order Theories and Automata on Infinite Trees, Transactions of the American Mathematical Society, vol.141, pp.1-35, 1969. ,
The complexity of theories of the monadic predicate calculus, IRIA Report, vol.136, 1975. ,
On a Problem of Formal Logic, Proceedings of The London Mathematical Society, 1930. ,
, Jaakko Hintikka, pp.43-76, 1987.
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
On the complexity of quantified linear systems, Theoretical Computer Science, vol.518, pp.128-134, 2014. ,
Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic, Verification, Model Checking, and Abstract Interpretation (VMCAI'17), pp.462-482, 2017. ,
Induction for SMT Solvers, Verification, Model Checking, and Abstract Interpretation (VMCAI'15), pp.80-98, 2015. ,
Solving quantified linear arithmetic by counterexample-guided instantiation, Formal Methods in System Design, vol.51, issue.3, pp.500-532, 2017. ,
Definability and Decision Problems in Arithmetic, Journal of Symbolic Logic, vol.14, issue.2, pp.98-114, 1949. ,
This is a paperback reprint of the 1967 original with the same author, 1987. ,
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
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
Deconstructing Shostak, Logic in Computer Science (LICS'01), pp.19-28, 2001. ,
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
Finding conflicting instances of quantified formulas in SMT, Formal Methods in Computer-Aided Design (FMCAD'14), pp.195-202, 2014. ,
Handbook of Automated Reasoning. I & II, 2001. ,
Variable Dependencies of Quantified CSPs, Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'08), pp.512-527, 2008. ,
Relationships between nondeterministic and deterministic tape complexities, Journal of Computer and System Sciences, vol.4, issue.2, pp.177-192, 1970. ,
Formalizing Bachmair and Ganzinger's Ordered Resolution Prover, Automated Reasoning (IJCAR'18), pp.89-107, 2018. ,
On Semantic Generalizations of the Bernays-Schönfinkel-Ramsey Class with Finite or Co-finite Spectra, 2010. ,
Über die Erfüllbarkeit einer Klasse von logischen Formeln, vol.110, pp.161-194, 1934. ,
Untersuchungen zum Entscheidungsproblem der mathematischen Logik, Mathematische Annalen, vol.109, issue.4, pp.572-603, 1934. ,
Theory of linear and integer programming. Wiley-Interscience series in discrete mathematics and optimization, 1999. ,
, Logic for Computer Scientists, 2008.
, Complexity Hierarchies beyond Elementary. ACM Transactions on Computation Theory, vol.8, issue.1, pp.1-3, 2016.
A decision method for validity of sentences in two variables, Journal of Symbolic Logic, vol.27, p.477, 1962. ,
A survey on guarded negation, SIGLOG News, vol.4, issue.3, pp.12-26, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01589314
A Resolution Decision Procedure for Fluted Logic, Automated Deduction (CADE-17), pp.433-448, 2000. ,
The Monadic Theory of Order, Annals of Mathematics, vol.102, issue.3, pp.379-419, 1975. ,
Decidability of a portion of the predicate calculus, Israel Journal on Mathematics, vol.28, pp.32-44, 1977. ,
Deciding Combinations of Theories, Journal of the ACM, vol.31, issue.1, pp.1-12, 1984. ,
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.
YAGO: A Large Ontology from Wikipedia and WordNet, Journal of Web Semantics, vol.6, issue.3, pp.203-217, 2008. ,
Interpolation formulae for predicates and terms which carry their own history, Archive for Mathematical Logic, vol.17, issue.3-4, pp.159-169, 1975. ,
First-Order Logic, 1995. ,
Recursively Enumerable Sets and Degrees, 1987. ,
Turing Computability Theory and Applications. Theory and Applications of Computability, In cooperation with the association Computability in Europe, 2016. ,
On Combinations of Local Theory Extensions, Programming Logics -Essays in Memory of Harald Ganzinger, pp.392-413, 2013. ,
Hierarchical Reasoning in Local Theory Extensions and Applications, Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'14), pp.34-41, 2014. ,
Collapsing probabilistic hierarchies. I. Algebra and Logic, vol.52, pp.159-171, 2013. ,
A note on definability in fragments of arithmetic with free unary predicates. Archive for Mathematical Logic, vol.52, pp.507-516, 2013. ,
Combining Shostak Theories, Rewriting Techniques and Applications (RTA'02), pp.1-18, 2002. ,
Extending H 1 -clauses with disequalities, Information Processing Letters, vol.111, issue.20, pp.1007-1013, 2011. ,
Extending H 1 -Clauses with Path Disequalities, Foundations of Software Science and Computational Structures (FOSSACS'12), pp.165-179, 2012. ,
The state of CASC, AI Communications, vol.19, issue.1, pp.35-48, 2006. ,
Backdoor Sets of Quantified Boolean Formulas, Journal of Automated Reasoning, vol.42, issue.1, pp.77-97, 2009. ,
Deciding Separation Formulas with SAT, Computer Aided Verification (CAV'02), pp.209-222, 2002. ,
A General Tableau Method for Deciding Description Logics, Modal Logics and Related First-Order Fragments, Automated Reasoning (IJCAR'08), pp.194-209, 2008. ,
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.
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
Thirty Years of Virtual Substitution: Foundations, Techniques, Applications, Symbolic and Algebraic Computation (ISSAC'18), pp.11-16, 2018. ,
Reduktionstheorie des Entscheidungsproblems im Prädikatenkalkül der ersten Stufe. Verlag der Ungarischen Akademie der Wissenschaften, 1959. ,
, The 9th IJCAR Automated Theorem Proving System Competition -CASC-J9. AI Communications, vol.31, pp.495-507, 2018.
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. ,
Flat and one-variable clauses: Complexity of verifying cryptographic protocols with single blind copying, ACM Transactions on Computational Logic, vol.9, issue.4, 2008. ,
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
On the Saturation of YAGO, Automated Reasoning (IJCAR'10), pp.441-456, 2010. ,
The Method of Forced Enumeration for Nondeterministic Automata, Acta Informatica, vol.26, issue.3, pp.279-284, 1988. ,
Resolution methods for decision problems and finite-model building, 1991. ,
Using Resolution for Extending KL-ONE-type Languages, Information and Knowledge Management (CIKM'95), pp.326-332, 1995. ,
Contributions to the theory of models, vol.XVI, pp.572-581, 1954. ,
A Decision Method for Elementary Algebra and Geometry, 1948. ,
A Decision Method for Elementary Algebra and Geometry, Quantifier Elimination and Cylindrical Algebraic Decomposition, pp.24-84, 1998. ,
An Approximation and Refinement Approach to First-Order Automated Reasoning, 2017. ,
A New Correctness Proof of the Nelson-Oppen Combination Procedure, Frontiers of Combining Systems (FroCoS'96), pp.103-119, 1996. ,
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
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. ,
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
Basic Proof Theory, Cambridge Tracts in Theoretical Computer Science, vol.43, 1996. ,
Range Allocation for Separation Logic, Computer Aided Verification (CAV'04), pp.148-161, 2004. ,
On Computable Numbers, with an Application to the Entscheidungsproblem, Proceedings of the, pp.230-265, 1936. ,
On Computable Numbers, with an Application to the Entscheidungsproblem. A Correction, Proceedings of the, pp.544-546, 1938. ,
First-Order Logic Theorem Proving and Model Building via Approximation and Instantiation, Frontiers of Combining Systems (FroCoS'15), pp.85-100, 2015. ,
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
Combining Nonstably Infinite Theories, Journal of Automated Reasoning, vol.34, issue.3, pp.209-238, 2005. ,
Dependence Logic -A New Approach to Independence Friendly Logic, vol.70, 2007. ,
Dynamic bits and pieces, 1997. ,
Logic and Structure, 2013. ,
Computational Complexity of Basic Decision Problems of Finite Tree Automata, 1997. ,
On Simultaneous Rigid E-Unification, 1997. ,
From Frege to Gödel -A Source Book in Mathematical Logic, pp.1879-1931, 2002. ,
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. ,
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
On Generalizing Decidable Standard Prefix Classes of First-Order Logic, ArXiv preprint, 2017. ,
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. ,
Bernays-Schönfinkel-Ramsey with Simple Bounds is NEXPTIME-complete, 2015. ,
The Complexity of Linear Problems in Fields, Journal of Symbolic Computation, vol.5, issue.1/2, pp.3-27, 1988. ,
Quantifier Elimination for Real Algebra -the Quadratic Case and Beyond. Applicable Algebra in Engineering, vol.8, pp.85-101, 1997. ,
Automated Deduction -A Basis for Applications, Applied Logic Series, vol.I, pp.291-320, 1998. ,
Towards an Automatic Analysis of Security Protocols in First-Order Logic, Automated Deduction (CADE-16), vol.1632, pp.314-328 ,
, , 1999.
Heinrich Behmann's Contributions to Second-Order Quantifier Elimination from the View of Computational Logic, 2015. ,
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. ,
Predicate Learning and Selective Theory Deduction for a Difference Logic Solver, Design Automation Conference (DAC'06), pp.235-240, 2006. ,
Fourier's Method of Linear Programming and Its Dual, The American Mathematical Monthly, vol.93, issue.9, pp.681-695, 1986. ,
Das Entscheidungsproblem der Prädikatenlogik 1. Stufe mit Identität und Funktionszeichen in Herbrandformeln, 1976. ,
Das Entscheidungsproblem der Klasse von Formeln, die höchstens zwei Primformeln enthalten, Manuscripta Mathematica, vol.22, pp.13-25, 1977. ,
Kleine unentscheidbare Klassen der Prädikatenlogik mit Identität und Funktionszeichen. Archiv für mathematische Logik und Grundlagenforschung, vol.19, pp.97-109, 1978. ,
Efficient Reasoning Procedures for Complex First-Order Theories, 2012. ,
Combining Theories with Shared Set Operations, Frontiers of Combining Systems (FroCoS'09), vol.5749, pp.366-382, 2009. ,
On a Connection Between the Resolution Method and the Inverse Method, Fundamentals of Computation Theory (FCT'87), pp.501-505, 1987. ,