12 citations · 23 across the 5 of their papers we have counts for
5 papers
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…
How can we prove that a proof search method is not an instance of another?
Guillaume Burel, Gilles Dowek
We introduce a method to prove that a proof search method is not an instance of another. As an example of application, we show that Polarized resolution modulo, a method that mixes…
EKSTRAKTO A tool to reconstruct Dedukti proofs from TSTP files (extended abstract)
Mohamed Yacine El Haddad, Guillaume Burel, Frédéric Blanqui
Proof assistants often call automated theorem provers to prove subgoals. However, each prover has its own proof calculus and the proof traces that it produces often lack many detai…
Translating HOL to Dedukti
Ali Assaf, Guillaume Burel
Dedukti is a logical framework based on the lambda-Pi-calculus modulo rewriting, which extends the lambda-Pi-calculus with rewrite rules. In this paper, we show how to translate th…
Efficiently Simulating Higher-Order Arithmetic by a First-Order Theory Modulo
Guillaume Burel
In deduction modulo, a theory is not represented by a set of axioms but by a congruence on propositions modulo which the inference rules of standard deductive systems---such as for…