Logic Programming with Focusing Proofs in Linear Logic, J. of Logic and Computation, vol.2, pp.297-347, 1992. ,
Theorem Proving via General Matings, J. ACM, vol.28, pp.193-214, 1981. ,
Eliminating Definitions and Skolem Functions in First-Order Logic, ACM Transactions on Computational Logic, vol.4, pp.402-415, 2003. ,
On the complexity of proof deskolemization, J. of Symbolic Logic, vol.77, pp.669-686, 2012. ,
On Skolemization and Proof Complexity, Fundamenta Informaticae, vol.20, pp.353-379, 1994. ,
Scalable Fine-Grained Proofs for Formula Processing, 26th International Conference on Automated Deduction (CADE) (LNCS), vol.10395, pp.398-412, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01526841
Translating Between Implicit and Explicit Versions of Proof, Automated Deduction -CADE 26 -26th International Conference on Automated Deduction, vol.10395, pp.255-273, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01645016
A Multi-Focused Proof System Isomorphic to Expansion Proofs, J. of Logic and Computation, vol.26, pp.577-603, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-00937056
The proof certifier Checkers, Proceedings of the 24th Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX) (LNCS), pp.201-210, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01208333
Proof Certificates for Equality Reasoning, Post-proceedings of LSFA 2015: 10th Workshop on Logical and Semantic Frameworks, pp.93-108, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01390919
Checking Foundational Proof Certificates for First-Order Logic (extended abstract), Third International Workshop on Proof Exchange for Theorem Proving, vol.14, pp.58-66, 2013. ,
A semantic framework for proof evidence, J. of Automated Reasoning, vol.59, pp.287-330, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01390912
A Formulation of the Simple Theory of Types, J. of Symbolic Logic, vol.5, pp.56-68, 1940. ,
Extraction of Proofs from the Clausal Normal Form Transformation, CSL: 16th Workshop on Computer Science Logic, vol.2471, pp.584-598, 2002. ,
Translation of resolution proofs into short firstorder proofs without choice axioms, Information and Computation, vol.199, pp.24-54, 2005. ,
ELPI: Fast, Embeddable, ?Prolog Interpreter, Logic for Programming, Artificial Intelligence, and Reasoning -20th International Conference, vol.9450, pp.460-468, 2015. ,
System Description: GAPT 2.0, Proceedings of the 8th International Joint Conference on Automated Reasoning, IJCAR 2016 (LNCS), vol.9706, pp.293-301, 2016. ,
No Choice: Reconstruction of First-order ATP Proofs without Skolem Functions, Proceedings of the 5th Workshop on Practical Aspects of Automated Reasoning (PAAR) (CEUR Workshop Proceedings, vol.1635, pp.24-31, 2016. ,
Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants, TACAS: Tools and Algorithms for the Construction and Analysis of Systems, vol.3920, pp.167-181, 2006. ,
URL : https://hal.archives-ouvertes.fr/inria-00001088
Investigations into Logical Deduction, The Collected Papers of Gerhard, pp.68-131, 1935. ,
A new constructive logic: classical logic, Math. Structures in Comp. Science, vol.1, pp.255-296, 1991. ,
URL : https://hal.archives-ouvertes.fr/inria-00075117
A BDD-Based Simplification and Skolemization Procedure, Logic Journal of the IGPL, vol.3, pp.827-855, 1995. ,
Proof mining in L 1 -approximation, Annals of Pure and Applied Logic, vol.121, pp.1-38, 2003. ,
Focusing and Polarization in Linear, Intuitionistic, and Classical Logics, Theoretical Computer Science, vol.410, pp.4747-4768, 2009. ,
Proofs in Higher-order Logic, Ph.D. Dissertation. Carnegie-Mellon University, 1983. ,
A Compact Representation of Proofs, Studia Logica, vol.46, pp.347-370, 1987. ,
Abstractions in logic programming, Logic and Computer Science, Piergiorgio Odifreddi, pp.329-359, 1990. ,
Unification of Simply Typed Lambda-Terms as Logic Programming, Eighth International Logic Programming Conference, pp.255-269, 1991. ,
Programming with Higher-Order Logic, 2012. ,
URL : https://hal.archives-ouvertes.fr/hal-00776197
System Description: Teyjus -A Compiler and Abstract Machine Based Implementation of ?Prolog, 16th Conf. on Automated Deduction (CADE) (LNAI), pp.287-291, 1999. ,
Computing Small Clause Normal Forms, Handbook of Automated Reasoning, 2001. ,
, I. Elsevier Science B.V., Chapter, vol.6, pp.335-367
Checkable Proofs for First-Order Theorem Proving, ARCADE 2017, 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements (EPiC Series in Computing), vol.51, pp.55-63, 2017. ,
Mathematical Logic, 1967. ,
SMT proof checking using a logical framework, Formal Methods in System Design, vol.42, pp.91-118, 2013. ,
Elpi: an extension language for Coq, The Fourth International Workshop on Coq for Programming Languages, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01637063