Logic Programming with Focusing Proofs in Linear Logic, Journal of Logic and Computation, vol.2, issue.3, pp.297-347, 1992. ,
DOI : 10.1093/logcom/2.3.297
Rewrite-based Equational Theorem Proving with Selection and Simplification, Journal of Logic and Computation, vol.4, issue.3, pp.1-31, 1994. ,
DOI : 10.1093/logcom/4.3.217
Resolution Theorem Proving, pp.19-99, 2001. ,
DOI : 10.1016/B978-044450813-3/50004-7
A Semantic Completeness Proof for TaMeD, pp.167-181, 2006. ,
DOI : 10.1007/11916277_12
URL : https://hal.archives-ouvertes.fr/hal-01337086
Principles of Superdeduction, 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007), pp.41-50, 2007. ,
DOI : 10.1109/LICS.2007.37
URL : https://hal.archives-ouvertes.fr/inria-00133557
Embedding Deduction Modulo into a Prover, pp.155-169, 2010. ,
DOI : 10.1007/978-3-642-15205-4_15
URL : http://www.ensiie.fr/~guillaume.burel/download/burel10embedding.pdf
Experimenting with Deduction Modulo, pp.162-176, 2011. ,
DOI : 10.1007/978-3-642-02959-2_10
URL : https://hal.archives-ouvertes.fr/hal-01125858
From Axioms to Rewriting Rules Available on author's web page, 2013. ,
Cut Admissibility by Saturation, pp.124-138, 2014. ,
DOI : 10.1007/978-3-319-08918-8_9
URL : https://hal.archives-ouvertes.fr/hal-01097428
How can we prove that a proof search method is not an instance of another?, Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages Theory and Practice, LFMTP '09, 2009. ,
DOI : 10.1145/1577824.1577838
Regaining cut admissibility in deduction modulo using abstract completion, Information and Computation, vol.208, issue.2, pp.140-164, 2010. ,
DOI : 10.1016/j.ic.2009.10.005
URL : https://hal.archives-ouvertes.fr/inria-00132964
Handbook of proof theory, 1998. ,
A Focusing Inverse Method Theorem Prover for First-Order Linear Logic, pp.69-83, 2005. ,
DOI : 10.1007/11532231_6
URL : http://www.cs.cmu.edu/afs/cs/user/fp/www/papers/cade05.ps
A Logical Characterization of Forward and Backward Chaining in the Inverse Method, Journal of Automated Reasoning, vol.40, pp.2-3, 2008. ,
The Proof Certifier Checkers, TABLEAUX (LNCS), pp.201-210, 2015. ,
DOI : 10.1007/978-3-642-45221-5_49
URL : https://hal.archives-ouvertes.fr/hal-01208333
Foundational Proof Certificates in First-Order Logic, pp.162-177, 2013. ,
DOI : 10.1007/978-3-642-38574-2_11
URL : https://hal.archives-ouvertes.fr/hal-00906485
Induction as Deduction Modulo Rapport de recherche. LORIA. http://www.loria.fr/ publications, 2004. ,
What Is a Theory?, pp.50-64, 2002. ,
DOI : 10.1007/3-540-45841-7_3
Truth Values Algebras and Proof Normalization, pp.110-124, 2006. ,
DOI : 10.1007/978-3-540-74464-1_8
Polarized Resolution Modulo, pp.182-196, 2010. ,
DOI : 10.1007/978-3-642-15240-5_14
URL : https://hal.archives-ouvertes.fr/hal-01054460
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/inria-00077199
Abstract, The Journal of Symbolic Logic, vol.87, issue.04, pp.1289-1316, 2003. ,
DOI : 10.1007/BFb0037116
Arithmetic as a Theory Modulo, pp.423-437, 2005. ,
DOI : 10.1007/978-3-540-32033-3_31
URL : http://pauillac.inria.fr/~werner/publis/rta05.pdf
) and a proof-search strategy for the focused sequent calculus, Proceedings of the Eighth ACM SIGPLAN international workshop on Logical frameworks & meta-languages: theory & practice, LFMTP '13, pp.3-14, 2013. ,
DOI : 10.1145/2503887.2503892
A Note on the Completeness of Certain Refinements of Resolution, 2002. ,
Méthodes Sémantiques en Déduction Modulo, 2005. ,
Axiom Directed Focusing, Types for Proofs and Programs, pp.169-185, 2008. ,
DOI : 10.1016/S0168-0072(00)00032-4
URL : https://hal.archives-ouvertes.fr/inria-00212059
Focusing and polarization in linear, intuitionistic, and classical logics, Theoretical Computer Science, vol.410, issue.46, pp.4747-4768, 2009. ,
DOI : 10.1016/j.tcs.2009.07.041
URL : https://doi.org/10.1016/j.tcs.2009.07.041
Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional Logic, LPAR (Lecture Notes in Computer Science), Iliano Cervesato, pp.174-181, 2008. ,
DOI : 10.1007/978-3-540-89439-1_12
Focused Labeled Proof Systems for Modal Logic, LPAR (LNCS), pp.266-280, 2015. ,
DOI : 10.1007/978-3-662-48899-7_19
URL : https://hal.archives-ouvertes.fr/hal-01213858
Automatic Deduction with Hyper-Resolution, International Journal of Computer Mathematics, vol.1, pp.227-234, 1965. ,
DOI : 10.1007/978-3-642-81952-0_27
Cut-elimination in logics with definitional reflection, Nonclassical Logics and Information Processing, pp.146-171, 1990. ,
DOI : 10.1007/BFb0031929
Automatic Theorem Proving With Renamable and Semantic Resolution, Journal of the ACM, vol.14, issue.4, pp.687-697, 1967. ,
DOI : 10.1145/321420.321428
Efficiency and Completeness of the Set of Support Strategy in Theorem Proving, Journal of the ACM, vol.12, issue.4, pp.536-541, 1965. ,
DOI : 10.1145/321296.321302