M. Baaz and C. G. Fermüller, Non-elementary speedups between different versions of tableaux, TABLEAUX'95, pp.217-230, 1995.
DOI : 10.1007/3-540-59338-1_38

B. Beckert, R. Hähnle, and P. H. Schmitt, The Even More Liberalized delta-Rule in Free Variable Semantic Tableaux, Proceedings of the Third Kurt Gödel Colloquium on Computational Logic and Proof Theory, pp.108-119, 1993.

E. W. Beth, Semantic entailment and formal derivability. Mededelingen van de Koninklijke Nederlandse Akademie van Wetenschappen, Afdeling Letterkunde, vol.18, issue.13, pp.309-351, 1955.

M. Boespflug, Q. Carbonneaux, and O. Hermant, The ??-calculus modulo as a universal proof language, ceur-ws. org, pp.28-43, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00917845

R. Bonichon, D. Delahaye, and D. Doligez, Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs, LNCS, vol.4790, pp.151-165, 2007.
DOI : 10.1007/978-3-540-75560-9_13
URL : https://hal.archives-ouvertes.fr/inria-00315920

D. Cantone and M. Nicolosi-asmundo, A Further and Effective Liberalization of the delta-Rule in Free Variable Semantic Tableaux In: Selected Papers from Automated Deduction in Classical and Non-Classical Logics, pp.109-125, 2000.

D. Cantone and M. Nicolosi-asmundo, A Sound Framework for delta-Rule Variants in Free-Variable Semantic Tableaux, J. Autom. Reasoning, vol.38, pp.1-3, 2007.

G. Dowek, Polarized Resolution Modulo, TCS. IFIP, vol.323, pp.182-196, 2010.
DOI : 10.1007/978-3-642-15240-5_14
URL : https://hal.archives-ouvertes.fr/hal-01054460

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

C. Dubois, T. Hardin, and V. Donzeau-gouge, Building certified components within focal, Trends in Functional Programming. Trends in Functional Programming, pp.33-48, 2004.
URL : https://hal.archives-ouvertes.fr/hal-01124970

M. Fitting, First Order Logic and Automated Theorem Proving, 1996.

M. Giese and W. Ahrendt, Hilbert???s ???-Terms in Automated Theorem Proving, TABLEAUX'99, pp.171-185, 1999.
DOI : 10.1007/3-540-48754-9_17

R. Hähnle and P. Schmitt, The liberalized ?-rule in free variable semantic tableaux, Journal of Automated Reasoning, vol.4, issue.2, pp.211-221, 1994.
DOI : 10.1007/BF00881956

A. Nonnengart and C. Weidenbach, Computing Small Clause Normal Forms, Handbook of Automated Reasonning, pp.336-367, 2001.
DOI : 10.1016/B978-044450813-3/50008-4
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.42.222

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

R. Smullyan, First-Order Logic, 1968.
DOI : 10.1201/b10689-23

A. Waaler and R. Antonsen, A Free Variable Sequent Calculus with Uniform Variable Splitting, TABLEAUX'03, pp.214-229, 2003.
DOI : 10.1007/978-3-540-45206-5_17