, Exemple, vol.176, pp.197-198

, ¬p(x) ? q(x) ? r(x, f (x)

, q(a) ? r (f (a)) res(2, 4) avec

, 14. ¬r (f (a)) res(7, 13) avec

, On note ?? la formule close ? x? où x est une suite des variables libres dans ?, Correction et complétude Notation, vol.177

. Le-modèle-m-est-bien and . Défini,

, On démontre le lemme 133 par induction sur ?

.. Soit-x-1, x n les variables libres de ? et soit t 1 ,. .. t n des termes clos. On a : M

, P, p.1

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

M. Ben-ari, Mathematical logic for computer science, 2012.

G. Boolos and R. C. Jeffrey, Computability and logic, 1987.

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

F. Baader and T. Nipkow, Term rewriting and all that, 1998.

M. Ben-or, D. Kozen, and J. Reif, The complexity of elementary algebra and geometry, Journal of Computer and System Sciences, vol.32, issue.2, pp.251-264, 1986.

R. Samuel and . Buss, The boolean formula value problem is in ALOGTIME, Proceedings of the 19th Annual ACM Symposium on Theory of Computing, pp.123-131, 1987.

B. Bollig and I. Wegener, Improving the variable ordering of obdds is np-complete, IEEE Trans. Computers, vol.45, issue.9, pp.993-1002, 1996.

J. Canny, Some algebraic and geometric computations in pspace, Proceedings of the twentieth annual ACM symposium on Theory of computing, pp.460-467, 1988.

O. Carton, Langages formels, calculabilité et complexité, vol.101, 2008.

R. Cori and D. Lascar, Logique mathématique ii. fonctions récursives, théorème de gödel, théorie des ensembles, théorie des modèles, 1993.

D. Lascar and C. , Logique mathématique, tome 1 : Calcul propositionnel, algèbre de boole, calcul des prédicats, coll. Sciences Sup, 2003.

S. Devismes, P. Lafourcade, and M. Lévy, Logique et démonstration automatique : introduction à la logique propositionnelle et à la logique du premier ordre, 2012.

R. David, K. Nour, C. Raffalli, and P. Curien, Introduction à la logique : théorie de la démonstration : cours et exercices corrigés. Dunod, 2001.

S. Dasgupta, C. H. Papadimitriou, and U. Vazirani, Algorithms, 2016.

J. Duparc, La logique pas à pas. PPUR Presses polytechniques, 2015.

S. Even, A. Itai, and A. Shamir, On the complexity of time table and multicommodity flow problems, Foundations of Computer Science, 1975., 16th Annual Symposium on, pp.184-193, 1975.

M. Fischer, J. Michael, . Fischer, and . Michael-o-rabin, Super-exponential complexity of presburger arithmetic, 1974.

J. Goubault, -. , and I. Mackie, Proof theory and automated deduction, vol.6, 2001.

J. Harrison, Handbook of practical logic and automated reasoning, 2009.

D. Kroening and O. Strichman, Decision procedures : an algorithmic point of view, 2008.

, René Lalement. Logique, réduction, résolution, 1990.

R. Lassaigne and M. De-rougemont, Logique et fondements de l'informatique, Hermes, 1993.

R. Legendre and F. Schwarzentruber, Compilation : Analyse lexicale et syntaxique du texte à sa structure en informatique, Reference Sciences. Ellipses, 2015.

V. Ju and . Matijasevi?, Enumerable sets are diophantine, Mathematical Logic In The 20th Century, pp.269-273, 2003.

. Derek-c-oppen, A 2 22pn upper bound on the complexity of presburger arithmetic, Journal of Computer and System Sciences, vol.16, issue.3, pp.323-332, 1978.

J. E. Savage, Models of computation-exploring the power of computing, 1998.

M. Sipser, Introduction to the theory of computation, 1997.

M. Sipser, Introduction to the Theory of Computation, Thomson Course Technology, vol.27, 2006.

J. Larry, A. Stockmeyer, and . Meyer, Word problems requiring exponential time (preliminary report), Proceedings of the fifth annual ACM symposium on Theory of computing, pp.1-9, 1973.

S. Tani, K. Hamaguchi, and S. Yajima, The complexity of the optimal variable ordering problems of shared binary decision diagrams, Algorithms and Computation, 4th International Symposium, ISAAC '93, pp.389-398, 1993.

. John-k-truss, Foundations of mathematical analysis, 1997.