Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo D Delahaye, D Doligez, F Gilbert, P Halmagrand, O Hermant Logic for Programming, Artificial Intelligence, and Reasoning: 19th …, 2013 | 48 | 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, ... | 32 | 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 | 26 | 2016 |
Checking Zenon modulo proofs in Dedukti R Cauderlier, P Halmagrand arXiv preprint arXiv:1507.08719, 2015 | 26 | 2015 |
Dedukti: a logical framework based on the λ Π-calculus modulo theory, 2019 A Assaf, G Burel, R Cauderlier, D Delahaye, G Dowek, C Dubois, F Gilbert, ... URL: http://www. lsv. fr/~ dowek/Publi/expressing. pdf, 2019 | 24 | 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 | 24 | 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 | 12 | 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 | 7 | 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 | 5 | 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 |
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 | | |