2020
Article dans une revue
- titre
- Linking focusing and resolution with selection
- auteur
- Guillaume Burel
- article
- ACM Transactions on Computational Logic, 2020, 21 (3), pp.1-30. ⟨10.1145/3373276⟩
- Accès au texte intégral et bibtex
-
2019
Article dans une revue
- titre
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- auteur
- Guillaume Burel, Guillaume Bury, Raphaël Cauderlier, David Delahaye, Pierre Halmagrand, Olivier Hermant
- article
- Journal of Automated Reasoning, 2019, 64 (6), pp.1001-1050. ⟨10.1007/s10817-019-09533-z⟩
- Accès au texte intégral et bibtex
-
Communication dans un congrès
- titre
- Ekstrakto A tool to reconstruct Dedukti proofs from TSTP files (extended abstract)
- auteur
- Mohamed Yacine El Haddad, Guillaume Burel, Frédéric Blanqui
- article
- PxTP 2019 - Sixth Workshop on Proof eXchange for Theorem Proving (PxTP), Aug 2019, Natal, Brazil. pp.27-35, ⟨10.4204/EPTCS.301.5⟩
- Accès au texte intégral et bibtex
-
- titre
- Teaching formal methods to future engineers
- auteur
- Catherine Dubois, Virgile Prévosto, Guillaume Burel
- article
- Third International Workshop and Tutorial, FMTea, Sep 2019, Porto, Portugal. pp.69-80, ⟨10.1007/978-3-030-32441-4_5⟩
- Accès au texte intégral et bibtex
-
2018
Communication dans un congrès
- titre
- Linking focusing and resolution with selection
- auteur
- Guillaume Burel
- article
- 43rd International Symposium on Mathematical Foundations of Computer Science(MFCS), Aug 2018, Liverpool, United Kingdom. pp.9:1-9:14, ⟨10.4230/LIPIcs.MFCS.2018.9⟩
- Accès au texte intégral et bibtex
-
2016
Communication dans un congrès
- titre
- Expressing theories in the λΠ-calculus modulo theory and in the Dedukti system
- auteur
- Ali Assaf, Guillaume Burel, Raphal Cauderlier, David Delahaye, Gilles Dowek, Catherine Dubois, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant, Ronan Saillard
- article
- TYPES: Types for Proofs and Programs, May 2016, Novi SAd, Serbia
- Accès au texte intégral et bibtex
-
Pré-publication, Document de travail
- titre
- Automata, Resolution, and Cut-elimination
- auteur
- Guillaume Burel, Gilles Dowek, Ying Jiang
- article
- 2016
- Accès au texte intégral et bibtex
-
- titre
- Dedukti: a Logical Framework based on the λΠ-Calculus Modulo Theory
- auteur
- Ali Assaf, Guillaume Burel, Raphaël Cauderlier, David Delahaye, Gilles Dowek, Catherine Dubois, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant, Ronan Saillard
- article
- 2016
- Accès au texte intégral et bibtex
-
2015
Communication dans un congrès
- titre
- A Completion Method to Decide Reachability in Rewrite Systems
- auteur
- Guillaume Burel, Gilles Dowek, Ying Jiang
- article
- International Symposium on Frontiers of Combining Systems FroCoS'15, Sep 2015, Wroclaw, Poland. pp.205-219, ⟨10.1007/978-3-319-24246-0_13⟩
- Accès au texte intégral et bibtex
-
- titre
- Translating HOL to Dedukti
- auteur
- Ali Assaf, Guillaume Burel
- article
- Fourth Workshop on Proof eXchange for Theorem Proving, PxTP'15, Aug 2015, Berlin, Germany. pp.74-88, ⟨10.4204/EPTCS.186.8⟩
- Accès au texte intégral et bibtex
-
2014
Communication dans un congrès
- titre
- Cut Admissibility by Saturation
- auteur
- Guillaume Burel
- article
- Joint International Conference, RTA-TLCA 2014, Jul 2014, Vienna, Austria. pp.124-138, ⟨10.1007/978-3-319-08918-8_9⟩
- Accès au texte intégral et bibtex
-
2013
Communication dans un congrès
- titre
- A Shallow Embedding of Resolution and Superposition Proofs into the λΠ-Calculus Modulo
- auteur
- Guillaume Burel
- article
- PxTP - Third International Workshop on Proof Exchange for Theorem Proving - 2013, Jun 2013, Lake Placid, United States. pp.43-57
- Accès au texte intégral et bibtex
-
- titre
- Detection of First Order Axiomatic Theories
- auteur
- Guillaume Burel, Simon Cruanes
- article
- FroCoS - 9th International Symposium on Frontiers of Combining Systems - 2013, Sep 2013, Nancy, France. pp.229-244, ⟨10.1007/978-3-642-40885-4_16⟩
- Accès au texte intégral et bibtex
-
- titre
- A Shallow Embedding of Resolution and Superposition Proofs into the ??-Calculus Modulo
- auteur
- Guillaume Burel
- article
- Third International Workshop on Proof Exchange for Theorem Proving, Jun 2013, Lake Placid, United States
- Accès au bibtex
-
2012
Communication dans un congrès
- titre
- CoqInE : Translating the calculus of inductive constructions into the ??-calculus modulo.
- auteur
- Mathieu Boespflug, Guillaume Burel
- article
- Second International Workshop on Proof Exchange for Theorem Proving (PXTP 2012), Jun 2012, Manchester, United Kingdom
- Accès au bibtex
-
2011
Communication dans un congrès
- titre
- Consistency Implies Cut Admissibility
- auteur
- Guillaume Burel
- article
- PSATTT'11: International Workshop on Proof-Search in Axiomatic Theories and Type Theories, Germain Faure, Stéphane Lengrand, Assia Mahboubi, Aug 2011, Wroclaw, Poland
- Accès au texte intégral et bibtex
-
- titre
- Experimenting with deduction modulo
- auteur
- Guillaume Burel
- article
- 23rd International Conference on Automated Deduction, Jul 2011, Wroclaw, Poland. pp.162--176
- Accès au bibtex
-
2010
Article dans une revue
- titre
- Regaining Cut Admissibility in Deduction Modulo using Abstract Completion
- auteur
- Guillaume Burel, Claude Kirchner
- article
- Information and Computation, 2010, 208 (2), pp.140-164. ⟨10.1016/j.ic.2009.10.005⟩
- Accès au texte intégral et bibtex
-
2009
Communication dans un congrès
- titre
- Automating Theories in Intuitionistic Logic
- auteur
- Guillaume Burel
- article
- 7th International Symposium on Frontiers of Combining Systems -FroCoS'09, Sep 2009, Trento, Italy. pp.181-197, ⟨10.1007/978-3-642-04222-5_11⟩
- Accès au texte intégral et bibtex
-
Thèse
- titre
- Bonnes démonstrations en déduction modulo
- auteur
- Guillaume Burel
- article
- Informatique [cs]. Université Henri Poincaré - Nancy 1, 2009. Français. ⟨NNT : 2009NAN10014⟩
- Accès au texte intégral et bibtex
-
Pré-publication, Document de travail
- titre
- How can we prove that a proof search method is not an instance of another?
- auteur
- Guillaume Burel, Gilles Dowek
- article
- 2009
- Accès au texte intégral et bibtex
-
2008
Communication dans un congrès
- titre
- A First-Order Representation of Pure Type Systems Using Superdeduction
- auteur
- Guillaume Burel
- article
- 23rd Annual IEEE Symposium on Logic In Computer Science, Jun 2008, Pittsburgh, PA, United States. pp.253-263, ⟨10.1109/LICS.2008.22⟩
- Accès au texte intégral et bibtex
-
Pré-publication, Document de travail
- titre
- Efficiently Simulating Higher-Order Arithmetic by a First-Order Theory Modulo
- auteur
- Guillaume Burel
- article
- 2008
- Accès au texte intégral et bibtex
-
2007
Communication dans un congrès
- titre
- Unbounded Proof-Length Speed-up in Deduction Modulo
- auteur
- Guillaume Burel
- article
- 16th EACSL Annual Conference on Computer Science and Logic - CSL 2007, Jacques Duparc, Sep 2007, Lausanne, Switzerland. pp.496-511, ⟨10.1007/978-3-540-74915-8_37⟩
- Accès au texte intégral et bibtex
-
- titre
- Cut Elimination in Deduction Modulo by Abstract Completion
- auteur
- Guillaume Burel, Claude Kirchner
- article
- Symposium on Logical Foundations of Computer Science LFCS'07, Sergei Artemov, Jun 2007, New York, United States. pp.115-131, ⟨10.1007/978-3-540-72734-7_9⟩
- Accès au texte intégral et bibtex
-
2006
Communication dans un congrès
- titre
- Completion is an Instance of Abstract Canonical System Inference
- auteur
- Guillaume Burel, Claude Kirchner
- article
- Algebra, Meaning, and Computation: A Festschrift Symposium in Honor of Joseph Goguen, Jun 2006, San Diego/USA, pp.497-520, ⟨10.1007/11780274_26⟩
- Accès au texte intégral et bibtex
-
2005
Rapport
- titre
- Systèmes Canoniques Abstraits : Application à la Déduction Naturelle et à la Complétion
- auteur
- Guillaume Burel
- article
- [Travaux universitaires] Rapport de stage de master 2 annee MPRI / Universite Paris 7, 2005, pp.93
- Accès au texte intégral et bibtex
-
2003
Rapport
- titre
- Logique Equationnelle et probabilités selon Halpern
- auteur
- Guillaume Burel
- article
- [Stage] A03-R-321 || burel03a, 2003, 19 p
- Accès au texte intégral et bibtex
-