Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction ModuloD Delahaye, D Doligez, F Gilbert, P Halmagrand, O Hermant
Logic for Programming, Artificial Intelligence, and Reasoning: 19th …, 2013
49 2013 Dedukti: a logical framework based on the λΠ-calculus modulo theory A Assaf, G Burel, R Cauderlier, D Delahaye, G Dowek, C Dubois, F Gilbert, ...
36 2016 Expressing theories in the λΠ-calculus modulo theory and in the Dedukti system A Assaf, G Burel, R Cauderlier, D Delahaye, G Dowek, C Dubois, F Gilbert, ...
TYPES: Types for Proofs and Programs, 2016
29 2016 Checking Zenon modulo proofs in Dedukti R Cauderlier, P Halmagrand
arXiv preprint arXiv:1507.08719, 2015
27 2015 Dedukti: a logical framework based on the λΠ-calculus modulo theory (2016) A Assaf, G Burel, R Cauderlier, D Delahaye, G Dowek, C Dubois, F Gilbert, ...
URL: http://www. lsv. fr/~ dowek/Publi/expressing. pdf, 2019
25 2019 Automated deduction in the B set theory using typed proof search and deduction modulo G Bury, D Delahaye, D Doligez, P Halmagrand, O Hermant
LPAR 20: 20th International Conference on Logic for Programming, Artificial …, 2015
25 2015 First-order automated reasoning with theories: when deduction modulo theory meets practice G Burel, G Bury, R Cauderlier, D Delahaye, P Halmagrand, O Hermant
Journal of Automated Reasoning 64 (6), 1001-1050, 2020
14 2020 Dedukti: a Logical Framework based on the lambda-pi-Calculus Modulo Theory. draft A Assaf, G Burel, R Cauderlier, G Dowek, C Dubois, F Gilbert, ...
INRIA, 2019
12 2019 Implementing polymorphism in Zenon G Bury, R Cauderlier, P Halmagrand
11th International Workshop on the Implementation of Logics (IWIL), 2015
7 2015 Dedukti: a Logical Framework based on the λΠ A Assaf, G Burel, R Cauderlier, D Delahaye, G Dowek, C Dubois, F Gilbert, ...
Calculus Modulo Theory, 2016
6 2016 Proof Certification in Zenon Modulo: When Achilles Uses Deduction Modulo to Outrun the Tortoise with Shorter Steps D Delahaye, D Doligez, F Gilbert, P Halmagrand, O Hermant
IWIL-10th International Workshop on the Implementation of Logics-2013, 2013
5 2013 Automated deduction and proof certification for the B method P Halmagrand
Conservatoire National Des Arts et Métiers, Paris, 2016
2 2016 Soundly proving B method formulae using typed sequent calculus P Halmagrand
International Colloquium on Theoretical Aspects of Computing, 196-213, 2016
2 2016 Dedukti: a Logical Framework based on the A Assaf, G Burel, R Cauderlier, D Delahaye, G Dowek, C Dubois, F Gilbert, ...
arXiv e-prints, arXiv: 2311.07185, 2023
1 2023 Déduction automatique et certification de preuve pour la Méthode B P Halmagrand
2016 Using Deduction Modulo in Set Theory P Halmagrand
SETS14, 1st International Workshop about Sets and Tools, 12, 2014
2014 Expressing theories in the λΠ-calculus modulo theory and in the Dedukti system G Dowek, CD Delahaye, F Gilbert, P Halmagrand, O Hermant, R Saillard
BWare B Proof Obligation Benchmark v1 D Delahaye, P Halmagrand
Automated Deduction in the B Set Theory using Deduction Modulo G Bury, D Delahaye, D Doligez, P Halmagrand, O Hermant
