10 citations · 18 across the 5 of their papers we have counts for
5 papers
A Strategy Language for Controlled Proof Search
Romain Sidhoum, Simon Robillard, David Delahaye
This paper introduces the strategy language of Pgeon, a meta-prover with a clear separation between inference rules and proof search. We give the semantics of strategies as functio…
Dedukti: a Logical Framework based on the -Calculus Modulo Theory
Ali Assaf, Guillaume Burel, Raphaël Cauderlier +7
Dedukti is a Logical Framework based on the -Calculus Modulo Theory. We show that many theories can be expressed in Dedukti: constructive and classical predicate logic, Simpl…
Tableaux Modulo Theories Using Superdeduction
Mélanie Jacquel, Karim Berkani, David Delahaye +1
We propose a method that allows us to develop tableaux modulo theories using the principles of superdeduction, among which the theory is used to enrich the deduction system with ne…
Recovering Intuition from Automated Formal Proofs using Tableaux with Superdeduction
David Delahaye, Mélanie Jacquel
We propose an automated deduction method which allows us to produce proofs close to the human intuition and practice. This method is based on tableaux, which generate more natural…
Diophantus' 20th Problem and Fermat's Last Theorem for n=4: Formalization of Fermat's Proofs in the Coq Proof Assistant
David Delahaye, Micaela Mayero
We present the proof of Diophantus' 20th problem (book VI of Diophantus' Arithmetica), which consists in wondering if there exist right triangles whose sides may be measured as int…