H. Amjad, Combining Model Checking and Theorem Proving, 2004.

M. Ben-ari, A. Pnueli, and Z. Manna, The temporal logic of branching time, Acta Informatica, vol.20, issue.4, pp.207-226, 1983.
DOI : 10.1007/BF01257083

A. Biere, A. Cimatti, E. Clarke, and Y. Zhu, Symbolic Model Checking without BDDs, Lecture Notes in Computer Science, vol.1579, pp.193-207, 1999.
DOI : 10.1007/3-540-49059-0_14

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.42.8033

R. Jerry, E. M. Burch, . Clarke, L. Kenneth, . Mcmillan et al., Symbolic Model Checking: 10 20 States and Bbeyond, Logic in Computer Science LICS'90, Proceedings., Fifth Annual IEEE Symposium on e, pp.428-439, 1990.

A. Bouajjani, J. Esparza, and O. Maler, Reachability analysis of pushdown automata: Application to model-checking, CONCUR'97: Concurrency Theory, pp.135-150, 1997.
DOI : 10.1007/3-540-63141-0_10

. Britton, The Wolf, the Goat and the Cabbage, 2013.

R. E. Bryant, Graph-Based Algorithms for Boolean Function Manipulation, IEEE Transactions on Computers, vol.35, issue.8, pp.677-691, 1986.
DOI : 10.1109/TC.1986.1676819

B. Beckert and S. Schlager, A Sequent Calculus for First-Order Dynamic Logic with Trace Modalities, Proceedings, International Joint Conference on Automated Reasoning, pp.626-641, 2001.
DOI : 10.1007/3-540-45744-5_51

G. Burel, Embedding Deduction Modulo into a Prover, CSL 2010, pp.155-169, 2010.
DOI : 10.1007/978-3-642-15205-4_15

G. Burel, Experimenting with Deduction Modulo, Nikolaj Bjørner and Viorica Sofronie-Stokkermans, pp.162-176, 2011.
DOI : 10.1007/978-3-642-02959-2_10

URL : https://hal.archives-ouvertes.fr/hal-01125858

