Publications HAL de Guillaume,Burel

2020

Journal articles

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
https://hal.science/hal-02908808/file/acmtocl.pdf BibTex

2019

Journal articles

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
https://hal.science/hal-02305831/file/dmt-in-atp.pdf BibTex

Conference papers

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
https://inria.hal.science/hal-02200548/file/main.pdf 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
https://cea.hal.science/cea-02874103/file/Teaching_Formal_Methods_to_Engineers.pdf BibTex

2018

Conference papers

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
https://inria.hal.science/hal-01670476/file/lipics.pdf BibTex

2016

Conference papers

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
https://minesparis-psl.hal.science/hal-01441751/file/A-654.pdf BibTex

Preprints, Working Papers, ...

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
https://inria.hal.science/hal-04281492/file/expressing.pdf BibTex
titre
Automata, Resolution, and Cut-elimination
auteur
Guillaume Burel, Gilles Dowek, Ying Jiang
article
2016
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04063102/file/automata.pdf BibTex

2015

Conference papers

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
https://hal.science/hal-01097412/file/translating-hollight-dedukti-pxtp-2015.pdf BibTex
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
https://inria.hal.science/hal-01252138/file/pkb.pdf BibTex

2014

Conference papers

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
https://inria.hal.science/hal-01097428/file/lncs.pdf BibTex

2013

Conference papers

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
https://inria.hal.science/hal-00921513/file/easychair.pdf 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
https://inria.hal.science/hal-00919759/file/theory_detection_free.pdf 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
BibTex

2012

Conference papers

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
BibTex

2011

Conference papers

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
https://inria.hal.science/inria-00614040/file/Burel.pdf 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
BibTex

2010

Journal articles

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
https://inria.hal.science/inria-00132964/file/gencomp_ic.pdf BibTex

2009

Conference papers

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
https://inria.hal.science/inria-00395934/file/FroCos.pdf BibTex

Theses

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
https://theses.hal.science/tel-01748505/file/manuscript.pdf BibTex

Preprints, Working Papers, ...

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
https://hal.science/hal-04078083/file/montreal.pdf BibTex

2008

Conference papers

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
https://inria.hal.science/inria-00198543/file/NJ_asLF.pdf BibTex

Preprints, Working Papers, ...

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
https://inria.hal.science/inria-00278186/file/speedup_HAL.pdf BibTex

2007

Conference papers

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
https://inria.hal.science/inria-00115556/file/bk_LFCS.pdf BibTex
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
https://inria.hal.science/inria-00138195/file/speedup_full.pdf BibTex

2006

Conference papers

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
https://inria.hal.science/inria-00000775/file/bk4jag-final.pdf BibTex

2005

Reports

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
https://inria.hal.science/inria-00000773/file/aacs.pdf BibTex

2003

Reports

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
https://inria.hal.science/inria-00107710/file/A03-R-321.pdf BibTex