Recherche - Archive ouverte HAL Accéder directement au contenu

Filtrer vos résultats

11 résultats
Page :
triés par
Image document

Implementing Polymorphism in Zenon

 Guillaume Bury , Raphaël Cauderlier , Pierre Halmagrand
11th International Workshop on the Implementation of Logics (IWIL), Nov 2015, Suva, Fiji
Communication dans un congrès hal-01243593v1
Image document

Proof Certification in Zenon Modulo: When Achilles Uses Deduction Modulo to Outrun the Tortoise with Shorter Steps

 David Delahaye , Damien Doligez , Frédéric Gilbert , Pierre Halmagrand , Olivier Hermant
IWIL - 10th International Workshop on the Implementation of Logics - 2013, Dec 2013, Stellenbosch, South Africa
Communication dans un congrès hal-00909688v1
Image document

Expressing theories in the λΠ-calculus modulo theory and in the Dedukti system

 Ali Assaf , Guillaume Burel , Raphal Cauderlier , David Delahaye , Gilles Dowek , et al.
TYPES: Types for Proofs and Programs, May 2016, Novi SAd, Serbia
Communication dans un congrès hal-01441751v1
Image document

Zenon Modulo: When Achilles Outruns the Tortoise using Deduction Modulo

 David Delahaye , Damien Doligez , Frédéric Gilbert , Pierre Halmagrand , Olivier Hermant
LPAR - Logic for Programming Artificial Intelligence and Reasoning - 2013, Dec 2013, Stellenbosch, South Africa. pp.274-290, ⟨10.1007/978-3-642-45221-5_20⟩
Communication dans un congrès hal-00909784v1
Image document

Using Deduction Modulo in Set Theory

 Pierre Halmagrand
SETS14, 1st International Workshop about Sets and Tools, Jun 2014, Toulouse, France. pp.12
Communication dans un congrès hal-01100512v1
Image document

Checking Zenon Modulo Proofs in Dedukti

 Raphaël Cauderlier , Pierre Halmagrand
Fourth Workshop on Proof eXchange for Theorem Proving (PxTP), Aug 2015, Berlin, Germany
Communication dans un congrès hal-01171360v1
Image document

Dedukti: a Logical Framework based on the λΠ-Calculus Modulo Theory

 Ali Assaf , Guillaume Burel , Raphaël Cauderlier , David Delahaye , Gilles Dowek , et al.
2016
Pré-publication, Document de travail hal-04281492v1
Image document

First-order automated reasoning with theories: when deduction modulo theory meets practice

 Guillaume Burel , Guillaume Bury , Raphaël Cauderlier , David Delahaye , Pierre Halmagrand , et al.
Journal of Automated Reasoning, 2019, 64 (6), pp.1001-1050. ⟨10.1007/s10817-019-09533-z⟩
Article dans une revue hal-02305831v1
Image document

Automated Deduction in the B Set Theory using Typed Proof Search and Deduction Modulo

 Guillaume Bury , David Delahaye , Damien Doligez , Pierre Halmagrand , Olivier Hermant
LPAR 20 : 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Nov 2015, Suva, Fiji. pp 42-58
Communication dans un congrès hal-01204701v2
Image document

Automated Deduction and Proof Certification for the B Method

 Pierre Halmagrand
Logic in Computer Science [cs.LO]. Conservatoire National Des Arts et Métiers, Paris, 2016. English. ⟨NNT : ⟩
Thèse tel-01420460v2
Image document

Soundly Proving B Method Formulae Using Typed Sequent Calculus

 Pierre Halmagrand
13th International Colloquium on Theoretical Aspects of Computing (ICTAC), Oct 2016, Taipei, Taiwan. pp 196-213, ⟨10.1007/978-3-319-46750-4_12⟩
Communication dans un congrès hal-01342849v1
Page :