[. Clarke, A. Biere, R. Raimi, and Y. Zhu, Bounded Model Checking Using Satisfiability Solving, Formal Methods in System Design, vol.19, issue.1, pp.7-34, 2001.
DOI : 10.1023/A:1011276507260

A. Cimatti, E. M. Clarke, F. Giunchiglia, and M. Roveri, NuSMV: A New Symbolic Model Verifier, Proceedings of the 11th International Conference on Computer Aided Verification, CAV '99, pp.495-499, 1999.
DOI : 10.1007/3-540-48683-6_44

B. Courcelle and J. Engelfriet, Graph Structure and Monadic Secondorder Logic: a Language-Theoretic Approach, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00646514

E. M. Clarke and J. , Orna Grumberg, and Doron A. Peled. Model Checking, 1999.

C. Chang and R. Lee, Symbolic Logic and Mechanical Theorem Proving, 1997.

B. Courcelle, The Monadic Second-order Logic of Graphs. I. Recognizable Sets of Finite Graphs. Information and computation, pp.12-75, 1990.
URL : https://hal.archives-ouvertes.fr/hal-00353765

D. David-delahaye, F. Doligez, P. Gilbert, O. Halmagrand, and . Hermant, Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo, LNCS, vol.8312, issue.19, pp.274-290, 2013.
DOI : 10.1007/978-3-642-45221-5_20

G. Dowek, T. Hardin, and C. Kirchner, Theorem Proving Modulo, Journal of Automated Reasoning, vol.31, issue.1, pp.33-72, 2003.
DOI : 10.1023/A:1027357912519

URL : https://hal.archives-ouvertes.fr/hal-01199506

G. Dowek and Y. Jiang, A Logical Approach to CTL. manuscript, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00919467

G. Dowek and Y. Jiang, Axiomatizing Truth in a Finite Model, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00919469

G. Dowek and Y. Jiang, Pushdown Systems in Polarized Deduction Modulo. manuscript, 2015.

G. Dowek, What Is a Theory?, STACS 2002, pp.50-64, 2002.
DOI : 10.1007/3-540-45841-7_3

G. Dowek, Polarized Resolution Modulo, TCS 2010, pp.182-196, 2010.
DOI : 10.1007/978-3-642-15240-5_14

URL : https://hal.archives-ouvertes.fr/hal-01054460

G. Dowek, Proofs and Algorithms: An Introduction to Logic and Computability, 2011.
DOI : 10.1007/978-0-85729-121-9

E. , A. Emerson, and E. M. Clarke, Characterizing Correctness Properties of Parallel Programs Using Fixpoints, Automata, Languages and Programming, pp.169-181, 1980.

[. Emerson and J. Y. Halpern, ???Sometimes??? and ???not never??? revisited: on branching versus linear time temporal logic, Journal of the ACM, vol.33, issue.1, pp.151-178, 1986.
DOI : 10.1145/4904.4999

J. Esparza, D. Hansel, P. Rossmanith, and S. Schwoon, Efficient Algorithms for Model Checking Pushdown Systems, Computer Aided Verification, pp.232-247, 2000.
DOI : 10.1007/10722167_20

E. and A. Emerson, Temporal and Modal Logic, In HANDBOOK OF THE- ORETICAL COMPUTER SCIENCE, pp.995-1072, 1995.
DOI : 10.1016/B978-0-444-88074-1.50021-4

N. Eén and N. Sörensson, An Extensible SAT-solver, Theory and Applications of Satisfiability Testing, pp.502-518, 2004.
DOI : 10.1007/978-3-540-24605-3_37

M. Fisher, A Resolution Method for Temporal Logic, IJCAI, pp.99-104, 1991.

H. Ganzinger and K. Korovin, Theory Instantiation, Logic for Programming, Artificial Intelligence, and Reasoning, pp.497-511, 2006.
DOI : 10.1007/11916277_34

J. Goubault-larrecq and J. Goubault-larrecq, A Note on the Completeness of Certain Refinements of Resolution, 2002.

R. Goré, And-Or Tableaux for Fixpoint Logics with Converse: LTL, CTL, PDL and CPDL, Automated Reasoning, pp.26-45, 2014.
DOI : 10.1007/978-3-319-08587-6_3

[. G. S83-]-g and . Tseitin, On the Complexity of Derivation in Propositional Calculus, Automation of Reasoning , Symbolic Computation, pp.466-483, 1983.

G. Edward, H. , and M. J. , An Introduction to Modal Logic, 1968.

M. Herle, M. Järvisalo, and A. Biere, Clause Elimination Procedures for CNF Formulas, LNCS, vol.6397, pp.17-357, 2010.

[. Ji, CTL Model Checking in Deduction Modulo, Automated Deduction -CADE-25, pp.295-310, 2015.
DOI : 10.1007/978-3-319-21401-6_20

URL : https://hal.archives-ouvertes.fr/hal-01241132

K. Ji, Resolution in Solving Graph Problems. manuscript, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01245138

K. Korovin, iProver ??? An Instantiation-Based Theorem Prover for First-Order Logic (System Description), LNCS, vol.5195, pp.292-298, 2008.
DOI : 10.1007/978-3-540-71070-7_24

D. Kozen, Results on the propositional ??-calculus, Automata, Languages and Programming, pp.348-359
DOI : 10.1007/BFb0012782

D. Kühlwein, S. Schulz, and J. Urban, E-MaLeS 1.1, Lecture Notes in Computer Science, vol.7898, pp.407-413, 2013.
DOI : 10.1007/978-3-642-38574-2_28

L. Kovács and A. Voronkov, First-Order Theorem Proving and Vampire, Computer Aided Verification, pp.1-35, 2013.
DOI : 10.1007/978-3-642-39799-8_1

L. Kenneth and . Mcmillan, Symbolic Model Checking, 1993.

L. Ken and . Mcmillan, Applying SAT Methods in Unbounded Symbolic Model Checking, Computer Aided Verification, pp.250-264, 2002.

G. L. Peterson, Myths about the mutual exclusion problem, Information Processing Letters, vol.12, issue.3, pp.115-116, 1981.
DOI : 10.1016/0020-0190(81)90106-X

A. Pnueli, The temporal logic of programs, 18th Annual Symposium on Foundations of Computer Science (sfcs 1977), pp.46-57, 1977.
DOI : 10.1109/SFCS.1977.32

[. Penczek, B. Wozna, and A. Zbrzezny, Bounded Model Checking for the Universal Fragment of CTL, Fundam. Inf, vol.51, pp.135-156, 2002.

J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM, vol.12, issue.1, pp.23-41, 1965.
DOI : 10.1145/321250.321253

J. A. Robinson, Automatic Deduction with Hyper-Resolution, Intl. J. Computer Mathematics, vol.1, issue.3, pp.227-234, 1965.
DOI : 10.1007/978-3-642-81952-0_27

N. [. Rajan, M. K. Shankar, and . Srivas, An integration of model checking with automated proof checking, Computer-Aided Verification, CAV '95, pp.84-97, 1995.
DOI : 10.1007/3-540-60045-0_42

[. Sassone, M. Nielsen, and G. Winskel, Models for concurrency: towards a classification, Theoretical Computer Science, vol.170, issue.1-2, pp.297-348, 1996.
DOI : 10.1016/S0304-3975(96)80710-9

]. G. Sut09 and . Sutcliffe, The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts, v3.5.0, Journal of Automated Reasoning, vol.43, issue.4, pp.337-362, 2009.

A. S. Troelstra and H. Schwichtenberg, Basic Proof Theory, 1996.
DOI : 10.1017/CBO9781139168717

M. Zohar and P. Amir, Temporal Verification of Reactive Systems? Safety, 1995.

W. Zhang, Bounded Semantics of CTL and SAT-Based Verification, ICFEM 2009, pp.286-305, 2009.
DOI : 10.1007/978-3-642-10373-5_15

W. Zhang, VERDS Modeling Language, 2012.

W. Zhang, Ternary Boolean Diagrams and Their Application to Model Checking. manuscript, 2013.

W. Zhang, QBF Encoding of Temporal Properties and QBF-Based Verification, IJCAR 2014, pp.224-239, 2014.
DOI : 10.1007/978-3-319-08587-6_16

L. Zhang, U. Hustadt, and C. Dixon, A resolution calculus for the branching-time temporal logic CTL, ACM Transactions on Computational Logic, vol.15, issue.1, p.10, 2014.
DOI : 10.1145/2529993